Forge sync: STATUS.md -> 06-08 canonical; HONEST_DISCLOSURE.md -> match GitHub (SLSA L2 attested line)

Read-only-audit follow-up: restore GitHub<->HF byte-identical on doc files. Locked-5 and Λ=Conjecture 1 unchanged.

HONEST_DISCLOSURE.md

@@ -1,6 +1,6 @@
 # HONEST_DISCLOSURE — a11oy Receipt Signing
 
-**Doctrine:** v11 LOCKED 749/14/163 · Λ = Conjecture 1 · SLSA L1 honest  
+**Doctrine:** v11 LOCKED 749/14/163 · Λ = Conjecture 1 · SLSA L1 honest · L2 build-attested (Rekor) · L3+ roadmap  
 **Date:** 2026-06-03
 
 ## HMAC Receipt Signing

STATUS.md

@@ -1,25 +1,47 @@
 # STATUS.md — a11oy (Governance Layer)
 
-**Updated:** 2026-06-02
-**Doctrine v11 — 749 / 14 / 163 — replay hash c7c0ba17**
+**Updated:** 2026-06-08
+**Doctrine v11 — locked-proven 749 / 14 / 163 — replay hash c7c0ba17**
 
 HF Space: <https://huggingface.co/spaces/SZLHOLDINGS/a11oy>
 
 ---
 
+## Proof state (honest, never inflate)
+
+- **LOCKED-PROVEN (kernel-verified) = EXACTLY 5** — F1, F11, F12, F18, F19 @ `c7c0ba17`
+  (749 / 14 / 163). This is the *only* "locked" claim. Never fold anything else in.
+- **Λ (F23)** — unconditional uniqueness is machine-checked **FALSE** for A1–A5, so it stays
+  **Conjecture 1**, unconditionally. We *have* proved the strongest axiom-free **conditional**
+  uniqueness: slice-multiplicativity (separability) ⇒ Λ, machine-checked (Wave12), and as of
+  Wave21 the conditional chain is axiom-clean end-to-end on its stated hypotheses. The
+  `(C-order)` gap-shift ordering remains an **honest structural hypothesis** (documented, not faked).
+- **Khipu Byzantine BFT safety** — **Conjecture 2**, open (a faulty organ can equivocate).
+
+## Experimental · CI-green tier (separate from the locked 5 — NEVER folded in)
+
+- `main @ 880c803e` — Wave19 / 20 / 21 merged; Phase-1 stabilize gate cleared; CI
+  (`lake build + numbers` + DCO + doctrine) green on main.
+- 1323 declarations · 23 axioms (22 unique) · sorries_raw 307 · drift 307 / 254.
+- All Wave19/20/21 theorems: `#print axioms ⊆ {propext, Classical.choice, Quot.sound}`;
+  no `sorry`; no new axiom.
+
 ## What's Live
 
-- **HF Space** — a11oy is deployed and operational on Hugging Face Spaces
-- **`/healthz`** — returns Doctrine v11 numbers (749/14/163) and service status
-- **`/sign`** — Wire D DSSE signing endpoint; Ed25519 signed receipts
-- **Λ-aggregator gate** — every request evaluated across Yuyay-13 axes before execution
-- **`/viz/*`** — SPA operator panel for receipt inspection
-- **Wire D** — cross-cutting signing fabric live to all other flagships
+- **HF Space** — a11oy is deployed and operational on Hugging Face Spaces.
+- **`/healthz`** — returns Doctrine v11 locked numbers (749/14/163) and service status.
+- **`/sign`** — Wire D DSSE signing endpoint; Ed25519 signed receipts.
+- **Λ-aggregator gate** — every request evaluated across Yuyay-13 axes before execution.
+- **`/console` + `/viz/*`** — operator panel for receipt inspection and governance surfaces.
+- **a11oy Code IDE** — live.
+- **Wire D** — cross-cutting signing fabric live to all other flagships.
+- **GitHub ↔ HF aligned** — a11oy 5/5, killinchu 9/9; UDS payload/mesh wired
+  (`theorem_ref` + `lake_receipt`, honest).
 
 ## What's Experimental
 
-- **Chain replay verification** — Khipu DAG chain anchoring is functional; full replay harness under development
-- **Multi-key rotation** — key rotation workflow documented but not yet automated
+- **Chain replay verification** — Khipu DAG chain anchoring is functional; full replay harness under development.
+- **Multi-key rotation** — key rotation workflow documented but not yet automated.
 
 ## What's Deprecated
 
@@ -28,4 +50,4 @@ Nothing deprecated in this repo.
 ---
 
 *Co-Authored-By: Perplexity Computer Agent*
-*Doctrine v11 — 749/14/163 — c7c0ba17*
+*Doctrine v11 — locked-proven 749/14/163 — c7c0ba17 · Λ = Conjecture 1 · main @ 880c803e*