betterwithage commited on
Commit
d3b8be4
·
verified ·
1 Parent(s): 6dc2ee8

Update HONEST_DISCLOSURE.md — honest org card / scrub dead-organ refs

Browse files
Files changed (1) hide show
  1. HONEST_DISCLOSURE.md +23 -9
HONEST_DISCLOSURE.md CHANGED
@@ -1,11 +1,25 @@
1
  # What is honest right now — Doctrine v11
2
 
3
- **lutar-lean @ tag `lutar-v18.0.0` / c7c0ba17:**
4
-
5
- - **749 declarations · 14 unique axioms (15 raw, 1 dup) · 163 tracked sorries** (112 baseline + 51 Putnam). `lake build` clean.
6
- - **Λ uniqueness is a Conjecture**, not a closed theorem — depends on the open CAUCHY_ND sorry (`Uniqueness.lean:120`) + a missing symmetry axiom.
7
- - **Wires:** Wire B (a11oy↔sentra immune) and Wire C (a11oy↔rosie receipt stream) are **LIVE on main**; Wire D (W3C traceparent across the mesh) is **NOT YET IMPLEMENTED**.
8
- - **SLSA: L1 (honest)** previously mis-claimed as L3; corrected in platform PR #235.
9
- - **Receipts:** DSSE envelopes ship from the amaru tick endpoint today; Sigstore CI signing is **PENDING** signatures labeled "PLACEHOLDER signing not yet wired into CI".
10
- - **Axioms:** A2 = `IsHomogeneous` (positive homogeneity deg 1); A4 = `IsBounded` (bounded by max axis). v3 Zenodo proofs (10.5281/zenodo.19983066) do NOT carry over.
11
- - Aligned with **EU AI Act Article 12** + **NIST AI RMF (MANAGE)**.
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
1
  # What is honest right now — Doctrine v11
2
 
3
+ 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.
4
+
5
+ **lutar-lean @ tag `lutar-v18.0.0` / `c7c0ba17`:**
6
+
7
+ - **749 declarations · 14 unique axioms · 163 tracked sorries** (112 baseline + 51 Putnam). `lake build` clean.
8
+ - **Locked proven set = 5 formulas** (Lean, sorry-free): **F1, F11, F12, F18, F19**. These are the only formulas we surface as "proven."
9
+ - **Λ (the trust aggregator) is Conjecture 1.** It is unique *only conditionally* under a block-consistency axiom (Csató 2018), CI-green on `lutar-lean` main. **Unconditional** uniqueness is machine-checked **false** (`unconditional_lambda_is_false`). Λ is never stated as an unconditional theorem.
10
+ - **Experimental waves** (proof waves 3/5/6/7 + the agentic loop) live in experimental Lean scopes, are **CI-green** but **excluded** from the locked v11 baseline. They are labeled experimental, never folded into the locked proven set.
11
+
12
+ **Supply chain:**
13
+ - **SLSA Build L2** on all service images (cosign + `slsa.dev/provenance/v0.2` attestation on GHCR). **No** L3 / FedRAMP / Iron Bank / CMMC is claimed.
14
+ - The `szl-mesh` UDS bundle is **cosign-signed** (keyless OIDC). The GitHub attestation for the bundle itself was not minted (token scope); the per-image SLSA L2 attestations are separate and intact.
15
+
16
+ **Receipts:**
17
+ - 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.
18
+
19
+ **Data honesty:**
20
+ - Maritime AIS on the field surface uses a clearly-labeled **sample/replay** dataset, not a live production feed.
21
+ - Live public feeds (CVE/NVD, CISA KEV, MITRE ATT&CK, USGS) are honestly attributed where shown.
22
+
23
+ **Compliance posture:** Aligned with **EU AI Act Article 12** (record-keeping) + **NIST AI RMF (MANAGE)**. These are alignment statements, not certifications.
24
+
25
+ *Built by Stephen P. Lutar Jr. · stephenlutar2@gmail.com · Doctrine v11 LOCKED.*