szl-formulas

The 21 canonical SZL formulas — pure, typed, stdlib-only — as a get_kernel-discoverable offline governance kernel, each carrying its verbatim PROOF-STATUS. From SZL Holdings.

Honest scope box — read this first

This is NOT a trained model. There are NO weights (.safetensors / .bin / .pt / .gguf). It is a pure-Python, stdlib-only governance kernel: an offline replay of the live Alloy formula surface — the 21 canonical formulas of SZLHOLDINGS/canonical-formulas-v1 plus the Codex-Kernel governed-loop composer. No network, no torch, no tensors. It is get_kernel-discoverable purely so the SZL family loads the same way; it does not import torch. Λ uniqueness stays Conjecture 1 (open); the composer's Λ roll-up is ADVISORY only, never proven trust.

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 here is an obligation-level label (that narrow property is discharged in Lean or numerically exact) — it is NOT a claim that 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 szl-holdings/lutar-lean (PROVEN_FORMULAS.md). 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 NOT asserted here (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(fx.proof_status("madhava_series"))        # "PROVEN(alternating series)" — verbatim
print(sorted(fx.LOCKED_PROVEN_FORMULA_IDS))     # exactly 8 F-ids

# governed loop: hash-chained receipts + 4 hard-stop validators
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)
print(fx.selfcheck())                              # falsifiable_demonstrated: True

The 21 canonical formulas

lambda_aggregate (Λ, weighted geo-mean D2), lambda_homogeneous (A2), lambda_bounded (A4), pac_bayes_mcallester, bekenstein_cascade, reidemeister_invariant, khipu_merkle_root, dsse_envelope, gleason_quantum_lambda, hoeffding_tail, pinsker_kl_bound, fisher_rao_distance, bohr_complementarity_floor, kochen_specker_18vector_witness, two_witness_ks18_soundness, shor_codeword_distance, css_ingress_verify, kitaev_surface_correct, reed_solomon_singleton, madhava_series, schur_concave_lambda_two_axis. Each is pure, typed, no-I/O; call list_formulas() for the name → verbatim PROOF-STATUS table.

The governed-loop 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 — and on any failure the loop HALTS and the receipt 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

17/17 passed on a local python3 run (MEASURED, stdlib-only). Every test is FALSIFIABLE: the registry is exactly 21; the locked-proven set is exactly 8 (never inflated); PROOF_STATUS matches the dataset verbatim and raises on unknown names (never coerced); Λ is a genuine weighted geo-mean (a zero axis pins it to 0; a spread vector sits below the arithmetic mean); a clean governed loop replays but a tampered receipt is detected and a sub-floor Λ halts the loop. selfcheck() reports falsifiable_demonstrated: True.

Provenance

Mirrors SZLHOLDINGS/canonical-formulas-v1 (code/python/formulas.py + composer.py). Backed by the Lean 4 formalization szl-holdings/lutar-lean, DOI 10.5281/zenodo.20434308; concept DOI 10.5281/zenodo.19944926. Λ uniqueness = Conjecture 1 (open); locked-proven = exactly 8 (machine-enforced locked_count_eight).

Compatibility

Python 3.9+, standard library only — no torch, no third-party deps.

License

Apache-2.0. Copyright 2026 SZL Holdings.

---

The SZL honest-model trio + the kernel suite

Part of the SZL Holdings honest-model trio — stdlib-only offline replays of the live Alloy surface:

Model	Lane
szl-invariants	8 falsifiable receipt/ledger invariants, offline
szl-ouroboros	bounded-loop trace + MEASURED/DERIVED loop-tax accounting
szl-formulas (this repo)	the 21 canonical formulas with verbatim PROOF-STATUS + governed-loop composer

Anchored by the governed-kernel suite szl-kernels (hub) and its members (szl-lambda-gate, szl-governed-norm, governed-inference-meter).

Live substrate: a-11-oy.com · a11oy Space.

---

_{SZL Holdings · 21 canonical formulas · PROOF_STATUS mirrored verbatim · locked-proven = exactly 8 (machine-enforced) · Λ = Conjecture 1, advisory only · a-11-oy.com · github.com/szl-holdings · huggingface.co/SZLHOLDINGS}

Signed-off-by: Stephen Lutar stephenlutar2@gmail.com