Round 5 (housekeeping): doc-consistency welded into the button; both round-4 approvals recorded

Round-4 verdicts: Claude reviewer — nothing blocks the freeze, no
remaining findings; GPT-5.6 — approve after minor documentation fixes,
attestation scoped to the mechanized model. This round is those fixes;
no Lean surface changed.

- 218/59 → 222/61 everywhere, and STRUCTURALLY: check.sh Phase 3c
  asserts the audit counts (STATEMENT-MAP + README vs allowlist/CONES)
  and the four fidelity pins (STATEMENT-MAP vs run_fidelity.py
  constants) on every run — stale-count drift is a red button now
  (R4-1, third recurrence of the class).
- Gap 14 reworded to evidence-vs-inference (the invariant "is assumed",
  not "transfers"), witnesses cited (paper §5.3/§5.4; pacta
  sthstore.py/logclient.py — outside the fidelity target). New gap 15:
  deployment refinement invariant unmechanized (GPT's principal
  finding, split out because it carries the deployed-soundness claim).
- Runbook: A1 marked done (both approvals on SD); B2 gains the REQUIRED
  scoped attestation wording (GPT §11) as a gate condition — entry 13
  cannot claim "deployed verifier formally verified".
- run_bare.sh fail-closes on Lean version AND commit (rejection path
  tested with a fake toolchain: FATAL, exit 1).
- Harness: "consistency baseline family" line (GPT §8); gap 14 says
  "fixed offsets n−1/n+1/n+7" (R4-5).
- RESPONSE round 5, incl. refutation of GPT §7 (the target tarball
  demonstrably contains MANIFEST.sha256 + TARGET-PROVENANCE.md; the
  round-5 kit also ships both unpacked as a courtesy).

check.sh exit 0 ATTESTATION GREEN (Phases 0-4 incl. new 3c); selftest
exit 0, 9/9 + control. Live LTL untouched (12 leaves, bcd15f9d…).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

ATTESTATION-RUNBOOK.md

@@ -52,15 +52,17 @@ Agent Appendix at the end. Every step ends in a mechanical check.
 
 ## PHASE A — do now / while waiting for the IACR decision
 
-### A1. Reviewer confirmations of round 4
+### A1. Reviewer confirmations of round 4 — **DONE (2026-07-15)**
-Deliver the round-4 kit (already on SD) to both reviewers. Required
+Both round-4 reviews are on the SD card. Claude reviewer: "Nothing
-outcome, in their words: GPT-5.6's conditional approval stands with the
+blocks the freeze… no remaining findings on the corpus itself"
-round-4 evidence (its conditions 2 and 3 — recorded hashes, fresh
+(re-executed everything hostile, incl. deliberately breaking the
-button run by exit code — are satisfied by `CORPUS-MANIFEST.sha256` and
+lied-size tripwires — both broke the run as designed — and the first
-`check-transcript.txt` in the kit); the Claude reviewer confirms F1*
+paper↔Lean cross-check, faithful). GPT-5.6: "Approve after minor
-was absorbed faithfully (gap 14 + lied-size family + banner scoping).
+documentation fixes" for an attestation SCOPED TO THE MECHANIZED MODEL
-**Check:** two written reviews on the SD card saying so. If either
+(see the B2 wording requirement below); its principal finding (the
-finds anything new: run another revision round first; do not proceed.
+deployment refinement invariant is unmechanized) is now KNOWN-GAPS
+gap 15. The round-5 housekeeping freeze addressed both reviewers'
+remaining documentation items.
 
 ### A2. The author's read (the one step only the operator can do)
 Read, in this order, against the paper's §6 and §10:
