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.