Theorem Catalog

THEOREM

External (Odrzywołek 2026) · Core Algebra

eml(x, y) = exp(x) − ln(y) generates every elementary function as a finite binary tree. Published arXiv:2603.21852.

Proof: Published, peer-reviewable proof. Constructs explicit trees for each elementary function using the Log Recovery identity and composition rules.

THEOREM

Sprint2 · Core Algebra

neg(x) = −x is computable in exactly 2 EML-family nodes: exl(0, deml(x,1)) = −x. Optimal; 1 node is impossible by exhaustive search.

Proof: Exhaustive search over all 1-node candidates finds no neg construction. Upper bound: explicit 2-node construction verified.

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))"

THEOREM

Depth Spectrum · Core Algebra

In the 16-operator family F16, mul(x,y) = ELAd(EXL(0,x), y) = x·y in exactly 2 nodes. This is optimal in F16. In the 6-operator F6 library, 3 nodes are required (T29).

Proof: Exhaustive search found exactly 4 matching 2-node trees in F16. Source: python/scripts/mul_lower_bound_search.py.

Depends on: T29.

THEOREM

Sprint2 · Analytic Properties

For all x > 0: eml(x,x) = exp(x) − ln(x) > x. The map x ↦ eml(x,x) has no fixed points. Minimum gap: eml(x,x) − x ≥ 1.648629... at x ≈ 1.7632.

Proof: Calculus: d/dx[exp(x)−ln(x)−x]=0 at x≈1.7632. Numerical minimum confirmed to 6 decimal places.

THEOREM

COMP-1 through COMP-5 · Operator Family

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.

Proof: Forward direction (T26): exp(+x) → complete. Reverse (T27): exp(−x) → incomplete by 5 distinct barrier types. LEX (T28): domain collapse.

Depends on: T09, T26, T27, T28, T24.

THEOREM

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. The self-composition slope is locked to +1; no DEML tree achieves slope −1.

Proof: Exhaustive search over 861,952 trees at N ≤ 13 finds no neg construction. Structural proof: slope locked to +1.

Depends on: T12.

THEOREM

Sprint2 · Analytic Properties

A depth-k EML tree has at most 2^k real zeros. This bound is tight: explicit constructions achieve it.

Proof: Structural induction: each EML node combines two sub-trees, at most doubling the zero count. Tightness: explicit constructions at each depth.

THEOREM

Sprint2 · Complex EML

Under strict principal-branch semantics, i = √−1 is not constructible from {1} using the ceml grammar in finite depth. At depth 6, the closest approach is |T − i| ≥ 4.76×10⁻⁶.

Proof: Lean 4 verification: complete inductive proof, 0 sorries. Depth-6 exhaustive search: minimum distance 4.76×10⁻⁶.

THEOREM

Sprint2 · Operator Family

emn(x,y) = ln(y) − exp(x) is approximately complete: for every elementary function f and ε > 0, there exists a finite EMN tree with sup-norm error < ε on any compact set. EMN is not exactly complete: the residual exp(·) error converges doubly-exponentially but never reaches 0.

Proof: Approximate completeness: −exp(x) unbounded gives full range access. Not exact: irremovable exp(·) residual.

Depends on: T12.

THEOREM

COMP-2 · Operator Family

Let O(x,y) = h(exp(x), ln y) where h does not impose a domain restriction preventing O from taking all real values. Then O is exactly complete.

Proof: (1) O(x,1) = exp(x). (2) O(c, exp(x)) achieves slope −1. (3) Cross-family bridge gives exact neg in ≤ 2 nodes. (4) With neg, exp, ln: all elementary functions by Ritt's theorem. Verified for all 8 complete operators.

Depends on: T09, T12.

THEOREM

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.

Proof: DEML: slope barrier (+1). DEMN: domain failure (outputs always negative). DEAL: irremovable e⁻¹ offset. DEXL: dead constant at c=1. DEDL/DEPL: exponential decay. All verified computationally.

Depends on: T12, T13.

THEOREM

COMP-3 · Operator Family

LEX(x,y) = ln(exp(x) − y) is incomplete despite having exp(+x). At self-composition depth n, the valid input domain shrinks to ∅.

Proof: Domain calculation: lex(1, lex(x,1)) requires x < ln(eᵉ+1) ≈ 2.81. Domain strictly shrinks at each level. Verified computationally.

Depends on: T12.

THEOREM

Depth Spectrum · Core Algebra

No 1-node or 2-node tree over the 6-operator library F6 = {EML, EDL, EXL, EAL, EMN, DEML} computes mul(x,y) = x·y exactly. Minimum in F6 is 3 nodes.

Proof: Exhaustive search over all 96 candidate 1-node trees and all 12,288 candidate 2-node mixed trees at 8 test points: no match found.

THEOREM

Depth Spectrum · Complex EML