@@ -173,8 +175,24 @@ GREEN`, `exit=0`. Any other outcome: STOP (iron rule 4).
 Fresh clone of `lean-transparency-log`, driver runs once, produces:
 `entries/000012.json`, updated `latest-sth.json` (tree_size 13),
 one new line in `sth-history.jsonl`, one new receipt.
+
+**REQUIRED ATTESTATION SCOPE (round-4 GPT §11 — this wording is a gate
+condition, not a suggestion).** The leaf's human-readable claim text
+must be scoped to the mechanized model, in substance:
+
+> This corpus kernel-checks the listed theorems about the mechanized
+> recursive accumulator model. Correspondence with the deployed
+> inclusion verifier is supported by finite differential testing over
+> the pinned families. The deployed consistency verifier is not
+> extensionally equal to the model; applying the mechanized soundness
+> result to the deployed consumer flow additionally relies on an
+> unmechanized authentic-size/root invariant (KNOWN-GAPS 14/15).
+
+The leaf must NOT say or imply "the deployed verifier is formally
+verified."
 **Check:** `git status` shows exactly those four paths changed/added,
-nothing else. `pacta witness-audit` on the clone exits 0.
+nothing else. The claim text above appears in the attestation.
+`pacta witness-audit` on the clone exits 0.
 
 ### B3. Consumer's-eye check before publishing
 From a DIFFERENT directory with the old pin (size 12):

KNOWN-GAPS.md

@@ -92,15 +92,37 @@ list is COMPLETE, not merely that the items are acceptable.
    identically. Consequences: (a) fidelity between the two consistency
    verifiers is agreement over the pinned case families, NOT
    extensional equality — the harness's lied-size family pins the
-   boundary (73,573 cases, 3,867 expected divergences, direction
+   boundary (73,573 cases: lied old size exhaustive for n < 60, lied
-   asserted one-sided); (b) Theorem 3 / `acceptCons_sound` cover the
+   new size at fixed offsets n−1/n+1/n+7; 3,867 expected divergences,
-   MECHANIZED accept set, and their soundness transfers to the deployed
+   direction asserted one-sided per case); (b) Theorem 3 /
-   verifier only under the side condition that the consumer's
+   `acceptCons_sound` cover the MECHANIZED accept set. The exhibited
-   `(n₀, r₀)` is an authentic pinned pair and `n₁` is the authentic
+   divergence is outside the intended pin-store input invariant;
-   size of the tree behind `r₁` — which pacta's pin-store flow supplies
+   applying the mechanized soundness result to the deployed flow
-   by construction (`n₀` comes from the consumer's own pin, never from
+   therefore additionally ASSUMES that the deployed state machine
-   the peer; `(n₁, r₁)` arrive together in one signed head). No
+   always binds each root to its authentic size and exposes no
-   exploitability against that flow is claimed or ruled out here;
+   alternate invocation path — an invariant that is NOT mechanized in
-   assessing it requires the signature/STH layer (gap 4). No pacta code
+   this corpus (gap 15). Where the invariant's witnesses live: paper
-   change is made (deployed behavior matches upstream RFC 9162
+   §5.3 (the signed head binds `(n₁, r₁)` together under one
-   implementations; the consumer flow enforces the side condition).
+   signature) and §5.4 (the pin `(n₀, r₀)` comes from the consumer's
+   own store, never from the peer), implemented in the pacta repo at
+   `src/pacta/sthstore.py` and `src/pacta/logclient.py` — code OUTSIDE
+   the supplied fidelity target (review R4-3/GPT-4). No exploitability
+   against that flow is claimed or ruled out here; assessing it
+   requires the signature/STH layer (gap 4). No pacta code change is
+   made (deployed behavior matches upstream RFC 9162 implementations).
+15. **Deployment refinement invariant unmechanized** (round-4 GPT, its
+   principal finding — split out from gap 14 because it carries the
+   deployed-soundness claim). The corpus proves soundness of the
+   mechanized `acceptCons`; it does NOT prove the refinement
+   `AuthenticPair(n₀,r₀,D₀) ∧ AuthenticPair(n₁,r₁,D₁) ∧
+   verify_consistency(…) → acceptCons(…)`. The operational invariant
+   (authentic-size/root binding via the signed-head + pin-store flow)
+   is relied upon but unverified, and the consumer flow implementing it
+   is not in the supplied fidelity target. Consequently any attestation
+   of this corpus must be scoped to the MECHANIZED model: "the deployed
+   consistency verifier is formally verified" is NOT a claim this
+   corpus supports. Closure paths (roadmap, operator decision, post
+   paper-freeze): (A) make the deployed verifier adopt
+   ConsRec-equivalent acceptance; or (B) mechanize the signed-head +
+   pin-store state machine and prove the refinement; or (C) keep the
+   boundary and this scoped claim permanently.

README.md

@@ -11,14 +11,19 @@ All paper-§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 after review round 1 (GPT-5.6 + second Claude) and round 2:
+Revised across four external review rounds (GPT-5.6 + a second Claude,
-the audit surface is now an environment-derived inventory
+adversarial; zero broken theorems in any round; both approved after
-(`Proofs/Inventory.lean` + pinned allowlist, self-tested by
+round 4). The audit surface is an environment-derived inventory
-`selftest_audit.sh`), the review kit's fidelity target is
+(`Proofs/Inventory.lean` + pinned allowlist — 222 constants,
-self-contained, `acceptIncl` routes Theorems 1–2, fidelity families
+61 human-reviewed cones, self-tested by `selftest_audit.sh`); the review
-extended (230,271 / 230,016). No changes until the external review
+kit is push-button reproducible (`run_bare.sh`, self-contained fidelity
-completes. The finished certificates' attestation into the LTL is a
+target); `acceptIncl`/`acceptCons_sound` route the theorems through the
-separate, explicitly-authorized operator decision.
+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.
 
 | layer | content | status |
 |---|---|---|
@@ -28,7 +33,7 @@ separate, explicitly-authorized operator decision.
 | L4 | frontier binding content (Lemma 2) | **done as specializations** — inlined in the extractor walk (`extractIncl`), whole-tree (`extractMTH`), ConsRec (`consRecBinding`); the standalone `Root` receipt-uniqueness instance was deleted with the vacuous `root_binding` in S3.5 and deliberately NOT restored (optional, unused — KNOWN-GAPS gap 3) |
 | L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) | **done, non-vacuous** |
 | L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, whole-tree instance) | **done, non-vacuous** |
-| L6b | Theorem 3 (consistency soundness): `consRecBinding` (steps 1–2) + `extractCons`/`extractCons_correct` (+ `_paper` at the paper's exact quantifiers) | **done, non-vacuous** |
+| L6b | Theorem 3 (consistency soundness): `consRecBinding` (steps 1–2) + `extractCons`/`extractCons_correct` (+ `_paper` at the paper's exact quantifiers; `acceptCons_sound` routes it through the named `acceptCons` predicate, size bound derived from acceptance via `consRec_some_le`) | **done, non-vacuous** |
 | L6c | pin-store state machine safety (Proposition 1): `pinAccept_monotone`, `pin_prefix_correct`, `fork_distinct` | **done, non-vacuous** (per-step; multi-step chain = gap 7) |
 
 ## Discipline (identical to the subject corpora)

RESPONSE-TO-REVIEWERS.md

@@ -1,119 +1,90 @@
-# Response to reviewers — round 4
+# Response to reviewers — round 5 (housekeeping)
 
-Corpus: `ltl-accumulator-verified`. Round-3 reviews received against the
+Round-4 reviews received against `2da0a79`: the Claude reviewer
-round-3 freeze `9972ab4`: GPT-5.6 (conditional approval, one portability
+("Round 4 is the cleanest round this corpus has had… Nothing blocks the
-finding) and the round-3 Claude reviewer's Socratic addendum (one new
+freeze; no remaining findings on the corpus itself") and GPT-5.6
-confirmed finding, four reinstated ones). Every claim was independently
+("Approve after minor documentation fixes", scoped-attestation
-re-verified by the operator before any change. This round contains ONE
+condition). No theorem, proof, or Lean surface changed this round —
-new theorem, one harness family, and packaging/scoping fixes. No
+this is the documentation-and-guardrails round both reviewers asked
-existing theorem statement or proof changed.
+for.
 
-## The headline: F1* (Claude addendum) — CONFIRMED and absorbed
+## Disposition
 
-The addendum demonstrated that the deployed `verify_consistency` and
+### Stale counts, third recurrence (Claude R4-1/R4-2 = GPT §6) — fixed STRUCTURALLY
-the mechanized `ConsRec` acceptance are **not extensionally equal**:
-the deployed RFC 9162 iterative verifier accepts honest proofs under
-lied size claims (witness: `verify_consistency(1, 3, R2, R3, P(2→3)) =
-True`; ConsRec rejects). Reproduced exactly on the operator machine
-against deployed pacta: same witness, same 3,405 divergences for
-n < 60, same strictly one-sided direction (the mechanized model is the
-stricter; inclusion diverges nowhere under identical abuse), same
-power-of-two seeding mechanism in the deployed source.
 
-Absorbed as follows:
+All `218/59` occurrences are now `222/61` (STATEMENT-MAP footer, the
+check.sh comment, README status), and — the structural part R4-1
+demanded — **check.sh gained Phase 3c (doc-consistency)**: the audit
+counts in STATEMENT-MAP and README are asserted against the allowlist
+and the CONES table, and the four fidelity pins quoted in the
+STATEMENT-MAP are asserted against the harness's own pinned constants,
+on every button press. Stale-count drift is now a red button, not an
+erratum. README status paragraph rewritten to round-4 reality
+(lied-size family, `acceptCons_sound`, both approvals); the L6b row
+names `acceptCons_sound`.
 
-- **KNOWN-GAPS gap 14**: full statement — witness, mechanism,
+### The deployment bridge (GPT §2/§3/§4, its principal finding) — adopted in full
-  one-sidedness, and the soundness-transfer side condition (the
-  consumer's `(n₀, r₀)` is an authentic pinned pair and `n₁` is the
-  authentic size behind `r₁`), which pacta's pin-store flow supplies by
-  construction. No exploitability against that flow is claimed or ruled
-  out; that assessment belongs to the signature/STH layer (gap 4).
-- **Harness**: new lied-size family — 73,573 boundary cases (lied old
-  size exhaustive for n < 60, lied new size sampled), 3,867 expected
-  divergences PINNED, and the one-sided direction asserted on every
-  case: a single `lean=True / deployed=False` instance fails the run.
-  These families would have caught F1* in round 1; now they guard it
-  forever.
-- **Banner**: `FIDELITY GREEN` now reads "agreement over the pinned
-  case families (not extensional equality; KNOWN-GAPS gap 14)". The
-  STATEMENT-MAP fidelity row and Theorem-3 row carry the same scoping.
-- **No pacta code change.** The deployed behavior matches upstream
-  RFC 9162 implementations; the consumer flow enforces the side
-  condition (`n₀` comes from the consumer's own pin, never from the
-  peer; `(n₁, r₁)` arrive together in one signed head). pacta also
-  remains change-frozen during paper processing.
 
-## F2 — `acceptCons` routed through zero theorems (CONFIRMED, fixed)
+- **Gap 14 reworded** to GPT's evidence-vs-inference formulation: the
+  exhibited divergence is outside the intended pin-store input
+  invariant; applying the mechanized soundness result to the deployed
+  flow additionally ASSUMES the authentic-size/root binding — "is
+  assumed", not "transfers". The invariant's witnesses are now cited by
+  name (paper §5.3/§5.4; pacta `src/pacta/sthstore.py`,
+  `src/pacta/logclient.py` — outside the fidelity target), per Claude
+  R4-3.
+- **New gap 15**: "Deployment refinement invariant unmechanized" — the
+  bridge gets its own named boundary, with the unproven refinement
+  spelled out and the three closure paths (adopt ConsRec semantics in
+  deployment / mechanize the state machine and prove refinement / keep
+  the scoped claim) recorded as a post-paper-freeze operator decision.
+- **Attestation language is now a runbook GATE**: the exact scoped
+  wording from GPT §11 is embedded in ATTESTATION-RUNBOOK step B2 as a
+  required check — entry 13 cannot be written as "the deployed verifier
+  is formally verified."
 
-New theorem `acceptCons_sound` (Theorem3.lean): soundness stated over
+### Toolchain enforcement (GPT §5) — fixed
-the named `acceptCons` predicate the harness tests — the consistency
-twin of round-2's `acceptIncl_sound`. The `n₀ = 0` disjunct is
-discharged from the non-prefix premise; the size bound `n₀ ≤ n₁` is
-derived from ConsRec acceptance itself via the new lemma
-`consRec_some_le` (the `n₀ > n` branch returns `none`), so the caller
-owes nothing beyond acceptance + wrong-prefix. Cones (read from
-`#print axioms`, as always): `consRec_some_le` = [propext,
-LTLAcc.sha256, Quot.sound]; `acceptCons_sound` = [propext,
-Classical.choice, LTLAcc.sha256, Quot.sound]. Both are in CONES,
-AxiomCheck, and the inventory allowlist (218 → 222 constants; the diff
-is exactly the two theorems plus their two generated auxiliaries).
 
