# Proof-to-code inventory: 21 callable formulas

Source: [`szl-formulas@4eb866bf78da5fa639b8f23d213756d80ba38534`](https://github.com/szl-holdings/szl-formulas/tree/4eb866bf78da5fa639b8f23d213756d80ba38534) and [`lutar-lean@3b0b589ea332fe962afff13328d9675b525e1819`](https://github.com/szl-holdings/lutar-lean/tree/3b0b589ea332fe962afff13328d9675b525e1819).

**Result:** 21/21 Python registry callables identified; 0/21 have an authoritative, checked mapping to one of the eight locked F-number theorems. `UNVERIFIED` means no proof-to-implementation refinement was established; it does not mean the formula is false. The source's `PROOF_STATUS` strings are copied verbatim, not promoted to verified Lean claims.
The 21 source labels begin with 12 `PROVEN`, 7 `AXIOM`, and 2 `SORRY`; these are obligation labels in the source catalog, not 12 checked Python implementations.

The Lean locked set is `{F1,F4,F7,F11,F12,F18,F19,F22}`. Its [machine-readable claim manifest](https://github.com/szl-holdings/lutar-lean/blob/3b0b589ea332fe962afff13328d9675b525e1819/claims/locked-formulas.v1.json) states narrower propositions and explicitly separates the genome/catalog labels from the compiled locked surface. The source [formula atlas](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/atlas/formula-atlas.v1.json) itself records `f_number_to_executable_registry_mapping: UNKNOWN_NOT_INFERRED`.

| # | Callable and source line | Source statement (first line) | Reported status | Formal relationship |
|---:|---|---|---|---|
| 1 | [`lambda_aggregate`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L129) | Λ_w(x) = ∏ xᵢ^{wᵢ}, Σwᵢ = 1, xᵢ ∈ [0,1] (weighted geometric mean). | `PROVEN(A1-A4); uniqueness CONJECTURE` | `CONDITIONAL_RELATED_FORMALIZATION`; mapping `UNVERIFIED` |
| 2 | [`lambda_homogeneous`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L156) | A2 IsHomogeneous: True iff Λ(c·x) == c·Λ(x) within ε. PROOF-STATUS: AXIOM(A2). | `AXIOM(A2)` | `NAMED_LEAN_PROPERTY_NO_REFINEMENT`; mapping `UNVERIFIED` |
| 3 | [`lambda_bounded`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L167) | A4 IsBounded: True iff Λ(x) <= max(x) within ε. PROOF-STATUS: PROVEN(Bound.lean). | `PROVEN(A4, Bound.lean)` | `NAMED_LEAN_PROPERTY_NO_REFINEMENT`; mapping `UNVERIFIED` |
| 4 | [`pac_bayes_mcallester`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L173) | R(Q) ≤ R̂(Q) + sqrt((KL + ln(2√n/δ)) / 2n). PROOF-STATUS: SORRY(PACBayes). | `SORRY(PACBayes)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 5 | [`bekenstein_cascade`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L186) | S_max = (2π R E)/(ℏ c). PROOF-STATUS: PROVEN(TH6 DPI form); dimensional helper. | `PROVEN(TH6 DPI form); dimensional helper` | `NON_EQUIVALENT_LOCKED_TOPIC`; mapping `UNVERIFIED` |
| 6 | [`reidemeister_invariant`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L196) | Apply a Reidemeister move to a braid word. PROOF-STATUS: AXIOM(r1/r2/audit). | `AXIOM(r1/r2/audit_reidemeister_invariance)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 7 | [`khipu_merkle_root`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L221) | Khipu summation-invariant Merkle DAG root. PROOF-STATUS: PROVEN(TH11). | `PROVEN(TH11 SummationInvariant)` | `NON_EQUIVALENT_LOCKED_TOPIC`; mapping `UNVERIFIED` |
| 8 | [`dsse_envelope`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L240) | DSSE envelope with a PLACEHOLDER signature (Sigstore not wired — honest). | `PROVEN(structure); signature PLACEHOLDER` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 9 | [`gleason_quantum_lambda`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L253) | Quantum-axis purity Tr(ρ²) ∈ (0,1]. PROOF-STATUS: AXIOM(gleason_length_mod_8). | `AXIOM(gleason_length_mod_8)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 10 | [`hoeffding_tail`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L263) | P(\|X̄ − E[X̄]\| ≥ t) ≤ 2 exp(−2 n t²). PROOF-STATUS: PROVEN(MomentSubGaussian). | `PROVEN(MomentSubGaussian)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 11 | [`pinsker_kl_bound`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L273) | KL(p\|\|q) ≥ 2·TV(p,q)² (returns the RHS). PROOF-STATUS: AXIOM(pinsker). | `AXIOM(pinsker)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 12 | [`fisher_rao_distance`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L284) | d_FR(p,q) = 2·arccos(Σ √(pᵢqᵢ)). PROOF-STATUS: PROVEN(closed-form). | `PROVEN(closed-form)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 13 | [`bohr_complementarity_floor`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L296) | True iff σ_A·σ_B ≥ 0.25. PROOF-STATUS: PROVEN(inequality). | `PROVEN(inequality)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 14 | [`kochen_specker_18vector_witness`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L304) | Cabello KS-18 parity-obstruction witness. PROOF-STATUS: AXIOM(KS-18 scaffold). | `AXIOM(KS-18 scaffold)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 15 | [`two_witness_ks18_soundness`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L313) | Sound iff TWO independent KS-18 witnesses fire. PROOF-STATUS: SORRY(TwoWitness). | `SORRY(TwoWitness)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 16 | [`shor_codeword_distance`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L319) | Minimum non-zero Hamming weight (= code distance). PROOF-STATUS: PROVEN(Hamming). | `PROVEN(Hamming)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 17 | [`css_ingress_verify`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L328) | Binds a DSSE envelope to a CSS transparency root (4-byte prefix commit). | `PROVEN(structure)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 18 | [`kitaev_surface_correct`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L337) | Minimal surface-code correction (exact for weight-≤1). PROOF-STATUS: AXIOM(QEC surface). | `AXIOM(QEC surface scaffold)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 19 | [`reed_solomon_singleton`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L343) | Singleton bound: max min-distance of an [n,k] code = n − k + 1. | `PROVEN(Singleton bound)` | `NON_EQUIVALENT_LOCKED_TOPIC`; mapping `UNVERIFIED` |
| 20 | [`madhava_series`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L352) | atan(x) = Σ (−1)^m x^(2m+1)/(2m+1), \|x\| ≤ 1. PROOF-STATUS: PROVEN(alternating series). | `PROVEN(alternating series)` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |
| 21 | [`schur_concave_lambda_two_axis`](https://github.com/szl-holdings/szl-formulas/blob/4eb866bf78da5fa639b8f23d213756d80ba38534/torch-ext/szl_formulas/_formulas.py#L365) | Λ(m,m) ≥ Λ(x1,x2), m=(x1+x2)/2. PROOF-STATUS: AXIOM(n-axis); 2-axis PROVEN. | `AXIOM(n-axis); 2-axis PROVEN` | `NO_SPECIFIC_FORMAL_LINK_IDENTIFIED`; mapping `UNVERIFIED` |

## Boundaries that matter for the showcase

- **Λ:** `lambda_aggregate` computes a floating-point weighted geometric mean on a restricted [0,1] contract. Lean's `lambda_unique_of_separable` is conditional on A1–A5 plus separability, multiplicative/monotone slices and normalization. `maxAgg_ne_Lambda` proves bare A1–A5 do not force Λ. Neither result certifies this Python implementation. [Conditional theorem](https://github.com/szl-holdings/lutar-lean/blob/3b0b589ea332fe962afff13328d9675b525e1819/Lutar/Round13/LambdaSeparable.lean#L85) · [counterexample](https://github.com/szl-holdings/lutar-lean/blob/3b0b589ea332fe962afff13328d9675b525e1819/Lutar/Round13/Lambda_Uniqueness.lean#L188).
- **Similar names are not a map:** Lean F18 proves RS(10,6) parity arithmetic; `reed_solomon_singleton` returns `n-k+1`. Lean F19 is Nat addition monotonicity; `bekenstein_cascade` computes a dimensional entropy expression. Lean F4/F22 do not prove `khipu_merkle_root` hash behavior.
- **Implementation guards are narrower than mathematical hypotheses:** the matrix CSV records each callable's input conditions and the visible gap. For example, `gleason_quantum_lambda` does not validate a density matrix, `pinsker_kl_bound` does not compute KL, `css_ingress_verify` compares four digest bytes, and `dsse_envelope` uses a placeholder signature.
- **Tests and proof:** source tests exercise several numeric vectors and rejection paths, but test success is not a Lean-to-Python refinement proof. `NO_DIRECT_ASSERTION_FOUND` in the CSV means this inspection did not find a direct assertion in the primary source tests.

## Next implementation gate

For a demonstrable mapping, add a reviewed contract for each chosen callable: a formal theorem with its exact hypotheses, a finite/float representation relation, a pinned test vector and error bound, and a CI check that binds the source commit to the theorem and vector. Start with `lambda_aggregate`/`lambda_bounded`; keep F18 and F19 unmapped unless the Python semantics are actually refined to their narrower Lean statements.

## Verification method

[The rebuild script](build_proof_code_matrix.py) parses the two public worktrees without importing their code. It refuses unexpected Git HEADs, checks the exact 21 registry symbols and source status strings against the checked-in atlas, checks the eight compiled claim IDs, and fails if the atlas starts asserting an F-number mapping. This pass did not run Lean, execute all 21 functions, or establish Hub mirror parity. Run it with `--formula-tree` and `--lean-tree` pointing to clean checkouts at the pinned SHAs above.