EML trees (with complex inputs) are dense in H(K), the space of holomorphic functions on any compact simply-connected K ⊂ ℂ. Additionally, i is an accumulation point of EML₁.

Proof: Density: Runge's theorem + T01. Accumulation: depth-6 exhaustive data — closest depth-6 value to i has |w − i| = 4.76×10⁻⁶. Resolves C02 and C03.

Depends on: T01, T17.

THEOREM

DOOR-1 · Core Algebra

In any 1-operator family F where the operator has the form h(exp(±x), ln(y)), multiplication x·y requires at least 2 nodes. A single operator node cannot compute mul.

Proof: Derivative obstruction: ∂op/∂x always contains an exp(x) factor, which cannot equal y for all (x,y). Verified for all 16 operators in F16 with 0 sorries in Lean.

Depends on: T29, T10u.

THEOREM

COST-2 · Cost Theory

For any expression E: Cost(E) ≤ NaiveCost(E) = Σ cᵢ · nᵢ where cᵢ is the SuperBEST v3 per-operation cost and nᵢ is the count of operation i in E. The bound is tight iff there are no shared subtrees, no compound patterns, and no constant folding.

Proof: Proof by construction: the naive expansion is a valid DAG. Minimality reduces it. Tightness conditions enumerated in R1_Cost_Definition.tex.

Depends on: T38.

THEOREM

COST-6 / R2 · Cost Theory

For any expression E: Cost(E) = NaiveCost(E) − SharingDiscount(E) − PatternBonus(E). All three terms are non-negative. The decomposition is unique for a fixed pattern set and canonical sharing strategy.

Proof: Proved in R2_Decomposition_Theorem.tex. SharingDiscount ≥ 0: merging shared nodes cannot increase cost. PatternBonus ≥ 0: each compound pattern replaces more-expensive naive subtrees. Uniqueness: canonical sharing + greedy pattern matching.

Depends on: T34.

THEOREM

Lean Sprint 2026-04-21 · Core Algebra

No single F16 operator 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.

THEOREM

Lean Sprint 2026-04-21 · Core Algebra

No single F16 operator 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.

THEOREM

Lean Sprint 2026-04-21 · Core Algebra

No single F16 operator computes x/y for all real x, y. Positive domain: exp(ln x − ln y) is 1 node. General domain: ≥ 2 nodes (Lean-verified).

Proof: Lean 4, 0 sorries. Witness (0,1) for each of 16 F16 operators.

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). SuperBEST v5.3 positive total: 14n (savings 80.8%).

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.

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.

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 and C (EML trees have finitely many zeros) remain open in Lean.

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).

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 v4.14.0. 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.

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/cos/tan, which do NOT preserve ELC (T01). 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 v4.14.0; numerical 3-4-5 witnesses via norm_num at ln 2.

THEOREM

Sprint2 / Sprint3 / S-T08 · Core Algebra

SuperBEST v4: 19 nodes total, all 9 entries structurally proved optimal. recip=1n (ELSb(0,x)=1/x), div=2n (ELSb(ln(x),y) — corrected from erroneous 1n entry), sub=2n (T33), mul=2n (T10u/F16), neg=2n (T09), add=3n (cross-derivative lower bound), pow=3n (3-intermediate lower bound), sqrt=2n (derivative obstruction), exp=1n, ln=1n.

Proof: S-T08 full structural audit (2026-04-20): every entry has a structural proof — no entry relies solely on exhaustive search. SuperBEST_v4_Structural_Audit.tex.

Depends on: T09, T10u, T12, T32, T33, R16-C1.

THEOREM

Depth Spectrum · Depth Hierarchy

All standard elementary functions (exp, ln, algebraic, trig via ℂ) have EML depth ≤ 3. The hierarchy is strictly infinite (exp^k requires exactly k nodes). Depth-4 exists but no standard function lives there.

Proof: S-T30 (2026-04-20): all 4 gaps closed. Hardy field Lemma 4.2 repaired (R17). Self-contained depth census in Depth_Spectrum_Self_Contained.tex — no external citations. GAP-4 (division case) closed via Hardy field total ordering. Correction: sinh/cosh are depth 3 (not 2 as previously claimed). T30(c) holds — all standard functions ≤ depth 3.

Depends on: T14.

THEOREM

COST-3 · Cost Theory

Three structural lower bounds on Cost(E): (T35) Cost(E) ≥ |O(E)| — each non-mergeable operator requires a distinct node, by F16 structure. (T36) Cost(E) ≥ d where d = distinct necessary intermediates — binary-tree counting identity. (T37) Cost(E) ≥ n_exp + n_ln — exp-nodes and ln-nodes are disjoint, each requiring a dedicated node.

Proof: R18 audit confirmed all three are structural arguments appealing to F16 operator structure, not just definitional unwrapping. Each proof is 2-4 lines. Weak theorems are still theorems.