-## F3 — Lean-side kit reproducibility (CONFIRMED, fixed)
+`run_bare.sh` now fail-closes on both the Lean version (`4.30.0-rc2`)
+and the exact compiler commit (`3dc1a088…`); `BARE RUN GREEN` is
+reserved for the pinned toolchain, exactly as recommended.
 
-`verification/lean-toolchain` now pins `leanprover/lean4:v4.30.0-rc2`,
+### Banner wording (GPT §8) — adopted
-and `verification/run_bare.sh` is the reviewer's standalone runner:
-plain public `lean`, no lake, no Aeneas checkout — compile all modules,
-print all cones, run the inventory gate. Verified green on this machine
-(under the operator's memory-cap discipline): 61 cone lines, 222
-constants, gate green. check.sh remains the operator's button.
 
-## F4 — regex metacharacters in Phase 3b (CONFIRMED, fixed)
+The per-family line now reads `consistency baseline family: … all
+agree`, so a detached quotation cannot suggest global equivalence.
 
-The `PINNED BUT NOT INVENTORIED` check now uses awk field equality
+### Fidelity-target provenance (GPT §7) — REFUTED, with a courtesy fix
-instead of a regex containing the constant name; the module-manifest
-greps were already `-F`. Dots no longer act as wildcards anywhere in
-the gate.
 
-## F5 — kit hygiene (CONFIRMED, fixed; one sharpening)
+The round-4 target tarball demonstrably contains `MANIFEST.sha256`
+(six per-file SHA-256 entries) and `TARGET-PROVENANCE.md` (repo URL,
+pinned commit `3d81d53`, verification instructions, extraction and run
+commands) at its root — `tar tzf` lists both. The review appears to
+have counted only the `.py` files. No packaging change was required;
+as a courtesy, the round-5 kit ALSO ships both files unpacked beside
+the tarball so they cannot be missed. (The project's discipline cuts
+both ways: reviewer findings are re-verified too, and this one did not
+reproduce.)
 
-The stray `.pyc` was worse than reported: it was **git-tracked**, which
+### Wording nit (Claude R4-5) — adopted
-is why `git archive` shipped it. Untracked; `__pycache__/`/`*.pyc`
-gitignored. The round-4 kit gives the corpus tarball the same treatment
-as the pacta target: `MANIFEST.sha256` over every file in the archive
-plus the pinned public commit and repo URL — this also implements
-GPT's governance condition (publish hashes of the audit-critical
-files; they are all in the archive the manifest covers).
 
