Proof — Lean kernel, data lake, and DOIs

Every SZL claim is meant to be checked. This page is the proof index: the machine-checked Lean kernel, the public attestation lake, and the persistent Zenodo DOIs. For the full reproduction commands and commit anchors, see Evidence.

Doctrine v11 LOCKED — 749 declarations / 14 unique axioms / 163 tracked sorries · kernel c7c0ba17. Λ = Conjecture 1 (not a theorem). SLSA L1 honest (cosign-signed, keyless Sigstore — L2 provenance attestation is roadmap, not yet claimed).

Lean kernel — lutar-lean

The machine-checked proof corpus.

• Repo: szl-holdings/lutar-lean — Lutar/
• Locked snapshot: tag lutar-v18.0.0 / c7c0ba17 — 749 / 14 / 163 (lake build clean)
• Key files: Lutar/Axioms.lean (A1–A4), Lutar/Khipu/SummationInvariant.lean, Lutar/QEC/KitaevSurface, Lutar/DPI/DPIBound.lean (Pinsker)
• PURIQ obligations: formulas/PuriqLean.lean — puriq_halting_safety, puriq_lambda_monotone, puriq_khipu_integrity, puriq_bekenstein_bound (all sorry-tagged, never hidden)

Reproduce the canonical figures yourself:

gh repo clone szl-holdings/lutar-lean /tmp/lutar -- --depth 1
cd /tmp/lutar
DECL=$(grep -rE '^(theorem|lemma|def|abbrev|axiom) ' --include='*.lean' Lutar/ | wc -l)
SORRY=$(grep -rE '\bsorry\b' --include='*.lean' Lutar/ | wc -l)
echo "Lean: $DECL declarations / $SORRY sorries"

Honest scope. lake build requires Mathlib (~12 GB); the sandbox cannot build it, so Lean verification is performed in GitHub Actions CI only. Λ uniqueness remains a Conjecture — it depends on the open CAUCHY_ND sorry (Uniqueness.lean:120) plus a missing symmetry axiom.

Data lake — szl-lake

The public attestation lake: DSSE receipts, doctrine snapshots, Khipu chains, SBOMs, and evaluation trajectories.

• GitHub: szl-holdings/szl-lake
• Hugging Face: SZLHOLDINGS/szl-lake
• Layout (7 dirs): attestations/ · doctrine/ · keys/ · khipu/ · papers/ · sboms/ · trajectories/
• Lean companion DOI: 10.5281/zenodo.20424992

Zenodo DOIs

The Ouroboros Thesis and supporting artifacts are deposited with persistent DOIs.

DOI	Role
10.5281/zenodo.20434276	Ouroboros Thesis v18.0 (versioned) — cited by every flagship
10.5281/zenodo.19944926	Concept DOI (always-latest)
10.5281/zenodo.20424992	Lean companion
10.5281/zenodo.20434308 · 20431181	Supporting artifacts

A complete, versioned list is maintained in the thesis repository's CITATION.cff. The Evidence page carries the full DOI register and commit anchors.

---

Doctrine v11 LOCKED · 749/14/163 · kernel c7c0ba17 · Λ = Conjecture 1 · SLSA L1 honest (L2 provenance attestation = roadmap)