68 posts · ← monogate.org · RSS
sin was the specific target. It turns out sin was never the point — no finite EML tree can equal ANY nonconstant, continuous, periodic function, full stop. We built genuine Extreme Value Theorem machinery to get there, then found the proof didn't need it: periodicity alone does the work an infimum was supposed to. Honest scope inside.
MachLib runs on axioms. The last post showed Mathlib's ℝ models each one, by hand. This post makes that an always-on invariant: enumerate the axioms from the kernel, decide 'witnessed' by typechecking an interpretation — never by name — and diff both directions so it fails loud. The teeth were real: the audit rejected an axiom that was actually false, an open-interval Rolle a name-matching check would have rubber-stamped forever.
MachLib's real numbers are an axiomatized interface, kept Mathlib-free for build speed. There's now a machine-checked witness that those axioms are consistent: Mathlib's ℝ models every one of them, each #print axioms bottoming out in Lean's three. The analytic finite-zeros theorem, once postulated, is now proved. Honest scope inside.
The finite zero-count bound for iterated exponentials now reaches e^(e^(e^x)), unconditionally and with the Khovanskii-citation axiom removed. Proven from Rolle's theorem alone. Honest scope inside.
A saturating guard keeps a plant's state inside a safe envelope for all time, for any controller, under any bounded disturbance. We proved it in Lean (sorryAx-free), turned the proof into a number — and then made that number a machine-checked theorem too — and measured it holding on a real FPGA, on a noisy breadboard, and on a genuinely nonlinear plant, while we injected an actuator fault on purpose. The breadboard limit-cycled and looked nothing like the simulation; the envelope held anyway, because safety rides on the saturation, not on good control. Here is the receipt, the one place a skeptic would push, and exactly what we do not claim.
The Infinite-Zeros Barrier — the line between functions you can write as a finite EML tree and ones you can't — turns out to be the compact (rotational) factor of a differential Galois group. We connect the two, turn 'is this function representable?' into a computation from a differential equation, validate the special-function registry against it, and machine-check the core in Lean. Honest scope inside.
A 63-function corpus through 6 software backends, then 17 multi-function modules, then a Lean proof-emit survey. Four real Forge bugs and two eFrog bugs surfaced and fixed upstream with regression coverage. Hardware-target survey blocked on Pro license. Honest scope inside.
MachLib now has a second, fully constructive proof of the SingleExp Khovanskii zero-count bound, built on a polynomial canonicalizer instead of the ExpPolyBridge embedding. Same theorem, different machinery, same axiom footprint. Honest scope inside.
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.
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.
A bounded research ledger for where EML helps, where protected standard math wins, and which claims remain blocked.
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.
Forge now has a saturation-deshelf packet: finite clamp-shelf collapse, pre-clamp pressure replay, boundary-structure recovery, and a MachLib clamp-invariant obligation.
The Monogate boundary-event rescue suite now has four packet-backed lanes and a unified Forge manifest.
Forge now has a guard-clamp overflow rescue packet: raw overflow-wall failure, bounded guarded evaluation, guard-rescue transition, and MachLib output-safety obligation.
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.
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.
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.
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.
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.
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.
Apollonius' problem has eight solutions in generic position. While formalizing it in MachLib we assumed the obvious general-position condition — three equal circles, comfortably separated. That assumption is false. At the exact locus d² = 8ρ² one of the four solution classes loses its leading coefficient, its quadratic becomes linear, and the count drops to seven. Nothing in the picture degenerates. A live exhibit lets you cross the locus yourself.
We named a proof obligation about how fast a shallow exp–log expression can approach zero. It fit the lower-depth results and it looked right. It was false — and false at exactly one scale. Replacing a linear term by an exponential one yields a statement that is machine-checked, and the implication between the two is machine-checked as well. So the correction is not 'whatever the prover would accept': the stronger form is formally refuted, the weaker is formally proved, and their relationship is a theorem.
A chain-order hierarchy theorem and an effective validity threshold — both flagged 'hard' by outside review months ago. We stopped repeating the label and went looking for the actual obstruction in each. One real bridge theorem came out of it. Neither question closed. Both are now precisely located instead of vaguely deferred.
We lifted an earlier rolle-only, machine-checked finiteness proof from one hardcoded tower of iterated exponentials to arbitrary exponential-type Pfaffian chains at every depth — with one honest hypothesis we do not round off: positivity.
One verified math source compiles to software, RTL, and a GPU shader. We stopped trusting the model and ran each artifact for real — C on gcc, RTL in Verilator, a shader on an NVIDIA GPU, and the datapath on an Arty A7 FPGA — checking every output against a Lean-proved error bound. Each one held. Building it found six real bugs. Here is the receipt, and here is exactly where it doesn't hold.
A practical guide to the proof-carrying rescue suite manifest: what the packets mean, what they prove, and what they deliberately do not claim.
EML trees are dense in C([a,b]). Any continuous function approximable to arbitrary precision — but not always exactly representable.
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.
We measured the node-cost decay across seven basis states on 222 elementary-function equations. One primitive dominates: fused-multiply-add.
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.
From Google's PageRank to your GPS to the NFL passer rating — every equation has a node count. Here are the ones that matter.
How close can an EML tree get to i? A gap of 4.76×10⁻⁶ and the transcendental obstruction via Lindemann–Weierstrass.