Theorem Catalog
Every result is labeled for what it actually is. Proved facts are theorems. Everything else is clearly marked.
29 theorems · 6 propositions · 3 open conjectures · 9 observations
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 — 29 · Complete, checkable proof. No gaps.
T01 EML Universality
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.
T09 Negation in 2 Nodes — Optimal LEAN ✓
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))"
T10u Multiplication in 2 Nodes — F16 Optimal
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.
T11 EML Self-Map Has No Fixed Points
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.
T12 Exponential Position Theorem
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.
T13 DEML Incompleteness
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.
T14 Tight Zeros Bound
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.
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. 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⁻⁶.
T24 EMN Approximate Completeness
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.
T26 Forward Completeness: exp(+x) → Exactly Complete
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.
T27 Reverse Incompleteness: exp(−x) → Incomplete
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.
T28 LEX Domain Incompleteness
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.
T29 Mul ≥ 3 Nodes in F6
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.
T31 Complex EML Closure Density
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.
T32 Mul ≥ 2 Nodes in Any exp-ln Family LEAN ✓
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.
T34 Naive Upper Bound
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.
T38 Cost Decomposition Theorem
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.
ADD-T1 Addition ≥ 2 Nodes — Lean Lower Bound LEAN ✓
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.
T33 Subtraction ≥ 2 Nodes — Lean Lower Bound LEAN ✓
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.
T_DIV_GEN_LB Division ≥ 2 Nodes (General Domain) — Lean LEAN ✓
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.
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). 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.
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 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).
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 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.
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/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.
T08 SuperBEST Table v4 — 19 Nodes, All Entries Structurally Proved
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.
T30 Depth Hierarchy: Standard Functions ≤ Depth 3
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.
T35 Lower Bound Theorems (Structural)
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.
T40 Linear Cost Law
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 — 6 · Proved, short or routine.
T15 Pumping Lemma for EML Trees
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.
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). 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.
T25 Depth-6 Phase Transition
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.
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). 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.
P-ACL Additive Cost Law
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.
P-SD Sharing Discount Formula
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 — 5 · Precisely stated, believed true, unproved.
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. T31 shows i is an accumulation point. 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: 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.
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: Verified on 187+ equations. No known counterexample. Supported by physical argument: standard textbook equations model at most pairwise interactions.
Depends on: T39.
C02 Complex EML Closure Density
RESOLVED → T31
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).
C03 i as Accumulation Point
RESOLVED → T31
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 — 9 · Empirical pattern. No proof.
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). 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).
O-ISO 8 Cross-Domain Isomorphisms
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.
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 — 4 · A new concept or classification choice.
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. Strict inclusions EML-0 ⊊ EML-1 proved. T30 establishes the strict infinite hierarchy.
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).
Note: Formally defined in R1_Cost_Definition.tex with 4 proved properties: non-negativity, terminal characterization, subadditivity, algebraic invariance.
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.