SuperBEST Routing Table

Best known constructions, in F16 nodes, for every elementary arithmetic primitive. Upper bounds are explicit constructions, each evaluated numerically on its domain. Lower bounds are Lean-checked for sub, add, mul and div over all reals (each at least 2 nodes); the other entries' lower bounds come from a numerical search or are open, so the capability card records this table as partially proven. CONJ_NO_OP_24 (no 24th operator) is a conjecture — no 24th operator passed the PGC+AIT filter on the open domain; the case analysis is argued on paper, and no Lean proof exists.

23 elementary operators (catalogued; that no 24th passes the PGC+AIT filter is a conjecture) + 8 Pfaffian tower generators (OBSERVATION tier; empirically verified) = 31 operators mapping two tiers of mathematics.

Which F16. On this site F16 means the sixteen operators on /framework, the list the Lean lower bounds (sub, add, mul and div each need at least 2 nodes) quantify over. Since 2026-09-13 the core table counts nodes in that list only. 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%: the sum ModelAudit.lean states, with its ln witness taken through EXL. No Lean theorem states the 15n total. Each construction is evaluated numerically (python/tests/test_superbest_f16_constructions.py), and the totals are upper bounds. The high-impact tables 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 signed division with 7 or fewer nodes (python/benchmarks/superbest_f16/search.py). The 3n that mul and div had before 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), and ln, which has no real value for x ≤ 0. The earlier basket read 16n / 74.2% over 8 operations. The naive costs are the library's pure-EML figures, not re-derived in the recount.

Core Arithmetic Primitives (F16 Layer 1)

Extended Operators (23-op Beyond F16)

Category A: genuine F16 algebraic shortcut. Category B: genuine via EML sign-variant. Category C: notation-only (23-op counts 1n; F16 costs 3–4n; no F16 shortcut exists).

High-Impact Expressions

Layer 1 = F16 ground-truth; Layer 2 = 23-op extended (must be labeled)

ML / Smooth Functions

These F16 counts use the taxonomy lock's orbit, which leaves out LEAd. With LEAd, F11 in the site's F16, softplus is 1 node (LEAd(x, 1)) and LSE(x, y) is 2 (LEAd(x, EML(y, 1))), against the 2 and 4 above; the table keeps the paper's figures.

Quantum / Information

Physics

Special Functions (argued infinite in F16; see each reason)

Pfaffian Tower Extensions OBSERVATION

Empirically verified at sample points, not Lean-proved. The 'no single operator spans two towers' theorem is open (CONJECTURE). The 8 tower families form a 3-rooted hierarchy under DLMF closed-form identities (see hierarchy_note below). Adding 8 tower generators to the EML grammar brings 35 previously-infinite-depth functions inside finite EML trees of depth ≤ 4. Tier label: OBSERVATION (empirical, not Lean-proved).

Verification: 2 towers exact (W, F); 4 towers to ~1e-31 — erf, Si, J, K (mpmath@30-digit precision at sample points); Gamma to ~1e-18 (one tricky sample, others 0.0); Airy via the defining ODE Ai''(x) = x·Ai(x) to 1.5e-7 (the cubic-phase improper integral resists direct mpmath.quadosc convergence).

Hierarchy (3-rooted): Pairwise pass over all 28 tower pairs (28-pair probe in exploration/tower-independence-2026-04-27/): 5 SUBSUMES — T_F (₂F₁) covers T_erf, T_Si, T_J, T_Ai, T_K via DLMF identities (7.18.5, 6.11.2, 10.1x, 9.x, 19.x); T_Gamma and T_W remain independent of everything else found. Minimum generating set in the abstract Pfaffian-closure sense: {T_F, T_Γ, T_W} = 3 towers. All 8 remain operationally needed in the F16 EML grammar (which lacks parameter-substitution primitives).

Outside the closure: Functions still outside the 23-op + 8-tower closure: zeta-family beyond polylog, modular forms, modulo, set/Boolean ops, generic non-computable. See the atlas page for the full out-of-closure list.

Honest Savings Summary

The core row is 1 − 15/73 = 79.5% counted in F16, and 1 − 14/73 = 80.8% in the Layer 2 column, which counts ln x = EXL(0, x) as one node. The ML, quantum and physics rows use the same pooled rule, 1 − (F16 nodes)/(naive nodes) and 1 − (23-op nodes)/(naive nodes), summed over the high-impact expressions of python/paper/exploration/SuperBEST_Final_Taxonomy_Lock.tex: ML, 5 expressions, 1 − 22/34 = 35% and 1 − 13/34 = 62%; quantum, 8, 1 − 48/59 = 19% and 1 − 33/59 = 44%; physics, 5, 1 − 25/35 = 29% and 1 − 21/35 = 40%. The tables above show 4, 6 and 4 of those expressions. Until 2026-09-13 these rows showed the paper's printed estimates, ~35%/~55%, ~15%/~35% and ~30%/~45%, which its own rows do not give. The Aggregate row is still the paper's estimate for a 'representative system' it does not specify, so it cannot be re-derived; pooling all 18 high-impact expressions gives 1 − 95/128 = 26% and 1 − 67/128 = 48%.

Verify it yourself

Reproduce the cost analysis on your own machine. `eml-cost 0.12.0` is on PyPI; the 578-row corpus is bundled inside the wheel.

pip install eml-cost

from eml_cost import analyze
from sympy import symbols, exp, sin

x, t = symbols('x t')
a = analyze(exp(-x) * sin(t))
print(a.cost_class)        # 'p2-d5-w2-c1' — the headline cross-domain class
print(a.pfaffian_r, a.is_pne)   # 2  False

from eml_cost import analyze_dynamics
from sympy import symbols, exp, sin, cos

x, t = symbols('x t')
d = analyze_dynamics(exp(-x) * sin(t) * cos(2*t))
print(d.predicted_r)       # 5  (1 decay + 2 oscillation modes)
print(d.confidence)        # 'high'

from eml_cost import find_siblings
from sympy import symbols, sin, pi

x = symbols('x')
for s in find_siblings(sin(pi*x)/(pi*x), max_distance=0)[:3]:
    print(s.distance, s.expression, s.domain)

Code matches the published 0.12.0 API. `analyze_dynamics` and `find_siblings` ship in 0.10.0+ (rolled up into 0.11.0 / 0.12.0).