A Constructive Khovanskii Reduction
MachLib now ships a finite zero-count bound for polynomial-in-(x, eˣ), proven modulo an axiomatized analytic base. A Forge-emitted Butler-Volmer kernel obligation closes on top of it. Honest scope inside.
Research Blog
55 posts · ← monogate.org · RSS
announcement 1theorem 17conjecture 3observation 13research 16deep dive 2exposition 1engineering 1meta 1
Search results
Featured
The Dashboard the Verification Needed
We shipped a constructive Khovanskii framework on MachLib, then built the CI dashboard the framework deserved. The dashboard caught us over-counting on its first run.
The EML Advantage Lab
A bounded research ledger for where EML helps, where protected standard math wins, and which claims remain blocked.
The First Proof-Carrying Rescue
A narrow Forge trace now demonstrates the Monogate stack's first end-to-end boundary rescue shape: raw domain-wall failure, log-domain lift, rescue packet, and MachLib positive-coordinate obligation.
The Fourth Proof-Carrying Rescue
Forge now has a saturation-deshelf packet: finite clamp-shelf collapse, pre-clamp pressure replay, boundary-structure recovery, and a MachLib clamp-invariant obligation.
Proof-Carrying Rescue Suite v0
The Monogate boundary-event rescue suite now has four packet-backed lanes and a unified Forge manifest.
The Second Proof-Carrying Rescue
Forge now has a guard-clamp overflow rescue packet: raw overflow-wall failure, bounded guarded evaluation, guard-rescue transition, and MachLib output-safety obligation.
The Third Proof-Carrying Rescue
Forge now has a precision-escape packet for a finite phantom-attractor trace: low-precision stalling, higher-precision sensitivity, escape to an interior event, and a MachLib precision obligation.
Why EML Optimization Lives on the Boundary
High-dimensional volume collapse explains why EML tree search hits corners, log-domain cliffs, overflow walls, and phantom-attractor behavior. The Monogate stack now has Forge traces, IR evidence, and MachLib theorem targets for it.
How Claude and I Built a Research Program in Two Weeks
578 expressions, 50 Lean theorems, 5 PyPI packages, an npm port, a HuggingFace dataset, three websites, four interactive demos. Two weeks. One human. Here's what actually worked, what failed, and what the audit system caught before it reached the public.
The Equation That Counts Physics
Hand a damped-oscillator equation to a computer and it can tell you, without knowing any physics, that there's one oscillation and one decay inside it. Across 193 expressions and 12 domains, this counter holds at ρ = +0.885.
Hear the Math: When Equations Become Sound
The best-selling synthesizer in history runs on a Bessel function. The Gibbs phenomenon's 9% overshoot is a theorem you can hear. Three interactive demos at 1op.io let you turn structural complexity into sound.
One Operator, All of Applied Mathematics
The NAND gate of continuous math. A single binary operation eml(x, y) = exp(x) − ln(y) generates every elementary function — and the structural fingerprint of an expression turns out to predict where it came from.
New
How to Read the Rescue Suite
A practical guide to the proof-carrying rescue suite manifest: what the packets mean, what they prove, and what they deliberately do not claim.
Proof-Carrying Rescue Status
A compact status table for Monogate's boundary rescue operators: Forge evidence, MachLib bridge status, and publication state.
When Olympiad Problems Produce EML Trees
Classical functional equations characterise exp and ln, and their solutions turn out to be minimal EML trees — often cheaper than the equations that define them.
FMA Is the Only Primitive That Matters
We measured the node-cost decay across seven basis states on 222 elementary-function equations. One primitive dominates: fused-multiply-add.
The Oscillation Boundary
Across 315 tested equations, a clean dichotomy: oscillatory functions sit outside ELC with one exception — a non-elementary token.
Two Boundaries of ELC
The elementary logarithmic closure is bounded by two structurally independent obstructions. Classical analysis guards one edge; classical algebra guards the other.
From the archive (picked at random)
The Operator Zoo: Which exp-ln Gates Are Complete?
We applied the DEML incompleteness template to seven exp-ln operators. Six are incomplete. One is open. One surprise: a gate with the identity function built in.
The Cost Theory Is Complete
One formula predicts the SuperBEST node cost of any scientific equation. Proved, validated on 187 equations, and open-sourced.
The Depth-6 Phase Transition
At depth 5, all complex EML values have Im = −π exactly. At depth 6, imaginary parts explode. A structural phase transition.
What BEST Routing Saves
Node-count and wall-clock benchmarks across 8 elementary functions. BEST dispatch vs naive EML.
The Completeness Trichotomy: EML, EMN, and Everyone Else
Three completeness classes for exp-ln operators: exactly complete (EML), approximately complete (EMN), and incomplete (all others). Two new theorems prove EMN's exact limits and approximate power.
The EML Self-Map Has No Fixed Points
f(x) = exp(x) − ln(x) satisfies f(x) > x for all real x > 0. The gap is minimized at x ≈ 1.31 where f(x) − x ≥ 1.648. This is a theorem about the operator's self-interaction — and it separates EML from every other operator in the family.