szl-formulas — the 21 canonical formulas, offline

🟩 Kernel + REAL trained surrogate. The governance kernel (pure-Python, stdlib-only) is UNCHANGED and remains the sole ground truth — an offline replay of the live Alloy formula surface: the 21 canonical formulas of canonical-formulas-v1 plus the Codex-Kernel governed-loop composer. Since surrogate v1 this repo ALSO ships model.joblib — a real trained sklearn classifier that identifies WHICH of the 21 formulas produced a given call trace, with MEASURED held-out accuracy 0.9709 (21-class). The surrogate never replaces the kernel's real evaluators. No network, no torch, no tensors in the kernel. Λ uniqueness stays Conjecture 1 (open); the composer's Λ roll-up is ADVISORY only.

Kernel Hub migration (verified 2026-07-15): get_kernel(...) resolves the first-class Kernel Hub repo; main and v1 pin verified revision 39a9fe6fd295f500f30ad7c6ff4cfdf559b48c4a.

Proof honesty (binding — Doctrine v11)

Two DISTINCT things, never conflated:

1. Per-formula PROOF_STATUS — mirrored VERBATIM from the canonical dataset, one of PROVEN / AXIOM / SORRY / CONJECTURE. A PROVEN(...) tag is an obligation-level label (that narrow property is discharged in Lean or numerically exact) — NOT a claim the formula belongs to the locked-proven canonical set.
2. LOCKED_PROVEN_FORMULA_IDS — the locked-proven canonical set is EXACTLY 8: {F1, F4, F7, F11, F12, F18, F19, F22}, machine-enforced by the no-axiom Lean theorem locked_count_eight in lutar-lean. This count is frozen at 8 and never inflated.

The F-numbering is lutar-lean's own corpus (≥ 22 formulas); its mapping onto these 21 registry entries is UNKNOWN — never fabricated.

Quickstart (fully offline)

from kernels import get_kernel
fx = get_kernel("SZLHOLDINGS/szl-formulas", revision="main", trust_remote_code=True)
print(fx.registry_count())                     # 21
print(fx.lambda_aggregate([0.9, 0.8, 0.95]))   # weighted geometric mean (D2)
print(sorted(fx.LOCKED_PROVEN_FORMULA_IDS))    # exactly 8 F-ids
chain = fx.run_governed_loop([
    {"formula_name": "lambda_bounded", "args": [[0.9, 0.8, 0.95]]},
    {"formula_name": "reed_solomon_singleton", "args": [255, 223]}])
print(chain["replay_ok"], chain["lambda_label"])  # True, ADVISORY (Conjecture 1)

The composer

run_governed_loop(calls) chains formula calls into hash-linked receipts; four HARD-STOP validators gate every step (state_transition, drift_bounds, human_gate, axis_floor) — on any failure the loop HALTS and the chain seals at the last good step. verify_chain is a pure replay verifier. The Λ composition is ADVISORY only (Λ = Conjecture 1); a high Λ is a non-compensatory roll-up, not proven trust.

Tests — MEASURED, local, stdlib-only

PYTHONPATH=build/torch-universal python3 -m pytest tests/ -q → 17 passed. Every test is FALSIFIABLE: registry exactly 21; locked-proven exactly 8 (never inflated); PROOF_STATUS verbatim + raises on unknown names; Λ a genuine weighted geo-mean; a tampered receipt is detected and a sub-floor Λ halts the loop.

Provenance

Mirrors canonical-formulas-v1 (formulas.py + composer.py). Backed by lutar-lean, DOI 10.5281/zenodo.20434308. Honest-model trio with szl-invariants and szl-ouroboros; anchored by szl-kernels. Live substrate: a-11-oy.com.

License

Apache-2.0 · © 2026 SZL Holdings · Stephen P. Lutar · ORCID 0009-0001-0110-4173.

Trained formula-identifier v1 (MEASURED — see TRAINING_RECEIPT.json)

A real sklearn HistGradientBoostingClassifier trained on 18,900 traces (900 per formula) generated and labeled by this kernel itself: every sample is produced by calling the REAL REGISTRY[name] evaluator, so the label is definitionally the producing formula (seed 20260721; 126 samples re-audited by kernel replay). Features are trace observables only — argument-shape + the formula's own output shape/type/aggregate stats. No formula name is ever leaked into a feature. Registry count is read from the kernel (registry_count() → 21) and asserted.

metric	value
test accuracy (21-class)	0.9709
mean per-class recall	0.9709

per-class recall	value
bekenstein_cascade	1.0000
bohr_complementarity_floor	0.7778
css_ingress_verify	1.0000
dsse_envelope	1.0000
fisher_rao_distance	0.8889
gleason_quantum_lambda	1.0000
hoeffding_tail	1.0000
khipu_merkle_root	1.0000
kitaev_surface_correct	1.0000
kochen_specker_18vector_witness	1.0000
lambda_aggregate	0.9889
lambda_bounded	1.0000
lambda_homogeneous	1.0000
madhava_series	1.0000
pac_bayes_mcallester	1.0000
pinsker_kl_bound	0.8833
reed_solomon_singleton	1.0000
reidemeister_invariant	1.0000
schur_concave_lambda_two_axis	0.8500
shor_codeword_distance	1.0000
two_witness_ks18_soundness	1.0000

Measured blind spot (stated, never hidden): bohr_complementarity_floor (0.7778), fisher_rao_distance (0.8889), pinsker_kl_bound (0.8833), schur_concave_lambda_two_axis (0.8500) sit below 0.90 recall. formulas that share an argument+output OBSERVABLE signature (e.g. several bool-returning axiom checks over similar inputs) are confusable from trace shape alone; the kernel's evaluators remain authoritative for identity Fast identification belongs to the surrogate; the real evaluators (the kernel) remain authoritative for formula identity. Λ untouched = Conjecture 1.

import joblib
clf = joblib.load("model.joblib")   # feature spec: TRAINING_RECEIPT.json data.features

Re-verify everything: python scripts/eval.py (sha256-checks the shipped model against the receipt, regenerates the seeded dataset via the in-repo kernel, retrains, and compares the 21-class accuracy within ±0.02).

---

_{SZL Holdings honesty footer. Λ = Conjecture 1 (advisory, never a theorem). locked-proven = exactly 8 {F1,F4,F7,F11,F12,F18,F19,F22}. Honesty labels: MEASURED / REPORTED / MODELED / HEURISTIC / UNKNOWN / UNAVAILABLE. Trust never 100% (ceiling 0.97). PROOF_STATUS mirrored verbatim, never inflated. a-11-oy.com · huggingface.co/SZLHOLDINGS}