# λ lutar-lean
### The formal-methods spine of the SZL governance substrate
**Machine-checked Lean 4 + Mathlib proofs for the Λ trust aggregator, the audit-fiber invariants, and the receipt/consensus theorems that every SZL runtime claim depends on.**
[](https://github.com/szl-holdings/lutar-lean/actions/workflows/lake-build.yml)
[](https://github.com/szl-holdings/lutar-lean/actions/workflows/ci.yml)
[](https://github.com/szl-holdings/lutar-lean/actions/workflows/dco.yml)
[](./LICENSE)
[](https://leanprover.github.io/)
[](https://slsa.dev/spec/v1.0/levels)
[-B79BD6.svg?style=flat-square)](./BOUNTY.md)
[-B79BD6.svg?style=flat-square)](https://github.com/szl-holdings/khipu-consensus)
[](https://doi.org/10.5281/zenodo.20434308)
[a11oy.net](https://a11oy.net) · [Org](https://github.com/szl-holdings) · [Thesis (szl-papers)](https://github.com/szl-holdings/szl-papers) · [Λ bounty](./BOUNTY.md) · [🤗 SZLHOLDINGS](https://huggingface.co/SZLHOLDINGS)
`receipts.in ≡ receipts.out`
---
## What this is
**lutar-lean** is the Lean 4 library that formally underwrites SZL's governance math. It defines the **Λ aggregator** (a geometric-mean trust score over four axes — provenance, containment, coherence, convergence), states the axiom system `LutarAxioms` (A1–A5), and machine-checks the theorems that the runtime relies on: aggregator bounds, monotonicity, permutation-invariance, hash-chain tamper-evidence, conformal coverage, and quorum agreement.
It is the **single source of truth** for every "proven" claim made anywhere in the SZL ecosystem. If a property is asserted in the apps, the papers, or the marketing, it is either (a) proven here and labeled *locked*, (b) proven here under explicit hypotheses and labeled *experimental / conditional*, or (c) honestly labeled a **conjecture**. Nothing is overstated.
---
## Proof status — read this before citing anything
SZL runs a strict **two-tier** honesty doctrine. The two tiers never blend.
### Tier 1 — LOCKED (proven, sorry-free, count machine-enforced)
> **Exactly 8 formulas are locked-proven: `F1, F4, F7, F11, F12, F18, F19, F22`.**
They are zero-`sorry`, use only Lean-core axioms `[propext, Classical.choice, Quot.sound]`, and the fact that there are **exactly 8** is *itself* a Lean theorem (`Lutar.Wave8.AxiomDisclosure.locked_count_eight`, which depends on **no** axioms). The locked set cannot silently grow. **It grew from 5 to 8 on 2026-06-10** when F4 and F7 were upgraded from vacuous placeholders (`t The experimental library on `main` type-checks at **1323 declarations / 23 axioms (22 unique), CI-green** on Lean `v4.18.0` (`lake build + numbers` ✅, DCO ✅).
These are real, kernel-verified theorems — waves 5/6/7/8, the agentic loop P1–P6, the airtight-Λ conditional results, and the **frontier theorem families Waves 11–17** — but they are an explicitly separate **EXPERIMENTAL · CI-green** tier and are **never** folded into the locked-8.
**Frontier families (Waves 11–17, all `#print axioms` ⊆ `[propext, Classical.choice, Quot.sound]`, no new axiom, no `sorry`):**
| Wave | Headline results |
|------|------------------|
| **11** | CF-1 graph-automorphism distance invariance · CF-2 Ouro KV-cache slots · CF-3 Ouro early-exit soundness · CF-5 immune Neyman–Pearson optimality |
| **12** | **CUT-2 `lambda_unique_of_separable`** (axiom-free conditional Λ uniqueness — Λ *off bare conjecture*) · CF-13 DEQ input-Lipschitz well-posedness · CF-17 floating-point summation error bound |
| **13** | replay-root completeness · non-Byzantine quorum shadow · Hardy–Littlewood–Pólya HM-bottleneck |
| **14** | CF-18 Leibniz/Mādhava alternating-series remainder · CF-19 Reed–Solomon MDS distance · CF-20 VCG efficiency + truthfulness core · CF-21 Cover–Thomas log-sum + Gibbs |
| **15** | **CF-22 `dpo_klDivergence_nonneg_on_simplex`** (KL ≥ 0 on the simplex — conditionally repairs the false-as-stated DPO axiom) · CF-24 axiom-free bisymmetry→CUT-2 bridge |
| **16** | CF-23 binary-KL convexity crux · CF-24 `geoBin` satisfies the **full Aczél quasi-arithmetic axioms** (idempotent/symmetric/homogeneous/monotone — the last analytic step before CUT-1) · CF-25 Λ scale-invariance · CF-26 abacus place-value |
| **17** | **CF-23 `binary_pinsker`** (full binary Pinsker `2(p−q)² ≤ KL`) · CF-27 monotone-DEQ unique equilibrium · CF-28 recurrent-depth `Kʳ`-Lipschitz |
~100 kernel-clean theorems across these waves; every one is drift-gate-checked and CI-green on `main`. None changes the locked count of 8; Λ stays **Conjecture 1**.
### The Λ line — Conjecture 1 (do not misquote this)
> **Rule of citation (Doctrine v11).** Any uniqueness claim about Λ must cite **Theorem U** (`TheoremU_LambdaUnique`) or its corollaries **U₁** (separable) / **U₂** (power-law factors): uniqueness holds *modulo* the audit-invariant equivalence `≈Λ` under the Identifiability Assumptions (IA). **Strict equality (`=`)** may be claimed **only** under the documented `Anchored` / `Normalized` predicate. *Unconditional* uniqueness under bare A1–A5 is **Conjecture 1 — OPEN** (machine-checked false as stated). Never write "Λ is unique" without one of these qualifiers — the [overclaim guard](./.github/workflows/overclaim-guard.yml) fails CI if you do.
| Claim | Status |
|---|---|
| Λ satisfies A1–A5 | **Proven** (`lambda_satisfiesAxioms_round13`), sorry-free |
| Λ uniqueness, **unconditional** under A1–A5 (`Conjecture1_LambdaUnique`) | **Conjecture 1 — OPEN.** Ships **statement-only**; machine-checked **FALSE** as stated (`Round13.maxAgg_ne_Lambda`: `maxAgg` and `min` satisfy A1–A5 and are not Λ). Open prize: [`lambda-bounty`](https://github.com/szl-holdings/lambda-bounty) |
| **Theorem U** — Λ uniqueness *modulo* `≈Λ` under IA | **REAL · CONDITIONAL** (axiom-free, no sorry): any two IA-solutions are `≈Λ` (`TheoremU_LambdaUnique`), with strict `=` **only** under `Anchored`/`Normalized` (`TheoremU_LambdaUnique_eq`, `lambda_equiv_to_eq_of_anchored`). By REDUCTION to Round13, **no new axiom token**. (Conditional only — Λ *unconditional* uniqueness stays **Conjecture 1**, machine-checked FALSE as stated.) See [`Lutar/Uniqueness/TheoremU.lean`](./Lutar/Uniqueness/TheoremU.lean), [`DEPENDENCY_MAP.md`](./DEPENDENCY_MAP.md) |
| **Corollary U₁** — separable slices | **Proven** (`CorollaryU1_LambdaUnique_Separable` → `Round13.lambda_unique_of_separable`) |
| **Corollary U₂** — power-law factorization | **Proven** (`CorollaryU2_LambdaUnique_Factors` → `Round13.lambda_unique_of_factors`) |
| Λ uniqueness, **conditional** (CUT-2, axiom-free) | **Proven**: any A1–A5 aggregator with multiplicative, separable per-axis slices equals Λ (`lambda_unique_of_separable`), reducing to the in-tree `multiplicative_monotone_isPow_pos` + `lambda_unique_of_factors` with **no new axiom token** |
| Λ uniqueness, **conditional** (Set α / Set δ) | **Proven** under explicitly declared, cited bridge axioms ([PR #192](https://github.com/szl-holdings/lutar-lean/pull/192)) |
| Byzantine BFT safety (equivocating organ) | **Khipu Conjecture 2 — open.** The Wave-13 `quorum_agreement_single_valued_vote` is an honestly-labeled *non-Byzantine shadow* (single-valued `voteOf`); the real `ubuntu_quorum_safety` obligation is left untouched. |
> **Bottom line:** Λ is **Conjecture 1**. We have a *proven, axiom-free conditional* core — **Theorem U** (uniqueness modulo `≈Λ` under IA, strict `=` only under `Anchored`/`Normalized`) plus CUT-2 and the Set α / Set δ variants — but **never** an unconditional uniqueness theorem, because that statement is false. Open prize: [`lambda-bounty`](https://github.com/szl-holdings/lambda-bounty) · [BOUNTY.md](./BOUNTY.md).
Full proof table with verbatim `#print axioms`, run IDs, and per-result maturity → **[PROVEN_FORMULAS.md](./PROVEN_FORMULAS.md)**.
---
## Architecture
```
Lutar/
├── Axioms.lean -- LutarAxioms A1–A5 (monotone, 1-homogeneous,
│ diagonal-normalized, bounded-by-max, symmetric)
├── Puriq/Formulas/
│ └── PuriqFormulaLean.lean -- the 8 LOCKED formula theorems {F1,F4,F7,F11,F12,F18,F19,F22}
├── Round13/ -- Λ-uniqueness machinery (Cauchy/Aczél, CUT-2 conditional)
│ ├── CauchyND_Closure.lean -- monotone+additive ⇒ linear (rational squeeze, 0 sorry)
│ └── Lambda_Uniqueness.lean -- maxAgg_ne_Lambda counterexample (Conjecture-1 anchor)
├── Wave8/AxiomDisclosure.lean -- locked_count_eight (no-axiom theorem: exactly 8 locked)
├── Wave13/Sweep.lean -- experimental: quorum shadow + HM bottleneck (CI-green)
├── Khipu/ -- receipt summation invariants, hash-chain tamper-evidence
├── Innovations/round*/ -- experimental frontier formulas (labeled, gated)
└── Putnam/ -- hard analysis obligations (honest sorries, references intact)
```
**How it fits the ecosystem:** the proofs here are *enforced* at runtime by the receipt layer — the runtime emits DSSE-signed receipts over a SHA-256 hash chain, stored append-only in [`szl-lake`](https://github.com/szl-holdings/szl-lake), witnessed by [`khipu-consensus`](https://github.com/szl-holdings/khipu-consensus), and surfaced for offline verification in [`szl-trust`](https://github.com/szl-holdings/szl-trust). The bounded-recursion runtime that consumes them lives in [`ouroboros`](https://github.com/szl-holdings/ouroboros). The live kernel browser is [`lean-kernel`](https://github.com/szl-holdings/lean-kernel); the open prize for unconditional Λ is [`lambda-bounty`](https://github.com/szl-holdings/lambda-bounty).
---
## Quickstart
```bash
git clone https://github.com/szl-holdings/lutar-lean
cd lutar-lean
lake exe cache get # fetch the Mathlib olean cache
lake build # type-checks the whole library (CI-green on main)
```
Inspect the honest proof posture of any declaration:
```bash
# the locked count is itself a no-axiom theorem
echo '#print axioms Lutar.Wave8.AxiomDisclosure.locked_count_eight' | lake env lean --stdin
# the Conjecture-1 counterexample
echo '#print axioms Lutar.Round13.maxAgg_ne_Lambda' | lake env lean --stdin
```
---
## Honest disclosures
- **Open `sorry`s are tracked, not hidden.** Putnam analysis, the xoshiro period bound (GF(2)²⁵⁶ companion-matrix primitivity), Hoeffding–Azuma assembly, Reed–Solomon Singleton, and the Brouwer/cohomology obligations are genuinely hard (multi-day to multi-week or need Mathlib facts absent at v4.18.0). They stay honest `sorry`s with their references intact.
- **Declared axioms are honest assumptions**, not proofs: cryptographic-hardness axioms (SHA-256 collision-resistance, domain separation), the Λ-family bridge axioms, and deep-math axioms (Gleason, Reidemeister, Liu-Hui) are disclosed and isolated. `#print axioms` is the source of truth.
- **No fabricated metrics. No inflated proof counts.** The locked count is exactly 8 and machine-enforced (was 5 until the 2026-06-10 genuine F4/F7 proofs); the experimental count is reported separately and CI-measured.
---
## Lineage
Mathematical patterns trace to durable, scholarly-documented sources (Rhind Papyrus false position, Inka khipu summation, Liu Hui polygon π, Madhava series-remainder bounds, Cauchy–Aczél functional equations). Ancient sources *inspire* verifiable patterns — no secret-decoding claims, no mystical language (Doctrine v11 boundary).
## License & citation
[Apache-2.0](./LICENSE) — SZL Holdings. ORCID [0009-0001-0110-4173](https://orcid.org/0009-0001-0110-4173).
> **SLSA note (honest):** this is a Lean proof library, not a built product image — its supply-chain posture is **SLSA L1 honest · L2 roadmap**. The org's shipping product images (a11oy, killinchu) are **SLSA L1 honest · L2 build-attested** (container provenance via attest-build-provenance, Sigstore keyless) · L3 roadmap.
> Not affiliated with Defense Unicorns. SZL mark USPTO Serial 99831122. No production ATO claimed.
```
S. P. Lutar Jr., "lutar-lean — Lean 4 Formal Proofs for the SZL Governance Substrate,"
Zenodo, DOI 10.5281/zenodo.20434308, 2026.
```