Spaces:
Running
Running
File size: 3,259 Bytes
545c5f9 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 | # 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](/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`](https://github.com/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:
```bash
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`](https://github.com/szl-holdings/szl-lake)
- **Hugging Face:** [`SZLHOLDINGS/szl-lake`](https://huggingface.co/datasets/SZLHOLDINGS/szl-lake)
- **Layout (7 dirs):** `attestations/` · `doctrine/` · `keys/` · `khipu/` · `papers/` · `sboms/` · `trajectories/`
- **Lean companion DOI:** [10.5281/zenodo.20424992](https://doi.org/10.5281/zenodo.20424992)
## Zenodo DOIs
The Ouroboros Thesis and supporting artifacts are deposited with persistent DOIs.
| DOI | Role |
|-----|------|
| [10.5281/zenodo.20434276](https://doi.org/10.5281/zenodo.20434276) | **Ouroboros Thesis v18.0** (versioned) — cited by every flagship |
| [10.5281/zenodo.19944926](https://doi.org/10.5281/zenodo.19944926) | **Concept DOI** (always-latest) |
| [10.5281/zenodo.20424992](https://doi.org/10.5281/zenodo.20424992) | Lean companion |
| [10.5281/zenodo.20434308](https://doi.org/10.5281/zenodo.20434308) · [20431181](https://doi.org/10.5281/zenodo.20431181) | Supporting artifacts |
A complete, versioned list is maintained in the thesis repository's `CITATION.cff`. The
[Evidence page](/evidence/) 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)*
|