Minimum F16-node constructions for every elementary arithmetic primitive. Taxonomy definitively closed: PROVED — no 24th operator passes PGC+AIT filter on open domain.
| Operation | Nodes (x>0) | Naive | Construction | Notes |
|---|---|---|---|---|
exp(x) | 1n | 1 | EML(x,1) = e^x | primitive — no domain restriction |
ln(x) | 1n | 1 | EXL(0,x) = ln(x), x > 0 | primitive; domain-restricted to x > 0 |
recip(x) = 1/x | 1n | 1 | ELSb(0,x) = exp(0 - ln(x)) = 1/x, x > 0 | R16-C1; X8 audit confirms negative x also handled in implementation |
div(x,y) = x/y | 2n | 2 | EXL(0,x) then ELSb(ln(x), y) = x/y, x > 0, y > 0 | v5.3 canonical sync: div_positive=2n full tree; div_general=3n. |
neg(x) = -x | 2n | 2 | EXL(0, DEML(x,1)) = ln(exp(-x)) = -x; or DEML(x,1)=exp(-x) then EXL gives -x | T09; 2n for all reals; positive domain gives no cost improvement |
mul(x,y) = x*y | 1n | 2 | ELMl(ln(x), y) = exp(ln(x) + ln(y)) = x*y for x,y > 0 | v5.3 canonical sync: mul_positive=1n; mul_general=3n. |
sub(x,y) = x - y | 2n | 2 | LEdiv(x, EML(y,1)) = ln(exp(x)/exp(y)) = x - y | T33; 2n for all reals; X8 confirmed |
add(x,y) = x + y | 2n | — | LEdiv(x, DEML(y,1)) = ln(exp(x)/exp(-y)) = x + y | NEW v5 (ADD-T1): all real x,y. Replaced add_pos=3n and add_gen=11n with unified 2n. |
sqrt(x) = x^(1/2) | 1n | 2 | EPL(0.5, x) = ELMl(0.5, x) = exp(0.5·ln(x)) = sqrt(x), x > 0 — single F16 node | T_SQRT_1N; EPL(0.5,x) = ELMl direct primitive. Same mechanism as pow=1n. Corrected from v5.1 (was 2n). Verified: EPL(0.5,4)=2.0, EPL(0.5,9)=3.0, EPL(0.5,16)=4.0. |
pow(x,n) = x^n | 1n | 3 | EPL(n,x) = ELMl(n,x) = exp(n * ln(x)) = x^n, x > 0 — single 1-node F16 operator from the 16-operator census | X20 RESOLUTION: EPL/ELMl = exp(x*ln(y)) = y^x IS in F16 census. pow(x,n)=x^n=EPL(n,x) for x>0 costs 1n (direct), not 3n. The 3n construction used EXL+ELAd+EML explicitly rather than recognizing EPL as a primitive. For positive domain: corrected to 1n. |
Cat A: genuine F16 algebraic shortcut. Cat B: genuine via EML sign-variant. Cat C: notation-only (23-op=1n; F16=3–4n; no F16 shortcut).
| Op | F16 cost (L1) | 23-op cost (L2) | Genuine saving | Category | Description |
|---|---|---|---|---|---|
EEM | 3n | 1n | 1 | A | Algebraic shortcut (add+exp) |
EED | 3n | 1n | 1 | A | Algebraic shortcut (sub+exp) |
EES | 1n/4n | 1n | 3n(const)/0n(gen) | B/C | Genuine F16 for const arg; notation-only general |
LLA | 3n | 1n | 1 | A | Algebraic shortcut (mul+ln) |
LLS | 3n | 1n | 1 | A | Algebraic shortcut (div+ln) |
LLD | 4n | 1n | 0 | C | Notation-only — no F16 shortcut |
EEA | 4n | 1n | 0 | C | Notation-only — enables LSE=2n in 23-op |
Layer 1 = F16 ground-truth; Layer 2 = 23-op extended (must be labeled)
| Expression | Naive | F16 (Layer 1) | 23-op (Layer 2) | Saving type |
|---|---|---|---|---|
softplus ln(1+exp(x)) | 4n | 2n | 2n | B: EML(x,1/e)+ln |
LSE(x,y) = ln(exp(x)+exp(y)) | 8n | 4n | 2n | F16: exp+exp+add+ln (corrected from 5n) |
sigmoid 1/(1+exp(-x)) | 6n | 4n | 3n | F16 route |
KL term l*ln(l/m) | 6n | 5n | 3n | A: div+ln+mul |
| Expression | Naive | F16 (Layer 1) | 23-op (Layer 2) | Saving type |
|---|---|---|---|---|
quantum rel entropy (per term) | 6n | 5n | 3n | A: genuine 1n save |
von Neumann entropy (per term) | 8n | 7n | 4n | A: 1n save |
Bures distance | 5n | 4n | 3n | B: genuine |
partition fn pair exp(-bEj)/exp(-bEi) | 10n | 10n | 7n | C: EEA notation-only |
spectral decay exp(-g*t) | 4n | 3n | 2n | A: mul+exp |
Kraus factor sqrt(1-exp(-g*t)) | 6n | 4n | 3n | B: EML-variant+EPL |
| Expression | Naive | F16 (Layer 1) | 23-op (Layer 2) | Saving type |
|---|---|---|---|---|
Boltzmann ratio exp(-b*(Ej-Ei)) | 10n | 6n | 5n | A: sub+mul+neg+exp |
Mayer f-function exp(-b*u)-1 | 6n | 3n | 3n | B: EML_neg+mul |
hydrogen radial decay | 4n | 3n | 3n | B: genuine |
Fermi-Dirac 1/(exp((e-m)/kT)+1) | 8n | 6n | 4n | A: algebraic route |
| Function | F16 / 23-op cost | Reason |
|---|---|---|
erf(x) | ∞ | T01: infinite zeros |
J_0(x) Bessel | ∞ | T01: infinite zeros |
Gamma(x) | ∞ | AIL theorem |
sin(x), cos(x) | ∞ | T01/AIL: proved |
| Catalog | Layer 1 — F16 genuine | Layer 2 — 23-op extended |
|---|---|---|
| Core arithmetic (9 ops) | 80.8% | 80.8% |
| ML functions (6 items) | ~35% | ~55% |
| Quantum (8 items) | ~15% | ~35% |
| Physics (5 items) | ~30% | ~45% |
| Special functions | 0% (all inf) | 0% (all inf) |
| Aggregate | ~12% | ~40% |
The cost theory's named results, mechanised in MachLib/CostTheory.lean ↗ — pure Nat, #print axioms shows only propext / Quot.sound, no sorryAx, no MachLib field axioms. Status is honest: the empirical mean-cost ordering (C < B < A < D) and the T42-QCC conjecture are not claimed as proven.
| Result | Statement | Lean theorem | Status |
|---|---|---|---|
T38-NNP | No-Nesting Penalty — composing operators is additive, no adapter/depth overhead | no_nesting_penalty | machine-checked |
T38 | Cost = Naive − Pattern − Sharing — the two savings account for exactly the naive/actual gap | t38_decomposition | machine-checked |
T40 | Additive Cost Law — independent branches sum exactly; sums are association-independent | additive_cost_law · sum_assoc_invariant | machine-checked |
T41-ISO | Cross-domain cost invariance — isomorphic DAG topologies cost the same (the 8 families' principle) | iso_cost | machine-checked |
T42 | O(N) single-sum law — N equal-cost terms cost (α₀+3)·N − 3 | cost_flatSum | machine-checked |
T42² | O(N²) double-sum law — a nested N×N sum is an exact quadratic | cost_doubleSum | machine-checked |
P1–P3 | Basic properties — non-negativity, terminal characterisation, subadditivity | p1_nonneg · p2_*_cost_ge · p3_subadditive_* | machine-checked |
T41 | Four structural classes — classification well-defined; rational is the cost floor, mixed the ceiling | classify · rational_floor · mixed_ceiling | structural core |
P4 | Algebraic invariance — cost as a function of the computed FUNCTION, not the tree | — | out of scope |
T42-QCC | Quadratic Ceiling Conjecture — no closed form exceeds O(N²); empirical over 187 equations | — | conjecture |
Research: monogate.org/superbest ↗ · Explorer: monogate.dev/explorer