--- tags: - kernel - governance - formulas - proof-status - lean4 - lambda-aggregate - doi:10.5281/zenodo.19944926 library_name: kernels license: apache-2.0 szl-governance: verdict: ADVISORY lambda: "Conjecture 1 (open) — uniqueness unproven; composer Λ roll-up is ADVISORY only, never proven trust" provenance: "offline replay of SZLHOLDINGS/canonical-formulas-v1 — 21 pure formulas + the governed-loop composer" honest_blocked: "PROOF_STATUS is mirrored verbatim; locked-proven canonical set is EXACTLY 8 (machine-enforced) — never inflated" --- # 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](https://huggingface.co/SZLHOLDINGS). > ## 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`](https://huggingface.co/datasets/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](https://github.com/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) ```python 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`](https://huggingface.co/datasets/SZLHOLDINGS/canonical-formulas-v1) (`code/python/formulas.py` + `composer.py`). Backed by the Lean 4 formalization [szl-holdings/lutar-lean](https://github.com/szl-holdings/lutar-lean), DOI [10.5281/zenodo.20434308](https://doi.org/10.5281/zenodo.20434308); concept DOI [10.5281/zenodo.19944926](https://doi.org/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`](https://huggingface.co/SZLHOLDINGS/szl-invariants) | 8 falsifiable receipt/ledger invariants, offline | | [`szl-ouroboros`](https://huggingface.co/SZLHOLDINGS/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`](https://huggingface.co/SZLHOLDINGS/szl-kernels) (hub) and its members ([`szl-lambda-gate`](https://huggingface.co/SZLHOLDINGS/szl-lambda-gate), [`szl-governed-norm`](https://huggingface.co/SZLHOLDINGS/szl-governed-norm), [`governed-inference-meter`](https://huggingface.co/SZLHOLDINGS/governed-inference-meter)). **Live substrate:** [a-11-oy.com](https://a-11-oy.com) · [a11oy Space](https://huggingface.co/spaces/SZLHOLDINGS/a11oy). --- 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 *