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.
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.
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.
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? A gap of 4.76×10⁻⁶ and the transcendental obstruction via Lindemann–Weierstrass.