szl-formulas

Software kernel for SZL formula composition. Not a model. No weights.

IS: a pure-Python, stdlib-only governance kernel — offline replay of the 21 canonical formulas plus the governed-loop composer. Public surface includes registry_count(), lambda_aggregate, LOCKED_PROVEN_FORMULA_IDS, run_governed_loop, PROOF_STATUS (mirrored verbatim).

IS NOT: trained weights, LoRA, GGUF, .pt, or a classifier. Hub model.joblib is QUARANTINED executable serialization (and is not on this tree) — do not joblib.load it. Not a CUDA/Triton speedup. Not lutar-lean and not the TypeScript ouroboros product.

Canonical GitHub source: https://github.com/szl-holdings/szl-formulas
Hub package: https://huggingface.co/kernels/SZLHOLDINGS/szl-formulas
This model-type repo is the publish / card mirror. Apache-2.0.

<!-- SZL-ATELIER-CUT:v1:START -->
## The cut

Papers have appendices. We have a kernel of formulas whose sorry-count is public (Doctrine v11: 749 / 14 / 163).

A formula registry that cannot drift from the Lean tree.

### Silhouette → leave → SZL

| Leader | Take, then tweak |
|---|---|
| Anthropic | Written principles, but ours compile. |
| NVIDIA | Recipe as code. |
| Unsloth | No. |

Nobody else ships this combination. That is the point of a one-of-one.

## Intended use

Import formulas. Check proof-status before citing.

## Limitations

- Λ uniqueness is Conjecture 1 — NOT a theorem.

Canonical GitHub: [`szl-holdings/szl-formulas`](https://github.com/szl-holdings/szl-formulas/blob/main/README.md)
<!-- SZL-ATELIER-CUT:v1:END -->

from kernels import get_kernel
fx = get_kernel("SZLHOLDINGS/szl-formulas", revision="main", trust_remote_code=True)
print(fx.registry_count())                   # 21
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)

Proof honesty: per-formula PROOF_STATUS is PROVEN / AXIOM / SORRY / CONJECTURE copied verbatim — that is not membership in the locked-proven set. Locked-proven is exactly 8: {F1, F4, F7, F11, F12, F18, F19, F22}. The F-number mapping onto these 21 registry names is UNKNOWN — never fabricated.

Claim	Label
Source on GitHub	REACHABLE
CUDA benches	UNAVAILABLE
Weights	not applicable
Λ	Conjecture 1 (advisory, never a theorem)

Doctrine v11. Copyright 2026 SZL Holdings · Stephen P. Lutar · ORCID 0009-0001-0110-4173.