# What is honest right now — Doctrine v11

This is the standing honesty disclosure for SZL Holdings. We surface only machine-checked facts as fact; everything else is labeled experimental, conditional, or conjectured.

**lutar-lean @ tag `lutar-v18.0.0` / `c7c0ba17`:**

- **749 declarations · 14 unique axioms · 163 tracked sorries** (112 baseline + 51 Putnam). `lake build` clean.
- **Locked proven set = 5 formulas** (Lean, sorry-free): **F1, F11, F12, F18, F19**. These are the only formulas we surface as "proven."
- **Λ (the trust aggregator) is Conjecture 1** unconditionally. **Unconditional** uniqueness is machine-checked **false** (Round13 `maxAgg_ne_Lambda`). It is proven **CONDITIONAL** on slice-multiplicativity (separability) under {A1,A2,A3,A5}, axiom-free — **CUT-2** (`lambda_unique_of_separable`, PR #202). Λ is never stated as an unconditional theorem. **Byzantine BFT safety is Conjecture 2**, not a theorem.
- **Experimental waves** (proof waves 5–14 + the agentic loop) live in experimental Lean scopes on `main` @ `b910c276`, are **CI-green** with every `#print axioms ⊆ {propext, Classical.choice, Quot.sound}`, but **excluded** from the locked v11 baseline. Through Wave 14: Wave 11 CF-1/2/3/5, Wave 12 CUT-2 + CF-13 + CF-17, Wave 13 replay-root + non-Byzantine vote + HM-bottleneck, Wave 14 CF-18/19/20/21. They are labeled experimental, never folded into the locked five.

**Supply chain:**
- **SLSA L1 build provenance (honest)** on all service images — cosign-signed, verifiable via `cosign verify`. **SLSA L2 is on the roadmap; we do NOT claim L2-verified today.** **No** L2-verified / L3 / FedRAMP / Iron Bank / CMMC is claimed.
- The `szl-mesh` UDS bundle is **cosign-signed** (keyless OIDC). The GitHub attestation for the bundle itself was not minted (token scope); per-image cosign signatures are intact and verifiable.

**Receipts:**
- Decision receipts are **DSSE envelopes over a SHA-256 hash chain**. Where a signing key is present (the killinchu engagement surface carries a real ECDSA-P256 cosign key), receipts are **genuinely signed** and verifiable offline. Where no key is present, receipts are **honestly marked unsigned** — never fabricated.

**Data honesty:**
- Maritime AIS on the field surface uses a clearly-labeled **sample/replay** dataset, not a live production feed.
- Live public feeds (CVE/NVD, CISA KEV, MITRE ATT&CK, USGS) are honestly attributed where shown.

**Compliance posture:** Aligned with **EU AI Act Article 12** (record-keeping) + **NIST AI RMF (MANAGE)**. These are alignment statements, not certifications.

*Built by Stephen P. Lutar Jr. · stephenlutar2@gmail.com · Doctrine v11 LOCKED.*