From 0fc2b59cbb6cbcd2c10f3ed80c638f70c6ba77c9 Mon Sep 17 00:00:00 2001
From: mrwulf <mrwulf.cleaner@gmail.com>
Date: Thu, 16 Jul 2026 20:40:19 +0200
Subject: [PATCH] =?UTF-8?q?README:=20status=20ATTESTED=20=E2=80=94=20LTL?=
 =?UTF-8?q?=20entry=2013,=20live=20(12=E2=86=9213,=20root=203488a2d0)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The corpus is now leaf index 12 of the log it describes. Status
FROZEN→ATTESTED; the 'attestation is a separate operator decision' line
is now the completed fact, with the live head, leaf hash, prefix
relation, and scope (KNOWN-GAPS 14/15) stated. Six review rounds noted.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
---
 README.md | 44 +++++++++++++++++++++++++++++++-------------
 1 file changed, 31 insertions(+), 13 deletions(-)

diff --git a/README.md b/README.md
index 8082d0b..ebd25df 100644
--- a/README.md
+++ b/README.md
@@ -5,25 +5,43 @@ Lean 4 mechanization of the security analysis (§6) of the paper
 accumulator's own correctness and soundness theorems, kernel-checked, in
 the same discipline as the four `*-ed25519-verified` subject corpora.
 
-## Status: **FROZEN for external review** (corpus complete)
+## Status: **ATTESTED — LTL entry 13, live (2026-07-16)**
 
-All paper-§10 mechanization targets are kernel-checked; the audit surface
-is defined and green (`verification/check.sh`, exit 0). See
+This corpus is now itself a leaf of the log it describes. It was appended
+as **entry 13** of the Lean Transparency Log (freeze `172a1d0`), making
+the log the first deployed transparency log to carry kernel-checked
+proofs of its own accumulator machinery. Live head after the append:
+tree size **13**, root
+`3488a2d0ff9f00415bb561d61b01a420e3ca2e0f7b29351ec9ebb3f57319da0d`; this
+corpus is leaf index 12, hash
+`8cb258d657f1fd00baaa9e0091e26c316cb69b591cb249a9543f51cade57c50a`. The
+old 12-leaf head (`bcd15f9d…`) is a proven prefix; the 12→13 consistency
+transition is accepted by both the deployed verifier and the mechanized
+model. Fetch and verify it at
+[ltl.zkdefi.org/v1/sth](https://ltl.zkdefi.org/v1/sth). The leaf carries
+its own **scope** block: what is kernel-checked is the mechanized model
+(§6), and correspondence to the deployed verifier is scoped by
+KNOWN-GAPS 14/15 — the leaf does not claim the deployed verifier is
+formally verified.
+
+All paper-§6/§10 mechanization targets are kernel-checked; the audit
+surface is defined and green (`verification/check.sh`, exit 0). See
 [STATEMENT-MAP.md](STATEMENT-MAP.md) for the paper↔Lean review surface and
 [KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger.
-Revised across four external review rounds (GPT-5.6 + a second Claude,
-adversarial; zero broken theorems in any round; both approved after
-round 4). The audit surface is an environment-derived inventory
-(`Proofs/Inventory.lean` + pinned allowlist — 222 constants,
-61 human-reviewed cones, self-tested by `selftest_audit.sh`); the review
-kit is push-button reproducible (`run_bare.sh`, self-contained fidelity
-target); `acceptIncl`/`acceptCons_sound` route the theorems through the
-named acceptance predicates; fidelity = agreement over pinned families
+Reviewed across **six** external adversarial rounds (GPT-5.6 + a second
+Claude; zero broken theorems in any round; both approved). The audit
+surface is an environment-derived inventory (`Proofs/Inventory.lean` +
+pinned allowlist — 222 constants, 61 human-reviewed cones, self-tested by
+`selftest_audit.sh`); the review kit is push-button reproducible
+(`run_bare.sh`, self-contained fidelity target);
+`acceptIncl`/`acceptCons_sound` route the theorems through the named
+acceptance predicates; fidelity = agreement over pinned families
 (230,271 + 230,016 baseline; 73,573 lied-size boundary cases with
 3,867 expected one-sided divergences — KNOWN-GAPS gaps 14/15, not
 extensional equality). Doc counts are asserted by check.sh Phase 3c.
-The finished certificates' attestation into the LTL is a separate,
-explicitly-authorized operator decision, scoped per the runbook.
+How the append was done — release tuple, preflight, candidate-inspection
+gate, and the 12→13 structural rehearsal — is recorded in
+[ATTESTATION-RUNBOOK.md](ATTESTATION-RUNBOOK.md).
 
 | layer | content | status |
 |---|---|---|