Stephen Lutar — The Provenanced Notebook. Founder page for Stephen P. Lutar Jr., Founder & CEO of SZL Holdings.
Live at: https://stephenlutar2-hash.github.io/founder-page/
A public founder page that is itself a demonstration of the thesis: every interaction mints a DSSE-signed Khipu receipt, the proof tree is rendered live from lutar-lean, and the trust formula is interactive. The page proves its own claims rather than just stating them.
| Metric | Value |
|---|---|
| Lean 4 declarations | 749 |
| Unique axioms | 14 |
| Sorries (open proof placeholders) | 163 |
| Locked-proven formulas | 8 |
| Wired (CI-checked, not locked) | ~35 |
| Full corpus (Waves 11–22) | ~185 |
| Λ uniqueness | Conjecture 1 (unconditional = machine-checked false; conditional = proven axiom-free) |
| SLSA posture | L1 honest + L2 build-attestation present · L2-verified / L3 / FedRAMP = roadmap |
Source of truth: szl-holdings/lutar-lean@main
- a11oy — governed-inference command platform → a-11-oy.com
- killinchu — maritime / drone C2 → huggingface.co/SZLHOLDINGS
- Company GitHub: github.com/szl-holdings
- Hugging Face org: huggingface.co/SZLHOLDINGS
- Thesis DOI: 10.5281/zenodo.19944926
- ORCID: 0009-0001-0110-4173
This repo does not claim "183 proven," "fully verified," "Λ proven," "SLSA L2 verified," or "L3." All counts above are reproducible from lutar-lean@main. Λ uniqueness is Conjecture 1 — stated and tracked as an open problem.
Apache-2.0 · Doctrine v11 LOCKED · 749 / 14 / 163 · 8 locked-proven · kernel c7c0ba17