-## GPT §7 — hard-coded toolchain bootstrap (CONFIRMED, fixed)
+Gap 14 now says "lied new size at fixed offsets n−1/n+1/n+7" —
+determinism advertised, not obscured.
 
-`AENEAS_ENV` override with a clear FATAL message in both check.sh and
+### Paper queue (Claude R4-4 + GPT §11) — recorded
-selftest_audit.sh, exactly as recommended; default unchanged for the
-operator. Together with F3 this closes the "reviewer-friendly
-push-button" gap: reviewers get `run_bare.sh`, operators keep the
-guarded button.
 
-## GPT §9 — paper-language conditions
+Added to the camera-ready queue: §10(v) "total correctness of the
-
+pin-store state machine" must be scoped to what gaps 4/7/10 delimit;
-Adopted into the paper-cycle queue verbatim (they overlap the queue
+Remark 1's "will carry" must get the gap-3 specializations rewording
-built across rounds 1–3), plus F1*'s two additions: the fidelity
+when the corpus is cited as delivered; and the paper may not describe
-sentence must say "finite differential testing over pinned families,
+Theorem 3 as mechanized "for the deployed verifier" without the gap-15
-extensional equality is false for consistency (one-sided)", and
+qualification.
-Theorem 3's deployment claim must carry the pinned-pair side condition.
-The paper is edited in its own cycle, not in this corpus.
-
-## Reviewer-process note (kept, per this project's candor convention)
-
-The round-3 Claude reviewer's self-analysis (Q1–Q7) found its own
-"confirmed/verified" inflations and then did what the drill demands:
-applied constructive-witness standards to its own strongest doubt and
-produced F1*. Its round-3.5 addendum is the strongest single review
-artifact this corpus has received. The operator re-verified every claim
-in it anyway — trust nothing, including good news.
 
 ## What did NOT change
 
