57 posts · ← monogate.org · RSS
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.
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.
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.
We measured the node-cost decay across seven basis states on 222 elementary-function equations. One primitive dominates: fused-multiply-add.
Across 315 tested equations, a clean dichotomy: oscillatory functions sit outside ELC with one exception — a non-elementary token.
The elementary logarithmic closure is bounded by two structurally independent obstructions. Classical analysis guards one edge; classical algebra guards the other.
We applied the DEML incompleteness template to seven exp-ln operators. Six are incomplete. One is open. One surprise: a gate with the identity function built in.
One formula predicts the SuperBEST node cost of any scientific equation. Proved, validated on 187 equations, and open-sourced.
At depth 5, all complex EML values have Im = −π exactly. At depth 6, imaginary parts explode. A structural phase transition.
Node-count and wall-clock benchmarks across 8 elementary functions. BEST dispatch vs naive EML.
Three completeness classes for exp-ln operators: exactly complete (EML), approximately complete (EMN), and incomplete (all others). Two new theorems prove EMN's exact limits and approximate power.
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.