Theorem Catalog
Every result is labeled for what it actually is. Proved facts are theorems. Everything else is clearly marked.
17 theorems · 12 propositions · 15 open conjectures · 10 observations
Cards cite papers in python/paper/. The papers are kept as written, so several still state
claims these cards withdraw or correct; python/paper/ERRATA.md lists them.
THEOREM — Complete, checkable proof. No gaps. PROPOSITION — Proved, short or routine. CONJECTURE — Precisely stated, believed true, unproved. OBSERVATION — Empirical pattern. No proof. DEFINITION — A new concept or classification choice. SPECULATION — Interesting but not currently testable or provable.
THEOREM — 17 · Complete, checkable proof. No gaps.
T01 EML Universality LEAN ~
THEOREM External (Odrzywołek 2026) + Lean, 2026-04-25 · Core Algebra
eml(x, y) = exp(x) − ln(y) generates every elementary function as a finite binary tree. Published arXiv:2603.21852. Independently re-derived as a local Lean formalization: an EML-elementary predicate closed under composition, with the universality statement as its capstone.
Proof: Published, peer-reviewable proof, plus an independent local Lean 4 formalization (0 sorries): eml_universality, built from EML_k_closed_comp / IsEMLElementary.comp over the complex EML grammar. The Lean theorem is the definitional form: every function satisfying the IsEMLElementary predicate is realized by an EML tree. That every elementary function satisfies the predicate is the published result, not a Lean statement.
T17 Strict i-Unconstructibility (Lean-verified)
THEOREM Sprint2 · Complex EML
Under strict principal-branch semantics, i = √−1 is not constructible from {1} using the ceml grammar in finite depth. Under the complex principal branch, where the question is open (C01, C03), the depth-6 value closest to i is 4.76×10⁻⁶ away.
Proof: Lean 4: T19_i_unconstructible_strict in StrictBarrier.lean (the private monogate-research repo) compiles against Mathlib with no sorryAx, re-checked before every deploy at a pinned monogate-research commit (scripts/lean_claims.json). The proof is short, not inductive: the strict evaluator returns real numbers by construction, and i is not real. The file is not in the public monogate-lean library, so the card carries no lean link. Depth-6 exhaustive search under the complex principal branch, re-run on 2026-09-13 (/blog/near-miss prints the script): the closest value to i is 8.07×10⁻⁸ + 0.99999523722i, at distance 4.7634634×10⁻⁶.
T32 Mul ≥ 2 Nodes: the 16 Lean F16 Operators, All Reals LEAN ✓
THEOREM DOOR-1 · Core Algebra
No single node of the 16 operators defined in MonogateEML/MulLowerBound.lean, the F16 on /framework, computes x·y for all real x, y.
Proof: Lean 4, 0 sorries: SB_mul_ge_two, with an explicit witness pair for each operator (Mathlib's log). CORRECTION (2026-09-13): this card claimed the bound for every operator of the form h(exp(±x), ln y), by a derivative obstruction. That is false: h(u, v) = ln(u)·exp(v) gives x·y in one node for every x and every y > 0, and LEpow(x, y) = ln((eˣ)ʸ) = x·y is one node in T32_Mul_Absolute_Optimality.tex's own operator list. The Lean list is not that paper's F16 either: it has no EXL, EDL, EAL or EMN.
ADD-T1 Addition ≥ 2 Nodes — Lean Lower Bound LEAN ✓
THEOREM Lean Sprint 2026-04-21 · Core Algebra
No single F16 operator (the sixteen on /framework, defined in AddLowerBound.lean) computes x+y for all real x, y. Combined with LEDIV(x, DEML(y,1)) = x+y (2-node explicit construction), SB(add) = 2.
Proof: Lean 4, 0 sorries. Witness-based proof for each of 16 F16 operators.
T33 Subtraction ≥ 2 Nodes — Lean Lower Bound LEAN ✓
THEOREM Lean Sprint 2026-04-21 · Core Algebra
No single F16 operator (the sixteen on /framework) computes x−y for all real x, y. Combined with explicit 2-node construction, SB(sub) = 2.
Proof: Lean 4, 0 sorries. Exhaustive witness proof over all 16 F16 operators.
T_DIV_GEN_LB Division ≥ 2 Nodes (General Domain) — Lean LEAN ✓
THEOREM Lean Sprint 2026-04-21 · Core Algebra
No single F16 operator (the sixteen on /framework) computes x/y for all real x, y. General domain: ≥ 2 nodes (Lean-verified). For x, y > 0 two nodes suffice: D_F16(x, D_F13(−1, y)) = x/y (div_two_node_pos_domain, Lean-verified). CORRECTION (2026-09-13): this card said exp(ln x − ln y) is 1 node on the positive domain; that operator is not one of the 16, and /superbest lists div for x, y > 0 as 2n.
Proof: Lean 4, 0 sorries. Witness (0,1) for each of 16 F16 operators.
T_DIV_EXP_OUTER Division, General Domain: No 2-Node exp-Outer Circuit — Lean LEAN ✓
THEOREM Lean, 2026-04-24 · Core Algebra
No 2-node F16 circuit with an exp-type outer operator (F13–F16) computes x/y for all real x, y — such circuits are always positive, but x/y takes negative values (witness (x,y) = (−1,2)). A further, Lean-proved step toward a general-domain ≥ 3 bound. Honest scope: the remaining F1–F12 outer cases are NOT Lean-proved — see the SuperBEST table's general div entry (8n as one F16 tree since 2026-09-13) for the precise status of that stronger claim.
Proof: Lean 4, 0 sorries. no_F13_outer_2node_div / no_F14_outer_2node_div / no_F15_outer_2node_div / no_F16fn_outer_2node_div, each via the shared lemma always_pos_ne_div (an always-positive function cannot equal x/y, which is negative at (−1,2)).
Depends on: T_DIV_GEN_LB.
T_SUPERBEST_UB SuperBEST Upper Bounds — 5 Positive-Domain Identities (Lean) LEAN ✓
THEOREM Lean Sprint 2026-04-21 · Core Algebra
Lean-verified (0 sorries): exp(x)=F1(x,1) (1n); exp(ln x+ln y)=xy for x,y>0 (1n); exp(n·ln x)=xⁿ for x>0 (1n); exp(−ln x)=1/x for x>0 (1n); exp(½·ln x)=√x for x>0 (1n). Counted with ln x = EXL(0, x) as one node (EXL is a census operator outside the sixteen on /framework), the v5.3 positive total is 14n (savings 80.8%), the sum ModelAudit.lean states. Counted in F16 alone, where ln x = LEdiv(0, F13(−1, x)) takes 2 nodes, it is 15n (79.5%): /superbest's figure since 2026-09-13, checked numerically and not stated by any Lean theorem.
Proof: Lean 4, 0 sorries. UpperBounds.lean + ModelAudit.lean. Mathlib: Real.exp_add, Real.exp_log, Real.rpow_def_of_pos, Real.sqrt_eq_rpow.
T_EULER_LEAN Euler Gateway + Euler Identity + Depth Hierarchy (Lean) LEAN ✓
THEOREM Lean Sprint 2026-04-21 · Complex EML
Three Lean-verified results: (T03) ceml(ix,1) = exp(ix) for x∈ℝ — Euler Gateway; (T05) ceml(iπ,1)+1 = 0 — Euler Identity; (T06) EML-0 ⊊ EML-1 — exp(x) is EML-1 and non-constant.
Proof: Lean 4, 0 sorries. euler_gateway: Complex.log_one. euler_identity: Complex.exp_pi_mul_I. exp_not_constant: Real.exp_one_gt_d9 via real-part extraction.
T01a sin Has Infinitely Many Zeros — Lean (Part A of T01) LEAN ✓
THEOREM Lean Sprint 2026-04-21 · Analytic Properties
The set {x∈ℝ | sin(x)=0} is infinite. Explicit: sin(nπ)=0 for all n∈ℤ, map n↦nπ is injective. Part A of the Infinite Zeros Barrier. Parts B (analytic non-zero functions have finitely many zeros) and C (well-formed EML trees are analytic on (0,∞)) are now also closed in Lean, 0 sorries each — only Part D, the uniform-in-depth barrier (sin_not_in_eml / sin_not_in_real_EML_k), remains open, gated on Khovanskii zero-count / o-minimal machinery not yet in Mathlib. See T01b for what is provable at small fixed depths without that machinery. The conclusion itself, that sin is not a real EML tree at any depth, is established another way in MachLib, by periodicity rather than zero counting (see /blog/periodicity-is-enough).
Proof: Lean 4, 0 sorries. sin_int_pi_zero: Real.sin_int_mul_pi. sin_has_infinitely_many_zeros: Set.infinite_range_of_injective.
Depends on: T01 (partial).
T01b sin ∉ EML at Fixed Small Depths 0–1 — Lean (no Khovanskii needed) LEAN ✓
THEOREM Lean, 2026-06-10 · Analytic Properties
No depth-0 or depth-1 EML tree equals sin(x) for all real x. Proved by direct two-point evaluation (at x=0 and x=π/2), case-split over each of the six grammar shapes reachable at depth ≤ 1 — sidestepping Part D's Khovanskii/o-minimal requirement entirely. The technique is stated to generalize mechanically to any fixed depth by extending the case enumeration; depth ≤ 2 has not been carried out.
Proof: Lean 4, 0 sorries. sin_not_in_eml_depth_le_0 (const/var, two-point contradiction). sin_not_in_eml_depth_le_1 (adds the four ceml(const/var, const/var) shapes).
Depends on: T01a.
T_EXP_LOG_DUALITY Exp–Log Multiplier Duality at Fixed Points (Lean) LEAN ✓
THEOREM Blind Session Follow-up 2026-04-22 · Complex EML
At any z ∈ slit plane with Complex.exp(z) = z, the multiplier product (exp)′(z)·(log)′(z) = 1. Corollary: every fixed point of exp is repelling under exp (|mult| = |z| > 1 for Lambert z_k*) and attracting under log on its branch (|mult| = 1/|z| < 1).
Proof: Lean 4, 0 sorries. Chain rule + Complex.hasDerivAt_exp + Complex.hasDerivAt_log in Mathlib (the revision monogate-lean's lake-manifest.json pins). Numerical evidence: all 7 tested Lambert fixed points z_k* (|k|≤3) satisfy |exp-mult|·|log-mult| = 1 to 10⁻¹⁵. Reproduce: python exploration/blind-sessions/scripts/s02_sin_vs_exp_tower.py. The corollary's |z| > 1 is not a Lean statement. On paper: if z = a + ib is a fixed point with a ≤ 0, then |z| = eᵃ ≤ 1, so |b| ≤ 1; b = 0 is impossible because eᵃ > a for every real a, and for 0 < |b| ≤ 1 the imaginary part gives |b| = eᵃ|sin b| < |b|. So a > 0 and |z| = eᵃ > 1.
T_HYP_ELC_PRESERVE Hyperbolic Functions Preserve ELC (Lean) LEAN ~
THEOREM Blind Session Follow-up 2026-04-22 · Operator Family
sinh(x) = (exp(x)−exp(−x))/2, cosh(x) = (exp(x)+exp(−x))/2, tanh(x) = sinh(x)/cosh(x). Hence sinh, cosh, tanh map ELC(ℝ) → ELC(ℝ). Contrast with sin and cos, which do not preserve ELC: sin(x) and cos(x) are not real EML trees at any depth (MachLib's periodic barrier; the T01 Infinite Zeros Barrier argument for the same fact still has open steps). Includes 3-4-5 Pythagorean triple witness: sinh(ln 2)=3/4, cosh(ln 2)=5/4, 5²−3²=4².
Proof: Lean 4, 0 sorries. Real.sinh_eq, Real.cosh_eq, Real.tanh_eq_sinh_div_cosh in Mathlib (the revision monogate-lean's lake-manifest.json pins); numerical 3-4-5 witnesses via norm_num at ln 2. Lean checks the three identities and the 3-4-5 witnesses; the ELC-closure consequence is not stated in Lean.
LOG_X_NOT_DEPTH_LE_TWO log x is unreachable at depth ≤ 2 LEAN ✓
THEOREM Finite-depth tameness, 2026-08-19 · Depth Hierarchy
No EML tree of depth ≤ 2 agrees with log x on (0, ∞). Proved via the below-identity-unbounded class: log x is unbounded above yet eventually strictly below the identity, and no expression of depth ≤ 2 lies in that class.
Proof: Lean 4, MachLib. log_x_not_depth_le_two, from log_belowIdentityUnbounded and belowIdentityUnbounded_not_depth_le_two. sorryAx absent. Non-vacuity checked adversarially: the depth-3 analogue of this statement is provably false, witnessed by logTree var.
LOG_X_DEPTH_THREE_WITNESS log x is realised at depth 3 LEAN ✓
THEOREM Finite-depth tameness, 2026-08-19 · Depth Hierarchy
logTree var has depth exactly 3 and evaluates to log x for every real x. The logarithm arrives negated and behind an exponential inside an eml node, so recovering it costs the two-level negation gadget on top of the node that produces it.
Proof: Lean 4, MachLib. logTree / logTree_eval (unconditional, all reals) with depth 3 by rfl; paired with the lower bound in log_x_depth_exact_three, which carries the domain in its statement. sorryAx absent.
X_PLUS_ONE_NOT_DEPTH_LE_THREE x + 1 is unreachable at depth ≤ 3 LEAN ✓
THEOREM Finite-depth tameness, 2026-08-19 · Depth Hierarchy
No EML tree of depth ≤ 3 agrees with x + 1 on (0, ∞). Instantiation of the intermediate-growth band exclusion at x + 1, which requires all four band conditions — unbounded, sub-exponential, superlinear and super-logarithmic.
Proof: Lean 4, MachLib. x_plus_one_not_depth_le_three, from x_plus_one_band_hyps (IntermediateBand (fun x => x + 1)) and intermediateBand_not_depth_le_three. The fourth band condition was missing until 2026-08-19, which is why this bound was open: the exclusion cannot be instantiated on a partial premise. sorryAx absent. Non-vacuity checked: the depth-4 analogue is provably false, witnessed by xPlusOneTree.
X_PLUS_ONE_TREE_DEPTH x + 1 is realised at depth 4 LEAN ✓
THEOREM Finite-depth tameness, 2026-08-19 · Depth Hierarchy
xPlusOneTree = negOffset (log 2) (negOffset 0 var) has depth exactly 4 and evaluates to x + 1 for every real x, with no side condition — so it holds on all of ℝ, a superset of the domain claimed here. The claim is stated on (0, ∞) so that it pairs with the lower bound on exactly the same domain. The grammar has no addition; it has negation, at two levels per use, and negating twice adds.
Proof: Lean 4, MachLib. xPlusOneTree_eval / xPlusOneTree_depth via x_plus_one_in_eml; x_plus_one_depth_exact_four states both halves in one declaration. The construction holds on all of ℝ, a superset of the exclusion's domain, so the pairing is sound. sorryAx absent.
PROPOSITION — 12 · Proved, short or routine.
T09 Negation in 2 Nodes
PROPOSITION Sprint2 · Core Algebra
neg(x) = −x for all real x in 2 nodes: exl(0, deml(x,1)) = e⁰·ln(e⁻ˣ) = −x, and deml(x,1) = e⁻ˣ > 0, so the tree is defined everywhere.
Proof: Direct computation; the reproducer below checks it. CORRECTION (2026-09-13): this card was a THEOREM calling 2 nodes optimal, with 1 node ruled out by exhaustive search. No search on record supports that. The only 1-node neg search (python/scripts/research_neg_add.py at 3e447127, deleted in bec74da7) rounds each value to 6 decimals and then compares it with −x at tolerance 1e−7, so at x = π it rejects every tree, exact ones included; its own 2-node enumeration finds no neg either. research_neg_optimality.py, which SuperBEST_v3.tex cites for this card, runs no 1-node search. Whether one node can suffice depends on the operator family and the constants allowed: LEpow(x, −1) = ln((eˣ)⁻¹) = −x is one node in T32_Mul_Absolute_Optimality.tex's operator list. (An earlier correction, 2026-07-23, removed a Lean badge citing a NegLowerBound.lean that was reverted the day it was added.)
python -c "import math; exl=lambda x,y: math.exp(x)*math.log(y); deml=lambda x,y: math.exp(-x)-math.log(y); print(round(exl(0,deml(1.5,1)),10))"
T10u Multiplication in 2 Nodes for x > 0 (a construction, superseded as the optimum)
PROPOSITION Depth Spectrum · Core Algebra
ELAd(EXL(0,x), y) = x·y for x > 0 and all real y, with ELAd(a,b) = eᵃ·b: a 2-node construction. In the 16-operator set of Mul_Tightening_and_SuperBEST_v2.tex §1 with leaves {x, y, 0, 1}, no 1-node tree computes x·y on x, y > 0, so 2 is the minimum in that set. It is not the minimum in the current F16: exp(ln x + ln y) = x·y is 1 node for x, y > 0 (see T_SUPERBEST_UB, Lean-verified), and the general-domain figure is 3n (see /superbest). T29's F6 comparison (3 nodes there) still stands.
Proof: Exhaustive search over the 256 one-node and 32,768 two-node trees of that set, at points with x, y > 0: no 1-node tree and exactly 4 two-node trees compute x·y (python/scripts/mul_lower_bound_search.py at b7ffdb0a, deleted in bec74da7; a re-run on 2026-09-13 reproduces the result). CORRECTION (2026-09-13): this card was a THEOREM saying mul takes exactly 2 nodes. That holds only in the April operator set on the positive quadrant: exp(ln x + ln y) is 1 node for x, y > 0, and the construction fails for x ≤ 0. (The 2026-07-22 audit had already withdrawn 'optimal in F16'.)
Depends on: T29.
T11 EML Self-Map Has No Fixed Points
PROPOSITION Sprint2 · Analytic Properties
For all x > 0: eml(x,x) = exp(x) − ln(x) > x, so the map x ↦ eml(x,x) has no fixed point in (0, ∞). The gap exp(x) − ln(x) − x has its unique minimum at x* ≈ 0.8064659942, the root of eˣ = 1 + 1/x, where it equals ≈ 1.648605440.
Proof: The gap g(x) = eˣ − ln x − x has g″(x) = eˣ + 1/x² > 0, so it is convex with a single critical point (python/paper/preprint_addendum_emn_mul_math.tex §B3). Independently, eˣ ≥ 1 + x + x²/2 and ln x ≤ x − 1 give g(x) ≥ (x − 1)²/2 + 3/2 > 0. CORRECTION (2026-09-13): this card was a THEOREM putting the minimum at x ≈ 1.7632 with gap ≥ 1.648629…. The derivative there is about 4.26, not 0, and the true minimum, 1.648605…, is below 1.648629, so the stated bound was false. The no-fixed-point claim is unaffected.
T29 Mul ≥ 3 Nodes in F6
PROPOSITION Depth Spectrum · Core Algebra
No 1-node or 2-node tree over F6 = {EML, EDL, EXL, EAL, EMN, DEML} with leaves {x, y, 0, 1} computes mul(x,y) = x·y on x, y > 0. EXL(EXL(0,x), EML(y,1)) = x·y for x > 0 is a 3-node construction, so 3 is the minimum over that set.
Proof: Exhaustive search over all 96 one-node and 4,608 two-node trees of that set, at 8 points in (0, ∞)²: no match, and the closest miss is off by 0.625 (python/scripts/mul_lower_bound_search.py at b7ffdb0a, deleted in bec74da7; a re-run on 2026-09-13 reproduces the April result). Trees with other real constants as leaves were not searched. CORRECTION (2026-09-13): this card was a THEOREM and gave 12,288 two-node trees. The search enumerates 4,608; Mul_Tightening_and_SuperBEST_v2.tex Lemma 2.2 computes 4,608 and then asserts 12,288 without a derivation. The card also did not name the leaf set or the domain.
T34 Naive Upper Bound
PROPOSITION COST-2 · Cost Theory
If each primitive operation op is realised by an F16 gadget of c_op nodes that is valid on the domain where E uses it, then Cost(E) ≤ Σ c_op·n_op(E): the gadgets compose with no extra nodes.
Proof: COST2_Naive_Upper_Bound.tex §3, Theorem T34. CORRECTION (2026-09-13): this card was a THEOREM stating the bound with the SuperBEST v3 unit costs as printed, and a tightness "iff" credited to R1_Cost_Definition.tex, which states no tightness conditions. The printed div = 1 has no valid gadget over all reals (no single F16 operator computes x/y, T_DIV_GEN_LB), so the bound as printed fails for x/y, and the 2-node mul gadget needs x > 0. The "iff" (COST2 §4) is false: e^{x₁} + e^{x₂} has no shared subtree, no catalogued pattern and no constant, yet EML(LEAd(x₂, EML(x₁,1)), 1) computes it in 3 nodes, below its naive cost of 4.
T08 SuperBEST Table v4 — 19 Nodes by Construction, Not All Optimal
PROPOSITION Sprint2 / Sprint3 / S-T08 · Core Algebra
SuperBEST v4 (2026-04-20): 19 nodes over 10 entries, each an explicit construction. recip=1n (ELSb(0,x)=1/x, x>0), div=2n (ELSb(ln(x),y)), sub=2n (LEdiv(x, EML(y,1)), T33), mul=2n (ELAd(EXL(0,x), y), x>0, T10u), neg=2n (EXL(0, DEML(x,1)), T09), add=3n, pow=3n, sqrt=2n, exp=1n, ln=1n. CORRECTION (2026-09-12): this card said every entry was structurally proved optimal. That was wrong. add is 2n for all real x, y (LEdiv(x, DEML(y,1)), ADD-T1). pow and sqrt are 1n for x > 0 (EPL(n,x) = exp(n·ln x), EPL(0.5,x)), and mul is 1n for x, y > 0 (exp(ln x + ln y)); see T_SUPERBEST_UB. The current table is on /superbest.
Proof: Each entry is an explicit identity, checkable by hand. The S-T08 structural audit (2026-04-20; python/paper/theorems/SuperBEST_v4_Structural_Audit.tex) also argued a lower bound for every entry, and three of those arguments were wrong: add ≥ 3 (cross-derivative), pow ≥ 3 (3-intermediate) and sqrt ≥ 2 (derivative obstruction) are each beaten by a construction inside the same 16-operator family. mul ≥ 2 over all reals holds (T32), but the 2-node construction needs x > 0. Lower bounds that hold over all reals: sub ≥ 2 (T33), add ≥ 2 (ADD-T1), mul ≥ 2 (T32), div ≥ 2 (T_DIV_GEN_LB). exp, ln and recip are one node, trivially minimal.
Depends on: T09, T10u, T12, T32, T33, R16-C1, ADD-T1, T_SUPERBEST_UB, T_DIV_GEN_LB.
T21 EXL Log-Structure Advantage
PROPOSITION Sprint2 · Operator Family
EXL(x,y) = exp(x)·ln(y) achieves ln(x) in 1 node: EXL(0,x) = ln(x). EXL is a census operator, not one of the sixteen on /framework; inside that F16, ln x needs 2 nodes, since no single F16 node equals it and LEdiv(0, F13(−1, x)) does. The "fastest multiplication route" half of the original claim is superseded — see T10u's correction — by a separate 1-node positive-domain identity, not this EXL route.
Proof: Direct computation: EXL(0,x) = 1·ln(x) = ln(x). The ELAd(EXL(0,x), y) = x·y route is a valid 2-node construction (T10u), not the current minimum.
T25 Depth-6 Phase Transition
PROPOSITION Sprint2 · Complex EML
Built from the leaf 1 with the principal complex logarithm, counting tree depth: every value of depth at most 4 is real; at depth 5 non-real values appear, and every one has imaginary part exactly −π; at depth 6 there are 13,600 distinct imaginary parts, the closest to 1 being 0.99999524. Counting eml nodes instead: trees with at most 4 nodes are real, 5-node trees have imaginary parts 0 and −π, and 6-node trees add 1.50795.
Proof: Exhaustive enumeration, rebuilt on 2026-09-13; /blog/depth-6-phase-transition prints the 29-line mpmath script. At 50 and at 80 digits it gives 397 values through depth 4, all real; 77,528 values through depth 5, of which 13,598 are non-real; and 13,600 distinct imaginary parts at depth 6 (closest to 1: 0.9999952372, a gap of 4.76×10⁻⁶). It skips pairs whose exponential eᵃ has Re a > 10⁵. Those are real or have imaginary part −π, so the depth-5 statement covers them, and the depth-6 count is a lower bound. Why −π: through depth 4 every value is real, so a non-real depth-5 value is eᵃ − ln b with b < 0, and ln b = ln|b| + iπ. No script was kept before: the page named experiments/complex_closure_depth6.py, which was never in this repository. CORRECTION (2026-09-13): this card said the depth-6 imaginary parts become dense and spread across ℝ; the depth-6 value set is finite. It also listed T31 as a dependency, which its computation does not use. A second correction the same day: the card then gave three distinct imaginary parts at depth 6, in [−π, 1.508]. That is the count by eml nodes (0, −π and 1.50795), not by depth.
T35 Intermediate-Value Lower Bound (T36; T35 and T37 withdrawn)
PROPOSITION COST-3 · Cost Theory
If every F16 DAG computing f must produce at least d distinct non-terminal intermediate values, then Cost(f) ≥ d, since each internal node outputs exactly one value.
Proof: COST3_Lower_Bound.tex §3, Theorem T36 and its corollary: one value per node. CORRECTION (2026-09-13): this card was a THEOREM bundling three bounds. T37, Cost(E) ≥ n_exp + n_ln, is false: EML(x, y) = eˣ − ln y is one node holding one exp and one ln, and the proof's claim that exp-nodes and ln-nodes are distinct (COST3 §4) is wrong. T35, Cost(E) ≥ |O(E)|, is withdrawn: "cannot be merged" is never defined, and its other printed form, Cost(E) ≥ 1, fails for LEdiv(x, 1) = x, which costs 0. The R18 audit's approval of all three is superseded.
T40 Linear Cost Law (naive count and upper bound)
PROPOSITION COST-9 / R5 · Cost Theory
For an N-term sum E_N joined by N − 1 additions, with per-term naive cost α₀: NaiveCost(E_N) = (α₀ + c_add)·N − c_add. With the 2-node addition LEdiv(x, DEML(y,1)) = x + y (all real x, y; ADD-T1), Cost(E_N) ≤ (α₀ + 2)·N − 2 whenever each term's naive cost is a valid upper bound (T34).
Proof: R5_Linear_Cost_Law.tex §3.1, by counting term and join nodes. CORRECTION (2026-09-13): this card was a THEOREM stating Cost(E_N) = (α₀ + 3)·N − 3 exactly (softmax 4N − 3, Shannon entropy 6N − 3, Taylor 8N − 3). Exactness came from T38, which is a definition, and it is false: x₁ + x₂ costs 2, not 3 (LEdiv(x₁, DEML(x₂,1))), and Σ e^{xᵢ} costs at most 2N − 1 (S₁ = EML(x₁,1), S_{k+1} = EML(LEAd(x_{k+1}, S_k), 1)). Addition takes 2 nodes for all real inputs, so the positive domain saves nothing, and an EAL node is not an addition. The R18 audit's approval is superseded.
Depends on: T34, ADD-T1.
P-NNP No Nesting Penalty Lemma
PROPOSITION COST-6 / R3 · Cost Theory
For any operators O₁, O₂ and expressions A, B, C: Cost(O₁(O₂(A,B), C)) ≤ c(O₁) + c(O₂) + Cost(A) + Cost(B) + Cost(C). Nesting adds no interface nodes.
Proof: Upper bound: explicit DAG construction (python/paper/cost_theory/R3_No_Nesting_Penalty.tex). CORRECTION (2026-09-13): this card stated equality. The lower bound is false: LEdiv(LEdiv(x,1),1) = x costs 0, not 2, and LEdiv(EML(x,2),1) = EML(x,2) costs 1, not 2. A minimal DAG need not contain the sub-DAGs the argument assumes.
P-ACL Additive Cost Law
PROPOSITION R6 · Cost Theory
For independent expressions E₁, E₂ and a single-node operator op: Cost(op(E₁,E₂)) ≤ Cost(E₁) + Cost(E₂) + 1. The node counts quoted for the Lorentz force (57n) and Black–Scholes (47n) use it, so they are upper bounds.
Proof: Upper bound: disjoint optimal DAGs plus one root node (python/paper/cost_theory/R6_Additive_Cost_Law.tex). CORRECTION (2026-09-13): this card stated equality. The lower bound is false: with E₁ = EML(x, 2) and E₂ = 1, which share no leaves, LEdiv(E₁, 1) = E₁ costs 1, not 2.
CONJECTURE — 15 · Precisely stated, believed true, unproved.
T12 Exponential Position Theorem
CONJECTURE COMP-1 through COMP-5 · Operator Family
Over ℂ with the principal logarithm, among the 16 standard exp-ln binary operators: 8 are exactly complete (all with exp(+x), no domain restriction), 1 approximately complete (EMN), 7 incomplete. The completeness class is determined entirely by the position of negation relative to exp.
Evidence: Forward direction (T26): exp(+x) → complete. Reverse (T27): exp(−x) → incomplete by 5 distinct barrier types. LEX (T28): domain collapse. CORRECTION (2026-09-12): this card was a THEOREM; its count of 7 incomplete operators rests on T27, whose DEML case (T13) is not proved. CORRECTION (2026-09-13): the other cases are unproved too. The forward direction (T26), the EMN case (T24) and the LEX case (T28) are conjectures; T28's domain-collapse argument is refuted by explicit trees; and over ℝ the count of 8 is false, since every real EAL tree is nondecreasing.
Depends on: T09, T26, T27, T28, T24.
T13 DEML Incompleteness
CONJECTURE Sprint2 · Operator Family
deml(x,y) = exp(−x) − ln(y) is not exactly complete: neg(x) = −x is not constructible from DEML and constant 1.
Evidence: An exhaustive search over all 862,118 DEML trees up to N = 17 nodes found no neg construction; the closest has max error 0.84 on [0.5, 3.14]. The search record, python/results/s_r1_deml_incompleteness.json, gives max_N_searched 17 and closest error 0.84 but misstates the total as 861,952; /blog/deml-is-incomplete prints a script that reproduces the search. The structural argument, that every DEML tree's linear component has slope 0 or +1, has a gap: its first case assumes each subtree f(x) grows with x or is bounded, and f(x) = deml(x,1) = exp(−x) does neither. No Lean proof. CORRECTION (2026-09-12): this card was a THEOREM citing that argument as its proof, and gave the search as N ≤ 13; the search record says N ≤ 17.
Depends on: T12.
T14 Zeros Bound for Depth-k Trees
CONJECTURE Sprint2 · Analytic Properties
Let T be a real EML tree over leaves {1, x} of depth k (leaves have depth 0), and I an open interval on which every ln argument in T is positive and T is not identically zero. Then T has at most 2^k zeros in I.
Evidence: No proof. The cited induction, that each node at most doubles the zero count, is not valid: the zeros of exp(A) − ln(B) are not determined by the zeros of A and B (eml(1, x) = e − ln x vanishes at x = e^e, where neither leaf does). The 2k+2 version on /blog/tight-zeros-bound has no complete proof either. No Lean proof; a depth-k zero-count bound is the open sorry in InfiniteZerosBarrier.lean. CORRECTION (2026-09-13): this card was a THEOREM stating that every depth-k tree has at most 2^k real zeros and that the bound is tight. Without the hypothesis that T is not identically zero the statement is false: eml(x, eml(eml(x,1),1)) = e^x − ln(e^(e^x)) is zero for every real x, at depth 3. The tightness clause was also false: the four depth-1 trees have at most one zero.
T24 EMN Approximate Completeness
CONJECTURE Sprint2 · Operator Family
emn(x,y) = ln(y) − exp(x), evaluated with the principal complex logarithm over leaves {1, x}: (a) for every elementary f, every compact interval K in its domain and every ε > 0, some finite EMN tree T has |T(x) − f(x)| < ε on K; (b) no finite EMN tree equals ln(x) on an open interval.
Evidence: No proof of either part. The census sketch for (a) says that iterating a pointwise argument "gives the approximation property"; the addendum's sketch mirrors EML trees through EML = −EMN, which negates only the root node. The sketch for (b) reduces ln(x) to R(x) = x·exp(exp(L(x))) and stops at "infinite regress". Exhaustive search to 8 nodes: the best mean squared error for ln(x) fell to 5.0×10⁻²⁴ at 7 nodes (the 0 at 8 nodes is float underflow), consistent with doubly-exponential decay. CORRECTION (2026-09-13): this card was a THEOREM; neither half has a complete proof, and part (b) is the EMN case of T12, which is a conjecture.
Depends on: T12.
T26 Forward Completeness (per operator, over ℂ)
CONJECTURE COMP-2 · Operator Family
Over ℂ with the principal logarithm and leaves {1, x}, each of EAL, EXL, EDL, EPL, LEAd, ELAd and ELSb is exactly complete, as EML is (T01).
Evidence: No proof. The census argument builds exp(x) and e^c − x for EML only, uses the constant e (not a leaf) for EXL, EDL and EPL, reaches LEAd's identity only as a limit, and obtains neg(x) from exl(0, deml(x,1)) (T09), which uses two different operators and the constant 0. Its lemma that exp, ln and neg suffice builds no two-argument operation. Over ℝ the EAL case is false: every real EAL tree T = exp(A) + ln(B) has T′ = A′·exp(A) + B′/B ≥ 0, so none comes within 1/2 of −x on [0, 1]. CORRECTION (2026-09-13): this card was a THEOREM stating that every O(x,y) = h(exp(x), ln y) without a domain restriction is exactly complete. As written that is false: h(a,b) = b gives O = ln y, whose trees never produce exp(x), and h(a,b) = b − a gives EMN, which the catalog does not list as exactly complete (T24). Its proof used operators other than O.
Depends on: T09, T12.
T27 Reverse Incompleteness: exp(−x) → Incomplete
CONJECTURE COMP-3 · Operator Family
Let O(x,y) = h(exp(−x), ln y), h ∈ {−, +, ×, /, ^}. Then O is incomplete. The 6 operators DEML, DEMN, DEAL, DEXL, DEDL, DEPL each fail by a distinct mechanism.
Evidence: DEML: slope barrier (+1), which is T13's argument, and that has a gap. DEMN: domain failure (outputs always negative). DEAL: irremovable e⁻¹ offset. DEXL: dead constant at c=1. DEDL/DEPL: exponential decay. All verified computationally. No Lean proof. CORRECTION (2026-09-12): this card was a THEOREM; its DEML case rests on T13, which is not proved, so the statement as a whole is not proved.
Depends on: T12, T13.
T28 LEX Incompleteness
CONJECTURE COMP-3 · Operator Family
LEX(x,y) = ln(exp(x) − y) is incomplete over leaves {1, x}: for some elementary function f and compact interval K, LEX trees cannot approximate f uniformly on K.
Evidence: No proof. The domain calculation does not reach the conclusion. The right-nested self-composition lex(1, lex(1, … lex(x,1))) is defined on an interval that decreases to about (3.97×10⁻⁶, 2.782) and stays there, not to ∅; left-nested ln(e^x − n) is defined for x > ln n at every n; and lex(x, lex(lex(1,1),1)) = ln(e^x − ln(e − 2)) is defined on all of ℝ at depth 3. Restricted domains for some trees would not bound all trees in any case, and lex(x, c) = LEAd(x, −c) for any negative constant tree c. CORRECTION (2026-09-13): this card was a THEOREM stating that the valid domain shrinks to ∅ under self-composition, with lex(1, lex(x,1)) requiring x < ln(e^e+1) ≈ 2.81. That value is 2.782, and the domain does not shrink to ∅.
Depends on: T12.
T31 Complex EML Closure Density
CONJECTURE Depth Spectrum · Complex EML
Let K ⊂ ℂ be compact with connected complement. For every f holomorphic on a neighbourhood of K and every ε > 0, some finite EML tree T over leaves {1, z}, evaluated with the principal logarithm, is holomorphic on a neighbourhood of K and satisfies |f(z) − T(z)| < ε on K.
Evidence: No proof. Runge's theorem reduces the claim to representing polynomials on K by EML trees, and that step is not done. The explicit monomial tree EML(EML(EML(0,z), 1/n), 1) in Complex_Closure_Density.tex evaluates to n·exp(e/z), not z^n. The general case is left to T01 to "handle branch choices internally", but T01 says nothing about a tree agreeing with a polynomial at every point of K, and the principal logarithm is discontinuous on (−∞, 0]. Over leaves {1, z} the claim would put a constant tree within ε of every complex number (take K containing 1 and set z = 1), including i, which is C03, open. CORRECTION (2026-09-13): this card was a THEOREM whose evidence was "Runge's theorem + T01", and it marked C02 resolved. The polynomial step that argument needs has not been carried out. (An earlier correction, 2026-09-12, withdrew its claim that i is an accumulation point of EML₁.)
Depends on: T01.
T30 Depth Hierarchy: Standard Functions ≤ Depth 3 (superseded in part)
CONJECTURE Depth Spectrum; corrected 2026-08-19 · Depth Hierarchy
SUPERSEDED / REFUTED IN PART (2026-08-19). Two clauses of the original entry are false. (1) "algebraic functions have EML depth ≤ 3" — refuted by x + 1, which is algebraic and has d_(0,∞)(x + 1) = 4. (2) "Depth-4 exists but no standard function lives there" — refuted by the same witness. The other clauses are not proved (2026-09-13). exp, ln, and sin and cos over ℂ (with constant rescaling free) have explicit trees of at most 3 nodes, and exp^k has a k-node tree for every k, but that exp^k needs exactly k nodes is proved in MachLib only for k ≤ 4.
Evidence: Original evidence (2026-04-20), no longer accepted: S-T30 reported all 4 gaps closed, Lemma 4.2 repaired (R17), and a self-contained census in Depth_Spectrum_Self_Contained.tex. REFUTATION (2026-08-19): MachLib x_plus_one_not_depth_le_three excludes depth ≤ 3 on (0,∞); xPlusOneTree_depth gives the depth-4 construction; x_plus_one_depth_exact_four states both halves in one declaration. sorryAx absent. The defect was one-sided reasoning: an upper-bound census hardened into a universal claim with no matching lower bound, which is precisely what a two-sided rule prevents. CORRECTION (2026-09-13): the surviving clauses kept this card a THEOREM; it is a CONJECTURE. The lower-bound proof in Depth_Spectrum_Self_Contained.tex (growth-ceiling lemma, division case) bounds 1/g by applying the inductive hypothesis to 1/g itself and carries no lower bound as g → 0, and R17_T30_Hardy_Field_Verification.tex, the audit cited above, rated the argument a PROPOSITION with a false intermediate step. MachLib proves exp^k needs exactly k nodes for k ≤ 4 (tower_certified_upto_four) and records the general case as open. The census gives tan over ℂ as 1 node with no tree. No clause uses T14, which is no longer a dependency.
C01 i-Constructibility (Extended Grammar)
CONJECTURE S11+ · Complex EML
If the grammar is extended beyond strict principal-branch ceml (e.g., by allowing multi-valued log, or adding i as an explicit terminal), then i = √−1 becomes exactly constructible.
Evidence: T17 shows i is not constructible under strict semantics. Whether i is even an accumulation point of EML values is open (C03). Open: does any natural extension make i exactly reachable?
T39 Linear Ceiling Conjecture
CONJECTURE COST-9 / R14 · Cost Theory
No standard scientific formula has SuperBEST cost exceeding O(N) where N is the number of terms in any sum. Every textbook equation is either O(1) or O(N).
Evidence: Checked by hand on the April 2026 corpus: 187+ equations across 12 domains by Cost_Theory_Complete.tex's count (its 157-equation corpus plus the 30-equation R12 blind test). Nothing re-checks it. Only counterexample class: Hopfield energy (double sum, O(N²)). No single-sum standard formula in that corpus exceeds O(N).
Depends on: T40.
QCC Quadratic Ceiling Conjecture
CONJECTURE R14 · Cost Theory
For any N-parameter scientific model, SuperBEST cost is O(N²). No standard scientific formula exceeds O(N²) cost. Pairwise interaction models (Hopfield: 7N²) are the ceiling.
Evidence: No counterexample among the equations costed by hand in April 2026. Cost_Theory_Complete.tex checks its 157-equation corpus (the remark after T42-QCC); its cumulative count of 187+ equations adds the 30-equation R12 blind test. Nothing re-checks it. Supported by physical argument: standard textbook equations model at most pairwise interactions.
Depends on: T39.
CHA Chain-Order Additivity
CONJECTURE Filed 2026-04-27 · Analytic Properties
For any symbolic expression f, the Pfaffian chain order of f equals the sum of chain orders over the multiset of Pfaffian-not-elementary primitive AST occurrences in f, counted with multiplicity. Proof requires the Khovanskii zero-count theorem on Pfaffian chains, not yet in Mathlib — the same gap blocking T01's Part D. Two downstream corollaries are filed alongside it, both conditionally sorry'd on this conjecture closing first.
Evidence: 22 of 23 test cases (drawn from two independent exploration sessions) hit the predicted chain order exactly. The one exception, J₀(x) + Y₀(x) at Δ = +3, is consistent with the rule once AST-occurrence counting is applied correctly: Y₀ contains a J₀ component internally, so the explicit sum's AST counts J₀ twice.
C02 Complex EML Closure Density
CONJECTURE S35 · Complex EML
The functions computed by finite EML trees over leaves {1, z}, evaluated with the principal logarithm, are dense in H(K) for every compact K ⊂ ℂ with connected complement. Open.
Evidence: Stated in S35. The argument recorded as T31 is incomplete: its polynomial step is missing. CORRECTION (2026-09-13): this card was marked RESOLVED by T31.
C03 i as Accumulation Point
CONJECTURE S35 · Complex EML
Is i an accumulation point of EML₁: do EML trees of growing depth get arbitrarily close to i? Open.
Evidence: Depth-6 exhaustive search, re-run on 2026-09-13 (/blog/near-miss prints the script): the closest value is 8.07×10⁻⁸ + 0.99999523722i, with |w − i| = 4.7634634×10⁻⁶. A targeted depth-7 search finds a value whose imaginary part is within 7.9×10⁻¹² of 1, but it lies 1.32 from i. That bounds the approach at depth 6 (T17 records the same bound); it does not show the distance goes to 0. CORRECTION (2026-09-12): this card was marked RESOLVED by T31 and said depth-6 trees get arbitrarily close to i, but T31 recorded only this data.
OBSERVATION — 10 · Empirical pattern. No proof.
T15 Zero Counts of Small EML Trees
OBSERVATION Sprint2 · Analytic Properties
Among all 862,118 real EML trees over {1, x} with at most 8 internal nodes, the most sign changes found on [−2, 2] was 1, 0, 1, 2, 2, 2, 2, 3, 3 for 0 through 8 nodes.
Data: python/results/d2_tight_zeros.json, entry TZ5 (removed from the public repo in bec74da7; recoverable from its parent). The count uses a 0.01 grid on [−2, 2] with a ±0.05 dead band, so it misses zeros outside [−2, 2] and zeros where a tree only touches 0. No zero bound is proved; see T14. CORRECTION (2026-09-13): this card was a PROPOSITION, "Pumping Lemma for EML Trees", stating that depth-k trees have at most 2^k real zeros "(proved)" and that the observed maximum is O(k). The bound is not proved, and counts up to 8 nodes do not establish a growth rate.
Depends on: T14.
O-FOURIER Fourier Beats Taylor by 100× in Node Count
OBSERVATION S-CAL · Calculus Costs
sin(x) costs 101 nodes as an 8-term Taylor series under BEST routing. The same function is 1 complex EML node via Fourier/Euler. Factor-100 gap is purely structural.
Data: Taylor: 9N−3 = 69n for N=8, or 101n with full coefficient expansion. Complex path: Im(ceml(ix,1)) = 1 node.
O-LYAPUNOV Lyapunov Landscape 92.9% Correlated with Mandelbrot Interior
OBSERVATION S-CHAOS · Dynamical Properties
The Lyapunov exponent landscape of iterating eml(z, c) over a grid of c-values is 92.9% correlated (Pearson) with the Mandelbrot interior indicator.
Data: Numerical: 500×500 grid, 200 iterations each. Pearson r = 0.929. No analytic proof.
O-ATTRACTOR DEML and EMN Generate Bounded Strange Attractors
OBSERVATION S-CHAOS · Dynamical Properties
Iterating DEML and EMN in the complex plane generates bounded strange attractors with estimated box-counting dimension ≈ 1.128.
Data: Computational: 10,000-iteration orbits, box-counting dimension estimated from 50×50 to 800×800 grid scales.
O-NODOUBLING No Period-Doubling in the Exponential Family
OBSERVATION S-CHAOS · Dynamical Properties
The bifurcation diagram of eml(z, c) as c varies shows no classical period-doubling cascade. The exponential family transitions directly from fixed points to chaos.
Data: Bifurcation diagrams computed for 1,000 c-values. Consistent with known theory for exponential maps (Devaney, 1987).
O-GEOMETRY Geometry Catalog: 126n vs 345n Naive
OBSERVATION Sprint2 · Domain Costs
12 classical geometric primitives (hyperbolic distance, Lie group maps, curvature, conformal maps) measured as EML trees: 126n total vs 345n naive. 63% savings.
Data: Manual tree construction for each primitive. Savings measured vs naive EML without operator library.
O-TIMBRE Timbre = EML Node Count
OBSERVATION Sprint2 · Domain Costs
Each Fourier harmonic = one complex EML node. Timbre measurements: Sine = 1n, Clarinet ≈ 5n, Violin ≈ 12n. 245× fewer nodes than Taylor-based synthesis.
Data: Node count matches harmonic count for each instrument timbre.
O-157 295+-Equation Cost Catalog
OBSERVATION Monster Sprint + COMP-ALL + domain-2 · Domain Costs
295+ standard equations across 12+ domains measured under SuperBEST v3/v4. Floor: 1n (ratio laws). The ceiling this card gave, 2037n for Reed-Solomon syndrome computation, is withdrawn: that is GF(256) arithmetic, outside EML, and the count came from the false (α₀+3)N − 3 law. Original: 157 equations (Monster Sprint, 7 domains). Expanded: 214 (COMP-ALL), then 295+ (domain-2: FIN, INFO, QM, THERMO, CHEM, BIO, ECON sessions).
Data: Manual operator-tree analysis for each equation, cross-checked against master_equation_catalog.json, which holds 168 equations. Blind test: 27/30 exact (MAE = 0.20). CORRECTION (2026-09-13): the statement gave a 2037n Reed-Solomon ceiling; see /blog/cost-of-everything.
O-ISO 8 Cross-Domain Isomorphisms
OBSERVATION R10 · Domain Costs
8 families of equations from different scientific domains share identical SuperBEST trees differing only in terminal labels (the best constructions found; that they are minimal is not shown): (1) exponential growth/decay, (2) NPV = N-compartment PK, (3) softmax = logit, (4) van't Hoff = Clausius-Clapeyron, (5) 1−exp(−t/τ) family, (6) simple ratio laws, (7) linear transport laws, (8) entropy p·ln(p) scaling.
Data: Explicit bijections between operator trees for each pair. Source: R10_Isomorphism_Theorem.tex.
O-CLASS Four Structural Classes of Scientific Formulas
OBSERVATION COST-4 / R9 · Cost Theory
Scientific equations fall into 4 structural classes: A (pure exponential, 5-12n), B (rational/polynomial), C (log-ratio, cheapest by mean), D (mixed exp+ln, most expensive). Cost ordering: mean(C) < mean(B) < mean(A) < mean(D).
Data: Verified on 50-equation chembio catalog: overall MAE = 1.80. Class B MAE = 1.11, Class C MAE = 0.85.
DEFINITION — 6 · A new concept or classification choice.
T38 Cost Decomposition (a definition, not a theorem)
DEFINITION COST-6 / R2 · Cost Theory
NaiveCost(E) − Cost(E) is split into SharingDiscount(E), the saving from constant folding and repeated subexpressions, and PatternBonus(E), the rest. Cost(E) = NaiveCost(E) − SharingDiscount(E) − PatternBonus(E) then holds because PatternBonus is defined as that remainder; it is not a formula for Cost.
Note: R2_Decomposition_Theorem.tex §2 and COST6_Decomposition_Theorem.tex §4 claim the identity with PatternBonus computed from a fixed pattern catalogue. Their minimality step asserts, without proof, that no other kind of reduction exists, and Cost_Theory_Complete.tex lists completeness of the pattern set as an open problem. CORRECTION (2026-09-13): this card was a THEOREM. With a catalogue PatternBonus the identity is false: e^{x₁} + e^{x₂} has SharingDiscount 0, matches no catalogued pattern and has naive cost 4, but costs at most 3 (EML(LEAd(x₂, EML(x₁,1)), 1)). The uniqueness claim rested on the same step and is dropped.
Depends on: T34.
P-SD Sharing Discount (a count, not a theorem)
DEFINITION COST-5 / R4 · Cost Theory
SharingDiscount(E), the part of NaiveCost(E) − Cost(E) credited to constant folding and repeated subexpressions, is counted as Σᵢ NC(Fᵢ) + Σⱼ Cost(Sⱼ)(mⱼ − 1), over the maximal pure-constant subexpressions Fᵢ and the maximal repeated live subexpressions Sⱼ with multiplicities mⱼ. An expression with neither has SharingDiscount 0.
Note: R4_Sharing_Discount.tex §2. Its catalog check applies the count to the 50 ChemBio equations: 30 have no folding or repeats (count 0) and 20 have a positive count, 3 of them from repeated live subexpressions. CORRECTION (2026-09-13): this card was a PROPOSITION saying the formula is proved and that 47 of 50 equations have SD = 0, the other 3 by constant folding only. R4 defines SD as NaiveCost − Cost, and under that definition the formula is false: e^{x₁} + e^{x₂} has no folding and no repeats, so the formula gives 0, yet its naive cost is 4 and it costs at most 3. As the folding-and-sharing part of the T38 split it is a definition. The 47/50 figure contradicted R4, which reports 30 and 20.
Depends on: T38.
D01 EML Depth Hierarchy
DEFINITION S19 · Depth Hierarchy
EML-k = {f : ℂ → ℂ | f = eval(t) for some EML tree t with depth ≤ k}. EML-0 = constants. EML-∞ = functions not in any EML-k for finite k. Hierarchy: EML-0 ⊆ EML-1 ⊆ EML-2 ⊆ EML-3 ⊆ EML-∞.
Note: Definitional. EML-0 ⊊ EML-1 is proved in Lean (exp_not_constant, T_EULER_LEAN). That every inclusion is strict is T30, a conjecture; MachLib proves the first four levels distinct (tower_certified_upto_four).
D02 SuperBEST Cost Function
DEFINITION R1 · Cost Theory
Cost_F(E) = minimum number of internal nodes in any DAG over operator family F computing E. NaiveCost(E) = Σ cᵢ·nᵢ using SuperBEST v3 unit costs: exp=1, ln=1, neg=2, recip=2, mul=2, sub=2, div=1, pow=3, add=3 (pos) / 11 (gen). These are the April v3 unit costs: several are not minimal (see /superbest), and add is 2 for all real inputs (ADD-T1).
Note: Defined in R1_Cost_Definition.tex §1. R1 §2 proves non-negativity (P1), subadditivity Cost(op(A,B)) ≤ Cost(A) + Cost(B) + 1 (P3), and invariance under equality of functions (P4). CORRECTION (2026-09-13): this card said R1 proves four properties. The fourth, P2 (Cost(E) = 0 iff E is a terminal), is false as stated: LEdiv(x, 1) = x is not a terminal but costs 0; the true form is "Cost(E) = 0 iff E computes the same function as a terminal". R1's Lean section is type signatures with sorry, not proofs.
D03 Complex EML (ceml)
DEFINITION S11 · Complex EML
ceml(z₁, z₂) = exp(z₁) − Log(z₂), where Log is the principal branch complex logarithm. The complex extension of eml.
Note: Definitional. Euler Gateway (ceml(ix,1) = exp(ix)) follows immediately.
D04 Tropical EML (teml)
DEFINITION S9 · Tropical EML
teml(a, b) = max(Re(a), −Re(b)) + i(Im(a) + Im(b)). The tropical analog of ceml in the (max, +) semiring. teml(a,a) = |a|.
Note: Definitional. teml(a,a) = max(a,−a) = |a| for real a.
SPECULATION — 2 · Interesting but not currently testable or provable.
S01 P = EML-2, NP = EML-∞
SPECULATION Internal · Depth Hierarchy
The analogy that P corresponds to EML-2 and NP to EML-∞. An interesting metaphor, not a formal statement.
Note: No evidence.
S02 NS Regularity is ZFC-Independent
SPECULATION S1220–S1237 · Connections to Existing Mathematics
Claim that Navier-Stokes global regularity is formally ZFC-independent via EML-theoretic analysis. The jump to ZFC-independence is not established.
Note: No complete proof. Speculative.