-All pre-existing theorem statements and proofs; the axiom boundary
+Every Lean file, the allowlist, the gate, the self-test, the fidelity
-(single opaque `sha256`); the 230,271/230,016 family pins; the live
+pins (230,271 / 230,016 / 73,573 / 3,867), the axiom boundary, the
-transparency log (12 leaves, root `bcd15f9d…`); deployed pacta.
+live log (12 leaves, `bcd15f9d…`), deployed pacta. Attestation remains
-Attestation remains blocked pending the ePrint decision, the author's
+gated on the ePrint decision, the operator's read (A2), the rehearsal
-read, and an explicit operator order.
+(A4), and an explicit operator order — with the B2 scope wording now
+part of the gate.

STATEMENT-MAP.md

@@ -46,14 +46,18 @@ hypothesis, nor that no other classical argument could reach the
 conclusion on some restricted domain.
 
 Audit surface (enforced by `verification/check.sh`, exit 0 = green):
-the FULL compiled environment of the corpus modules — 218 constants,
+the FULL compiled environment of the corpus modules — 222 constants,
 read from the Lean environment by `Proofs/Inventory.lean` (fully
 qualified names, kinds, axiom cones) and pinned in
 `verification/inventory-allowlist.txt`, diffed fail-closed both
 directions on every run (round-3 replacement for the round-2 source-regex
-gate, which GPT H1 showed was evadable). The 59 human-reviewed statement
+gate, which GPT H1 showed was evadable). The 61 human-reviewed statement
 cones above are additionally checked via `#print axioms` and
 cross-checked against the inventory's independently computed cones.
