Monogate — Research Blog

Apollonius' problem has eight solutions in generic position.

We named a proof obligation about how fast a shallow exp–log expression can approach zero.

sin was the specific target.

A chain-order hierarchy theorem and an effective validity threshold — both flagged 'hard' by outside review months ago.

MachLib runs on axioms.

MachLib's real numbers are an axiomatized interface, kept Mathlib-free for build speed.

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.

The finite zero-count bound for iterated exponentials now reaches e^(e^(e^x)), unconditionally and with the Khovanskii-citation axiom removed.

A saturating guard keeps a plant's state inside a safe envelope for all time, for any controller, under any bounded disturbance.

One verified math source compiles to software, RTL, and a GPU shader.

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.

A 63-function corpus through 6 software backends, then 17 multi-function modules, then a Lean proof-emit survey.

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.

MachLib now ships a finite zero-count bound for polynomial-in-(x, eˣ), proven modulo an axiomatized analytic base.

We shipped a constructive Khovanskii framework on MachLib, then built the CI dashboard the framework deserved.

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.

578 expressions, 50 Lean theorems, 5 PyPI packages, an npm port, a HuggingFace dataset, three websites, four interactive demos.

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.

The best-selling synthesizer in history runs on a Bessel function.

The NAND gate of continuous math.

A 600-point parameter sweep across all 16 F16 operators shows that 12 of them collapse to period-2 dynamics, while the four multiplicative operators (EXL, DEXL, EXN, DEXN) exhibit long cycles, chaos, and a period-3 Sharkovskii signature.

The EAL self-map and the EXL self-map have completely different fixed points, yet both have derivative exactly 4.3164206… at those points.

We measured the node-cost decay across seven basis states on 222 elementary-function equations.

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.

Across 315 tested equations, a clean dichotomy: oscillatory functions sit outside ELC with one exception — a non-elementary token.

Six canonical electromagnetic formulas costed in F16 nodes.

The elementary logarithmic closure is bounded by two structurally independent obstructions.

Four things we retracted, corrected, or demoted during the 2026-04 foundation audit.

Classical integral transforms partition into three ELC-direction classes.

Every repelling fixed point of exp is an attracting fixed point of log on its branch, with reciprocal multipliers.

sinh, cosh, and tanh map ELC inputs to ELC outputs. sin, cos, and tan don't.

Iterate principal log on any seed in ℂ and you land at 0.318 + 1.337i.

How much accuracy you lose by approximating ReLU with the smooth softplus activation — to three decimals, this is a clean closed-form constant.

A complete catalog of SuperBEST node counts for standard equations across 12+ domains — from 1-node trivialities to 2037-node error correction.

The only operation in SuperBEST costing more than 3 nodes was general-domain addition at 11n.

Taylor series, integration, ODEs, autodiff, and Fourier transforms measured in EML nodes.

How many operator nodes does it take to compute 40 standard equations from chemistry and biology?

16 operators, one structural rule: exp(+x) with no domain restriction implies exactly complete. exp(-x) implies incomplete.

A thought experiment: if tan(1) could be built from EML trees, what would follow?

From Google's PageRank to your GPS to the NFL passer rating — every equation has a node count.

Four structural classes, the cost decomposition theorem (T38), complexity classes O(1)/O(N)/O(N²), and the Linear Ceiling Conjecture (T39): a complete theory of how many EML nodes any standard scientific equation requires.

One formula predicts the SuperBEST node cost of any scientific equation.