Best known F16-node constructions for every elementary arithmetic primitive. Every count is an upper bound; none is shown to be minimal. Taxonomy: 23 operators. CONJ_NO_OP_24, that no 24th operator passes the PGC+AIT filter on an open domain, is a conjecture: the monogate repository's exploration notes argue it by case analysis and a filter pass over the remaining candidate operators, and no Lean proof exists.
Which F16. The core table counts nodes in the sixteen operators on monogate.org/framework ↗ and nothing else, since monogate.org recounted it on 2026-09-13. ln x takes 2 nodes there, LEdiv(0, F13(−1, x)), so the positive-domain total is 15n / 79.5%. Counting ln x = EXL(0, x) as one node instead, with the census operator EXL, exp(x)·ln y, gives 14n / 80.8%. Both totals are upper bounds. Each construction is evaluated numerically on its domain by the monogate repository's python/tests/test_superbest_f16_constructions.py, which this site does not run, and this site gates no Lean theorem that states either total. Before each deploy the totals are compared with python/monogate/superbest.py, and every node count in the table with monogate.org's copy. The high-impact tables below follow the taxonomy-lock paper, whose "F16 orbit" is a different sixteen that leaves out LEAd (F11 on /framework).
General domain. The general basket is exp, neg, add, sub, mul and div, each with one F16 tree valid for every real input where the operation is defined (div needs y ≠ 0). mul takes 3 nodes, LEdiv(0, F13(y, DEML(x, 1))), and div takes 8. A numerical search over F16 trees with constant leaves 0, 1, −1, 2 and 1/2 finds no smaller signed division (python/benchmarks/superbest_f16/search.pyin the monogate repository); a search is not a proof. Before the recount, mul and div counted sign-dispatch case splits, one circuit per sign quadrant, not trees. Two operations left the basket: abs, because no real F16 tree computes |x| (every tree is real-analytic where it is defined, and |x| is not analytic at 0; a paper argument, not a Lean proof), and ln, which has no real value for x ≤ 0. recip has a row-level entry for x ≠ 0; sqrt and pow have none over all reals. The naive costs are the monogate library's pure-EML figures, not re-derived in the recount.
| Operation | Nodes (x>0) | v4 cost | Construction | Notes |
|---|---|---|---|---|
exp(x) | 1n | 1 | EML(x,1) = e^x | primitive — no domain restriction |
ln(x) | 2n | 1 | LEdiv(0, F13(-1,x)) = 0 - ln(x^-1) = ln(x), x > 0 | No single F16 node equals ln x (a search over one-node trees finds none). EXL(0,x) = ln(x) in one node, but EXL is a census operator outside F16; the count with EXL on this page uses it. |
recip(x) = 1/x | 1n | 1 | F13(-1,x) = exp(-ln(x)) = 1/x, x > 0 | R16-C1's ELSb(0,x) is the same function at the same count for x > 0 (ELSb is a census operator). The general entry is row-level; recip is not in the general basket. |
div(x,y) = x/y | 2n | 2 | F16fn(x, F13(-1,y)) = exp(ln(x) + ln(1/y)) = x/y, x > 0, y > 0 | Recounted in F16 on 2026-09-13: one tree for every x and y != 0. The earlier general entry counted a sign-dispatch case split. |
neg(x) = -x | 2n | 2 | LEdiv(0, EML(x,1)) = 0 - ln(exp(x)) = -x; EML(x,1) = exp(x) > 0, so LEdiv is always valid | T09 wrote the same count with the census operator EXL, as EXL(0, DEML(x,1)). No single F16 node computes -x (search over one-node trees). |
mul(x,y) = x*y | 1n | 2 | F16fn(x, y) = exp(ln(x) + ln(y)) = x*y for x, y > 0 | One tree over all reals since the F16 recount of 2026-09-13. |
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 | F13(0.5, x) = exp(0.5·ln(x)) = sqrt(x), x > 0 — single F16 node (EPL(0.5, x) in the census) | T_SQRT_1N; EPL(0.5,x) = ELMl direct primitive. Same mechanism as pow=1n. Corrected from v5.1 (was 2n). Spot values: 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 | F13(n, x) = exp(n·ln(x)) = x^n, x > 0 — single F16 node (EPL/ELMl in the 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; with no F16 shortcut, the saving exists only in the 23-op count. Node counts here and in the high-impact tables are from the SuperBEST taxonomy lock of 2026-04-21. Nothing on this site re-derives them; before each deploy they are compared cell by cell with the copy monogate.org shows.
| 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 |
| Catalog | Layer 1 — F16 genuine | Layer 2 — 23-op extended |
|---|---|---|
| Core arithmetic (10 ops, positive domain) | 79.5% | 80.8% |
| ML functions (5 items) | 35% | 62% |
| Quantum (8 items) | 19% | 44% |
| Physics (5 items) | 29% | 40% |
| Special functions | 0% (all inf) | 0% (all inf) |
| Aggregate | ~12% | ~40% |
The core-arithmetic row's Layer 1 cell is the positive-domain F16 headline; its Layer 2 cell counts ln x = EXL(0, x) as one node, as monogate.org's does. Both are computed from totals that are checked against the monogate.superbest library before each deploy. The ML, quantum and physics rows are pooled over the SuperBEST taxonomy lock's own item rows, as monogate.org recomputed them on 2026-09-13 (they were rounded estimates before); the aggregate row is still the paper's rounded estimate, dated 2026-04-21. Nothing on this site re-derives them. Before each deploy they are compared with the copy monogate.org shows, so a change there fails the next deploy until this table matches.
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 | 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 ↗