+(These two counts, and the fidelity pins in the table above, are
+asserted against the allowlist/CONES/harness by check.sh Phase 3c on
+every run — stale-count drift is now a red button, not an erratum:
+review R4-1, after three consecutive rounds of hand-edit failures.)
 `verification/selftest_audit.sh` attacks the gate with nine injection
 cases (attributed/indented/private/instance declarations, a nested
 namespace reusing an audited basename, a smuggled axiom, a deleted

verification/check.sh

@@ -26,8 +26,9 @@ PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theore
 # Certificates and their exact expected cones (observed via #print axioms,
 # never guessed; any drift in EITHER direction is a failure).
 # AUDIT SURFACE: Phase 3b pins the FULL environment of the corpus modules
-# (inventory-allowlist.txt, 218 constants incl. compiler-generated
+# (inventory-allowlist.txt, every compiler-generated auxiliary included —
-# auxiliaries); the 59 entries below are the human-reviewed statement
+# the count is pinned by the allowlist itself and asserted against the
+# docs in Phase 3c); the entries below are the human-reviewed statement
 # surface, additionally queried through #print axioms in Phase 3 and
 # cross-checked against the inventory's independently computed cones.
 declare -A CONES=(
@@ -248,6 +249,33 @@ done
 [ "$COVFAIL" = 0 ] && echo "  coverage complete: environment == allowlist, CONES cross-checked"
 [ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; FAIL=1; }
 [ "$FAIL" = 0 ] || exit 1
+
+# -- Phase 3c: documentation consistency (review R4-1: hand-maintained ------
+# counts went stale three rounds running — so the docs' numbers are now
+# ASSERTED against their sources: allowlist, CONES, and the fidelity pins.
+echo "=== Phase 3c: doc-consistency ==="
+DOCFAIL=0
+NALLOW=$(grep -c '^INV|' "$HERE/inventory-allowlist.txt")
+NCONES=${#CONES[@]}
+SMAP="$HERE/../STATEMENT-MAP.md"
+RDME="$HERE/../README.md"
+grep -qF "$NALLOW constants" "$SMAP" || { echo "  DOC DRIFT: STATEMENT-MAP lacks '$NALLOW constants'"; DOCFAIL=1; }
+grep -qF "$NCONES human-reviewed" "$SMAP" || { echo "  DOC DRIFT: STATEMENT-MAP lacks '$NCONES human-reviewed'"; DOCFAIL=1; }
+grep -qF "$NALLOW constants" "$RDME" || { echo "  DOC DRIFT: README lacks '$NALLOW constants'"; DOCFAIL=1; }
+grep -qF "$NCONES human-reviewed" "$RDME" || { echo "  DOC DRIFT: README lacks '$NCONES human-reviewed'"; DOCFAIL=1; }
+# fidelity pins quoted in the docs must equal the harness's pinned constants
+for n in $(python3 -c "
+import re
+src = open('$HERE/fidelity/run_fidelity.py').read()
+vals = [re.search(r'assert ti == ([0-9_]+)', src).group(1),
+        re.search(r'assert tc == ([0-9_]+)', src).group(1),
+        re.search(r'LIED_PIN_TOTAL = ([0-9_]+)', src).group(1),
+        re.search(r'LIED_PIN_DIV = ([0-9_]+)', src).group(1)]
+print(' '.join(f'{int(v.replace(chr(95),\"\")):,}' for v in vals))"); do
+  grep -qF "$n" "$SMAP" || { echo "  DOC DRIFT: STATEMENT-MAP lacks fidelity pin '$n'"; DOCFAIL=1; }
+done
+[ "$DOCFAIL" = 0 ] && echo "  docs agree with allowlist ($NALLOW), CONES ($NCONES), fidelity pins"
+[ "$DOCFAIL" = 0 ] || { echo "DOC-CONSISTENCY FAILED"; exit 1; }
 # -- Phase 4: definition fidelity (Lean defs vs deployed pacta verifiers) --
 echo "=== Phase 4: definition fidelity ==="
 PACTA_SRC="${PACTA_SRC:-$HERE/../../proof-aware-crypto-tooling-agent/src}"

verification/fidelity/run_fidelity.py

@@ -167,7 +167,7 @@ def main():
     ti, rc, pc = inclusion()
     print(f"  inclusion:   {ti} verifier cases, {rc} MTH==merkle_root, {pc} Path==inclusion_proof  — all agree")
     tc = consistency()
-    print(f"  consistency: {tc} verifier cases (incl. honest), MTH checks  — all agree")
+    print(f"  consistency baseline family: {tc} verifier cases (incl. honest), MTH checks  — all agree")
     tl, dl = lied_sizes()
     print(f"  lied-sizes:  {tl} boundary cases, {dl} EXPECTED divergences, all deployed-accepts-only (gap 14)")
     # pinned counts (identical generation to the paper's harness)

verification/run_bare.sh

@@ -21,6 +21,17 @@ command -v lean >/dev/null || { echo "FATAL: no 'lean' on PATH (want $(cat "$HER
 echo "toolchain: $(lean --version)"
 echo "pinned:    $(cat "$HERE/lean-toolchain")"
 
+# Fail-closed toolchain check (review round 4, GPT §5): BARE RUN GREEN is
+# reserved for the pinned version AND Lean commit — a different toolchain
+# must not be able to print the green marker.
+EXPECTED_VERSION="4.30.0-rc2"
+EXPECTED_COMMIT="3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc"
+ACTUAL="$(lean --version)"
+grep -qF "version $EXPECTED_VERSION" <<<"$ACTUAL" || {
+  echo "FATAL: toolchain version mismatch (want $EXPECTED_VERSION): $ACTUAL"; exit 1; }
+grep -qF "commit $EXPECTED_COMMIT" <<<"$ACTUAL" || {
+  echo "FATAL: toolchain commit mismatch (want $EXPECTED_COMMIT): $ACTUAL"; exit 1; }
+
 export LEAN_PATH="${LEAN_PATH:+$LEAN_PATH:}$HERE/gen:$HERE"
 
 echo "=== compile (gen + 9 proof modules) ==="