Depends on: T38.

THEOREM

COST-9 / R5 · Cost Theory

For N-term positive-domain summations: Cost(E_N) = (α₀ + 3)·N − 3 exactly, where α₀ is the per-term cost. Softmax: 4N−3. Shannon entropy: 6N−3. Taylor: 8N−3. The positive-domain assumption is genuine: licenses c_add=3 instead of 11, saving 8n per node.

Proof: R18 audit confirmed induction proof is gap-free. Base N=1: Cost=α₀ (T38 with SD=PB=0). Step: new term costs α₀ (independent, T38) + 1 EAL node (cost 3, T40-DF) = α₀+3. Exact equality by T38. Proved in R5_Linear_Cost_Law.tex.

Depends on: T38, T34.

PROPOSITION

Sprint2 · Analytic Properties

Depth-k EML trees have at most 2^k real zeros (proved). Observed computational maximum is O(k), suggesting the bound is far from tight.

Proof: Upper bound: T14. Gap between 2^k and observed O(k) is unproved.

Depends on: T14.

PROPOSITION

Sprint2 · Operator Family

EXL(x,y) = exp(x)·ln(y) achieves ln(x) in 1 node: EXL(0,x) = ln(x). Combined with T10u, EXL gives the cheapest logarithm and fastest multiplication route in F16.

Proof: Direct computation: EXL(0,x) = 1·ln(x) = ln(x). Route to mul: ELAd(EXL(0,x), y) = x·y in 2 nodes.

PROPOSITION

Sprint2 · Complex EML

At depth 5, all complex EML values computed from input 1 have imaginary part Im = −π exactly. At depth 6, imaginary parts escape this constraint and become dense.

Proof: Exhaustive computation of all depth-5 and depth-6 trees rooted at 1. At depth 5: Im ∈ {−π} (verified). At depth 6: Im values spread across ℝ.

Depends on: T31.

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). Nested operators pay exactly the sum of individual costs.

Proof: Upper bound: explicit DAG construction. Lower bound: O₂ sub-DAG, O₁ node, and C sub-DAG are pairwise disjoint in any minimal DAG.

Depends on: T38.

PROPOSITION

R6 · Cost Theory

For independent expressions E₁, E₂: Cost(op(E₁,E₂)) = Cost(E₁) + Cost(E₂) + 1. Explains Lorentz force (57n) and Black-Scholes (47n).

Proof: Upper bound: disjoint optimal DAGs + one root node. Lower bound: root op and independent sub-DAGs are disjoint. Proved in R6_Additive_Cost_Law.tex.

Depends on: T38.

PROPOSITION

COST-5 / R4 · Cost Theory

SharingDiscount(E) = Σᵢ NC(Fᵢ) + Σⱼ Cost(Sⱼ)(mⱼ − 1). For single-formula expressions over distinct variables: SharingDiscount = 0. 47/50 chembio equations have SD = 0.

Proof: 47/50 chembio equations verified. The 3 exceptions have constant-folding only. Proved in R4_Sharing_Discount.tex.

Depends on: T38.

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. T31 shows i is an accumulation point. Open: does any natural extension make i exactly reachable?

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: Verified on 187+ equations across 12 domains. Only counterexample class: Hopfield energy (double sum, O(N²)). No single-sum standard formula exceeds O(N).

Depends on: T40.

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: Verified on 187+ equations. No known counterexample. Supported by physical argument: standard textbook equations model at most pairwise interactions.

Depends on: T39.

CONJECTURE

S35 · Complex EML

RESOLVED — The set of functions representable by finite ceml trees over ℂ is dense in H(K) for any compact K. Stated as a conjecture; proved as T31.

Evidence: Resolved by T31. Runge's theorem + T01 give density in H(K).

CONJECTURE

S35 · Complex EML

RESOLVED — i is an accumulation point of EML₁: depth-6 EML trees get arbitrarily close to i. Proved as part of T31.

Evidence: Resolved by T31. Depth-6 exhaustive search: closest value |w − i| = 4.76×10⁻⁶.

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.

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.

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.

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).

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.

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.

OBSERVATION

Monster Sprint + COMP-ALL + domain-2 · Domain Costs

295+ standard equations across 12+ domains measured under SuperBEST v3/v4. Floor: 1n (ratio laws). Ceiling: 2037n (Reed-Solomon). 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. Blind test: 27/30 exact (MAE = 0.20).

OBSERVATION

R10 · Domain Costs

8 families of equations from different scientific domains share identical minimal SuperBEST trees differing only in terminal labels: (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.

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

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. Strict inclusions EML-0 ⊊ EML-1 proved. T30 establishes the strict infinite hierarchy.

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).

Note: Formally defined in R1_Cost_Definition.tex with 4 proved properties: non-negativity, terminal characterization, subadditivity, algebraic invariance.

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.

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

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.

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.