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.
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.
A practical guide to the proof-carrying rescue suite manifest: what the packets mean, what they prove, and what they deliberately do not claim.
A compact status table for Monogate's boundary rescue operators: Forge evidence, MachLib bridge status, and publication state.
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.
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.
One accounting identity for the SuperBEST node cost of a scientific equation. The decomposition (T38) is a definition, not a theorem; several results hold only as upper bounds, and the Quadratic Ceiling Conjecture and other problems are open. The predictions were checked on 100 validation equations.
Four structural classes, the cost decomposition (T38, a definition), complexity classes O(1)/O(N)/O(N²), and the Linear Ceiling Conjecture (T39): an upper-bound model of how many EML nodes a standard scientific equation needs.
Iterating exp(z)−k is Devaney's exponential family. We computed 8 operator fractal zoos, measured box-counting dimensions, and found DEML/EMN generate bounded strange attractors.
f(x) = exp(x) − ln(x) satisfies f(x) > x for all real x > 0. The gap is minimized at x ≈ 0.806, where f(x) − x ≈ 1.6486. This is a proposition (T11) about the operator's self-interaction; of the eight operators compared below, EMN and EDL have no real fixed points either.
Each Fourier harmonic is one complex EML node. We measured timbre complexity for 5 instruments and found: Sine=1n, Clarinet=5n, Violin=12n. EXL is the most musically useful operator.
The BEST router's mul entry drops to 3 nodes via exl(ln(x), exp(y)) = x·y. A search confirms 3 is the minimum over four operators (EML, EXL, EAL, EDL); with more operators multiplication takes 2 nodes, and 1 for x, y > 0.
DEML and EMN generate bounded 2D strange attractors. No classical period-doubling — the exponential family is a different universality class. Lyapunov landscape 92.9% correlated with Mandelbrot interior.
How close can an EML tree get to i? The closest depth-6 value is 4.76×10⁻⁶ away. The tan(1) obstruction once given is not a proof, and a depth-7 tree gets its imaginary part within 7.9×10⁻¹² of 1.