diff --git a/.gitignore b/.gitignore
index a01f31d..395edfa 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,5 @@
 *.olean
 .lake/
+__pycache__/
+*.pyc
+bare-*.out
diff --git a/KNOWN-GAPS.md b/KNOWN-GAPS.md
index eb2334e..34279bb 100644
--- a/KNOWN-GAPS.md
+++ b/KNOWN-GAPS.md
@@ -77,3 +77,30 @@ list is COMPLETE, not merely that the items are acceptable.
    from the kit). Round 3 ships the complete stdlib-only import closure
    of `pacta.transparency`, content-addressed against pacta commit
    `3d81d53`, plus the clean-extraction transcript with exit code.
+14. **Deployed `verify_consistency` accepts strictly more than the
+   mechanized `ConsRec` on lied-size inputs** (round-3 Claude addendum
+   F1*, reproduced by the operator against deployed pacta). Witness:
+   for the honest proof P between sizes 2→3, `verify_consistency(1, 3,
+   R2, R3, P)` returns True — a semantically false claim ("R2 is the
+   root of a size-1 prefix") — while `ConsRec` rejects; 3,405 such
+   divergences exist for n < 60, ALL one-sided (the mechanized model
+   never accepts anything the deployed verifier rejects; inclusion
+   shows zero divergences under identical abuse). Mechanism: when the
+   claimed old size is a power of two, the deployed RFC 9162 iterative
+   algorithm seeds the walk with the old root and uses the sizes only
+   as bit-navigation state, so several size claims navigate one proof
+   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
+   asserted one-sided); (b) Theorem 3 / `acceptCons_sound` cover the
+   MECHANIZED accept set, and their soundness transfers to the deployed
+   verifier only under the side condition that the consumer's
+   `(n₀, r₀)` is an authentic pinned pair and `n₁` is the authentic
+   size of the tree behind `r₁` — which pacta's pin-store flow supplies
+   by construction (`n₀` comes from the consumer's own pin, never from
+   the peer; `(n₁, r₁)` arrive together in one signed head). 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; the consumer flow enforces the side condition).
diff --git a/README.md b/README.md
index 158677b..6d1ae49 100644
--- a/README.md
+++ b/README.md
@@ -40,6 +40,10 @@ separate, explicitly-authorized operator decision.
 - `verification/check.sh` is THE button: compiles every file through
   `lean-guard` (memory cap, core pinning, timeout, single-flight lock)
   and axiom-audits every certificate against its documented exact cone.
+- Reviewers without the operator toolchain: `verification/run_bare.sh`
+  compiles, axiom-audits, and inventory-gates the corpus with a plain
+  public `lean` (version pinned in `verification/lean-toolchain`); the
+  operator path is overridable via `AENEAS_ENV`.
 - Expected boundary: `propext, Classical.choice, Quot.sound` plus
   `LTLAcc.sha256` for hash-touching certificates — documented per
   certificate in `check.sh`, audited both directions.
diff --git a/RESPONSE-TO-REVIEWERS.md b/RESPONSE-TO-REVIEWERS.md
index 5c51068..2a54e2e 100644
--- a/RESPONSE-TO-REVIEWERS.md
+++ b/RESPONSE-TO-REVIEWERS.md
@@ -1,136 +1,119 @@
-# Response to reviewers — round 3
+# Response to reviewers — round 4
 
-Corpus: `ltl-accumulator-verified`. Round-2 reviews received against the
-round-2 freeze `260ad64` (GPT-5.6 second adversarial review; second
-Claude round-2 findings). Every finding was independently re-verified
-against the corpus before any change; all confirmed findings are fixed
-in this freeze. No theorem statement changed except the one interface
-tightening both reviewers requested (L1/NEW-2).
+Corpus: `ltl-accumulator-verified`. Round-3 reviews received against the
+round-3 freeze `9972ab4`: GPT-5.6 (conditional approval, one portability
+finding) and the round-3 Claude reviewer's Socratic addendum (one new
+confirmed finding, four reinstated ones). Every claim was independently
+re-verified by the operator before any change. This round contains ONE
+new theorem, one harness family, and packaging/scoping fixes. No
+existing theorem statement or proof changed.
 
-## Disposition of round-2 findings
+## The headline: F1* (Claude addendum) — CONFIRMED and absorbed
 
-### GPT H1 / Claude NEW-1 — coverage gate evadable (CONFIRMED, fixed structurally)
+The addendum demonstrated that the deployed `verify_consistency` and
+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.
 
-Both reviewers were right, and GPT's namespace-collision attack
-(`LTLAcc.Hidden.MTH` classified against `CONES[LTLAcc.MTH]`) showed that
-regex hardening (Claude's proposed fix) would not have closed the class.
-We adopted GPT's required correction in full — the inventory is now
-derived from the Lean environment, not from source:
+Absorbed as follows:
 
-- **`Proofs/Inventory.lean`** imports every corpus module and emits
-  EVERY constant whose originating module is a corpus module: fully
-  qualified name, declaration kind, and axiom cone. There is **no
-  filtering** — compiler-generated auxiliaries and `_private.*` mangles
-  are emitted and pinned too, so there is no name shape that can hide.
-  A corpus module missing from the import list is an elaboration error.
-- The axiom cone is computed by our own walker AND cross-checked
-  in-process against core `collectAxioms` (the machinery `#print axioms`
-  uses) for every constant — divergence is a hard error. (This caught a
-  real toolchain subtlety during development: `ConstantInfo.value?`
-  returns `none` for theorems on 4.30.0-rc2, which would have silently
-  truncated cones; the direct constructor match avoids it, and the
-  cross-check would have refused to ship it.)
-- **`verification/inventory-allowlist.txt`** pins all 218 constants;
-  **`inventory_gate.sh`** diffs environment vs allowlist fail-closed in
-  BOTH directions (UNCLASSIFIED / STALE), requires the INV-COUNT
-  trailer (a truncated Lean run cannot pass as an empty diff), and
-  asserts the whole corpus contains exactly one axiom-kind constant:
-  `LTLAcc.sha256`.
-- check.sh Phase 3b additionally verifies: the inventory's module list
-  == the compile manifest (both directions), every CONES entry appears
-  in the allowlist **with an identical cone** (two independent cone
-  computations must agree), and every CONES entry is queried by
-  AxiomCheck.
-- **GPT release condition 2 (adversarial tests) is met by
-  `verification/selftest_audit.sh`**, which attacks the exact production
-  gate: attributed, indented, private, and instance declarations, the
-  nested-namespace basename collision, a smuggled axiom, a deleted
-  declaration (STALE direction), and unmanifested `Proofs/` and `gen/`
-  modules through the full check.sh — plus a positive control so the
-  self-test cannot pass vacuously. Transcript in the kit
-  (`selftest-transcript.txt`).
+- **KNOWN-GAPS gap 14**: full statement — witness, mechanism,
+  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.
 
-### GPT H2 — fidelity target could not run (CONFIRMED, fixed)
+## F2 — `acceptCons` routed through zero theorems (CONFIRMED, fixed)
 
-Reproduced exactly (`ModuleNotFoundError: pacta.postquantum`). The
-round-3 `pacta-fidelity-target` ships the complete **load-time import
-closure** of `pacta.transparency` (`__init__`, `transparency`,
-`postquantum`, `signing`, `yamlio`) — all stdlib-only, so a bare
-Python 3 runs it with no pip installs — content-addressed in
-`MANIFEST.sha256` against pacta commit `3d81d538…` with verification
-instructions (`TARGET-PROVENANCE.md`). The kit includes the complete
-terminal transcript AND exit code of `run_fidelity.py` executed from a
-clean extraction: exit 0, `230,271 + 230,016`, zero mismatches
-(`fidelity-clean-run-transcript.txt`), plus the full green `check.sh`
-transcript ending in `ATTESTATION GREEN` with fidelity not skipped
-(`check-transcript.txt`) — GPT release conditions 3 and 5.
+New theorem `acceptCons_sound` (Theorem3.lean): soundness stated over
+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).
 
-### GPT M1 — audit narrower outside Proofs/ (CONFIRMED, fixed)
+## F3 — Lean-side kit reproducibility (CONFIRMED, fixed)
 
-- Orphan-olean guard is now recursive over the whole tree (it caught a
-  stray development artifact on its first run).
-- gen/ has the same unmanifested-source ("dead file") check as Proofs/.
-- The axiom surface is pinned corpus-wide twice: textually (exactly one
-  `axiom` line under gen/, none under Proofs/) and semantically (the
-  inventory admits exactly one axiom-kind constant anywhere).
-- Declaration discovery under gen/ now goes through the environment
-  inventory like everything else.
+`verification/lean-toolchain` now pins `leanprover/lean4:v4.30.0-rc2`,
+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.
 
-### GPT M2 — stale fidelity counts in STATEMENT-MAP (CONFIRMED, fixed)
+## F4 — regex metacharacters in Phase 3b (CONFIRMED, fixed)
 
-The row now reads 230,271 + 230,016 with the expanded families named.
-Process note: the round-2 Claude review certified this row as already
-fixed; it was not. Consistent with this project's experience, "verified"
-claims by reviewers are themselves re-verified now.
+The `PINNED BUT NOT INVENTORIED` check now uses awk field equality
+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.
 
-### GPT M3 — "not choice-dischargeable" overclaims (CONFIRMED, fixed)
+## F5 — kit hygiene (CONFIRMED, fixed; one sharpening)
 
-STATEMENT-MAP now uses (essentially) GPT's safer wording: the guards
-show each named extractor returns a non-collision on at least one
-canonical honest input, ruling out the globally-inhabited-existential
-degeneration; they do NOT establish logical dependence on every
-hypothesis, nor exclude other classical arguments on restricted domains.
+The stray `.pyc` was worse than reported: it was **git-tracked**, which
+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 L1 / Claude NEW-2 — redundant `hm` in `acceptIncl_sound` (CONFIRMED, fixed)
+## GPT §7 — hard-coded toolchain bootstrap (CONFIRMED, fixed)
 
-The hypothesis is gone; the range fact is derived from `hacc.1`, so the
-theorem is stated purely in terms of acceptance + wrong-leaf premise.
-Cone unchanged (`propext, Classical.choice, LTLAcc.sha256, Quot.sound`),
-re-verified by `#print axioms` and the inventory.
+`AENEAS_ENV` override with a clear FATAL message in both check.sh and
+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 ledger additions (adopted, as history)
+## GPT §9 — paper-language conditions
 
-KNOWN-GAPS gains gap 12 (audit-gate lineage: the round-2 gate was
-evadable, what replaced it, and the residual limits of an
-environment-derived inventory — it cannot see never-compiled source,
-which the dead-file checks cover, nor defeat a hostile toolchain) and
-gap 13 (the round-2 kit's fidelity target was not self-contained).
+Adopted into the paper-cycle queue verbatim (they overlap the queue
+built across rounds 1–3), plus F1*'s two additions: the fidelity
+sentence must say "finite differential testing over pinned families,
+extensional equality is false for consistency (one-sided)", and
+Theorem 3's deployment claim must carry the pinned-pair side condition.
+The paper is edited in its own cycle, not in this corpus.
 
-## Found in round-3 self-review (neither reviewer caught)
+## Reviewer-process note (kept, per this project's candor convention)
 
-- **README layer table was still stale at `260ad64`**: L4 carried
-  "queued for S4 restoration" and the pin-store row said "pending",
-  despite round-1 F2 being certified as fixed by the round-2 Claude
-  review. The table now matches the frozen state (all layers done,
-  L4 explicitly "done as specializations" per gap 3).
-- KNOWN-GAPS gap 2 still cited the old 164,224 count; updated.
-
-## Round-2 Claude review, remaining notes
-
-NEW-1 was correct in direction; we implemented the stronger
-environment-based fix rather than the proposed regex broadening, since
-the namespace collision defeats any basename-keyed source scan. The
-round-2 Claude claim that the fidelity harness was "confirmed green
-against the real pacta code" was obtained by hand-stubbing the missing
-modules — with the round-3 self-contained target, that result is now
-reproducible by anyone from the kit alone.
+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 theorem statements and proofs except the `acceptIncl_sound`
-signature tightening; the axiom boundary (single opaque `sha256`); the
-pinned CONES table (59 entries, all cones byte-identical to round 2);
-the fidelity counts. The live transparency log remains frozen at
-12 leaves (root `bcd15f9d…`) and is untouched by this round;
-attestation remains blocked pending the ePrint decision, author
-review, and an explicit operator order.
+All pre-existing theorem statements and proofs; the axiom boundary
+(single opaque `sha256`); the 230,271/230,016 family pins; the live
+transparency log (12 leaves, root `bcd15f9d…`); deployed pacta.
+Attestation remains blocked pending the ePrint decision, the author's
+read, and an explicit operator order.
diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md
index a362426..fecc1cb 100644
--- a/STATEMENT-MAP.md
+++ b/STATEMENT-MAP.md
@@ -21,11 +21,11 @@ mechanization to items i–v).
 | Lemma 2, whole-tree instance | `extractMTH` + `extractMTH_correct` | Descent | sha256 (+choice) |
 | Lemma 2, ConsRec instance (Thm 3 steps 1–2) | `consRecBinding` | Binding3 | sha256 (+choice) |
 | Theorem 2 (inclusion soundness, explicit 𝓔) | `extractIncl` + `extractIncl_correct` | Extract | sha256 (+choice) |
-| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged) | Theorem3 | sha256 (+choice) |
+| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged); `acceptCons_sound` routes it through the named `acceptCons` predicate (size bound derived from acceptance via `consRec_some_le`). Covers the MECHANIZED accept set; transfer to the deployed verifier is conditional on the pinned-pair side condition of gap 14 | Theorem3 | sha256 (+choice) |
 | Prop 1(1) (pin monotonicity + prefix) | `pinAccept`, `pinAccept_monotone`, `pin_prefix_correct` | PinStore | sha256 (+choice) |
 | Prop 1(2), Merkle share | `fork_distinct` (different roots ⇒ different content); transferability = signature layer, out of scope | PinStore | sha256 |
 | non-vacuity guards (anti-pigeonhole) | `extractIncl_nonvacuous`, `extractMTH_nonvacuous`, `extractCons_nonvacuous`, `pin_prefix_nonvacuous` | Extract/Descent/Theorem3/PinStore | sha256 |
-| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency (paper's case set + out-of-range families m≥n, n₀>n₁, n₀=0; round-2 M2 fixed the stale pre-expansion counts here) | fidelity | (testing) |
+| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency over the pinned case families — **not extensional equality**: the lied-size family (73,573 cases) pins the known one-sided divergence of gap 14 (3,867 expected, deployed-accepts-only, direction asserted) | fidelity | (testing) |
 
 Note on "assumption-free" (paper §10(i)): `incl_complete`'s cone lists
 `LTLAcc.sha256`, but the theorem assumes **no property** of it — it
diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index 2a35d50..5482147 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/verification/Proofs/AxiomCheck.lean
@@ -68,3 +68,5 @@ import Proofs.PinStore
 #print axioms LTLAcc.acceptIncl_sound
 #print axioms LTLAcc.extractCons_correct_paper
 #print axioms LTLAcc.Hash
+#print axioms LTLAcc.consRec_some_le
+#print axioms LTLAcc.acceptCons_sound
diff --git a/verification/Proofs/Theorem3.lean b/verification/Proofs/Theorem3.lean
index c403a75..8de80c1 100644
--- a/verification/Proofs/Theorem3.lean
+++ b/verification/Proofs/Theorem3.lean
@@ -78,4 +78,41 @@ theorem extractCons_correct_paper (n₀ : Nat) (C : List Hash) (D₀ D₁ : List
     rw [hD0, h0]; simp
   · exact extractCons_correct n₀ C D₀ D₁ hlen0 hpos hle hne hacc
 
+/-- `ConsRec` acceptance implies the size bound: the `n₀ > n` branch
+    returns `none`, so a `some` forces `n₀ ≤ n`. Lets `acceptCons_sound`
+    owe no separate range hypothesis (mirrors `acceptIncl_sound`
+    deriving `m < n` from `hacc.1` — review round 3, F2). -/
+theorem consRec_some_le {n₀ n : Nat} {C : List Hash} {b : Bool} {r : Hash}
+    {p : Hash × Hash} (h : ConsRec n₀ n C b r = some p) : n₀ ≤ n := by
+  rcases Nat.lt_or_ge n n₀ with hgt | hge
+  · rw [ConsRec, if_neg (by omega : ¬ n₀ = n),
+        if_pos (Or.inl hgt : n₀ > n ∨ n₀ = 0 ∨ n ≤ 1)] at h
+    simp at h
+  · exact hge
+
+/-- Consistency soundness through the named acceptance predicate
+    (review round 3, F2 — the consistency twin of `acceptIncl_sound`):
+    if `acceptCons` holds between the pinned head of `D₀` and the head
+    of `D₁` but `D₀` is not the real prefix, `extractCons` outputs a
+    collision. The `n₀ = 0` disjunct of `acceptCons` is impossible under
+    `hne` (`D₀ = [] = D₁.take 0`); the size bound comes from acceptance
+    itself (`consRec_some_le`).
+
+    SCOPE (gap 14): this covers the MECHANIZED accept predicate. The
+    deployed `verify_consistency` accepts strictly more on inputs whose
+    claimed sizes are not the authentic sizes of the trees behind the
+    roots; soundness transfers to deployment only under the pinned-pair
+    side condition documented in KNOWN-GAPS gap 14. -/
+theorem acceptCons_sound (n₀ : Nat) (C : List Hash) (D₀ D₁ : List Bytes)
+    (hlen0 : D₀.length = n₀)
+    (hne : D₀ ≠ D₁.take n₀)
+    (hacc : acceptCons n₀ D₁.length (MTH D₀) (MTH D₁) C) :
+    IsCollision (extractCons n₀ C D₀ D₁).1 (extractCons n₀ C D₀ D₁).2 := by
+  rcases hacc with h0 | hcons
+  · exfalso; apply hne
+    have hD0 : D₀ = [] := List.length_eq_zero_iff.mp (by omega)
+    rw [hD0, h0]; simp
+  · exact extractCons_correct_paper n₀ C D₀ D₁ hlen0
+      (consRec_some_le hcons) hne hcons
+
 end LTLAcc
diff --git a/verification/check.sh b/verification/check.sh
index 2ee90d3..da35e09 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -9,7 +9,11 @@
 #         2 compile manifest · 3 boundary-exact axiom audit
 # ─────────────────────────────────────────────────────────────────────────────
 set -euo pipefail
-source ~/aeneas-toolchain/env.sh
+# Toolchain bootstrap is overridable for reviewers with their own install
+# (review round 3, GPT §7); the operator default stays pinned.
+AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
+[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV (set AENEAS_ENV; or use run_bare.sh with a plain lean per lean-toolchain)"; exit 1; }
+source "$AENEAS_ENV"
 HERE="$(cd "$(dirname "$0")" && pwd)"
 AENEAS_LEAN="$AENEAS_HOME/backends/lean"
 TIMEOUT="${LEAN_TIMEOUT:-600}"
@@ -86,6 +90,8 @@ declare -A CONES=(
   [LTLAcc.acceptIncl_complete]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
   [LTLAcc.acceptIncl_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
   [LTLAcc.extractCons_correct_paper]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.consRec_some_le]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.acceptCons_sound]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
 )
 
 # (The former EXCLUDE table is gone: since Phase 3b reads the environment,
@@ -225,8 +231,11 @@ while IFS='|' read -r _ name _ cone; do
       echo "  CONE CROSS-CHECK FAILED: $name CONES=[$want] inventory=[$got]"; COVFAIL=1; }
   fi
 done < <(grep '^INV|' "$HERE/inventory-allowlist.txt")
+# (field-equality, not regex — dots in names must not act as wildcards;
+#  review round 3, F4)
 for cert in "${!CONES[@]}"; do
-  grep -q "^INV|$cert|" "$HERE/inventory-allowlist.txt" || {
+  awk -F'|' -v n="$cert" '$1=="INV" && $2==n {found=1} END {exit !found}' \
+      "$HERE/inventory-allowlist.txt" || {
     echo "  PINNED BUT NOT INVENTORIED: $cert (in CONES, not in allowlist)"; COVFAIL=1; }
 done
 rm -f "$INVLOG"
diff --git a/verification/fidelity/__pycache__/lean_defs.cpython-314.pyc b/verification/fidelity/__pycache__/lean_defs.cpython-314.pyc
deleted file mode 100644
index e898b29..0000000
Binary files a/verification/fidelity/__pycache__/lean_defs.cpython-314.pyc and /dev/null differ
diff --git a/verification/fidelity/run_fidelity.py b/verification/fidelity/run_fidelity.py
index 97d6cc3..b293bf2 100644
--- a/verification/fidelity/run_fidelity.py
+++ b/verification/fidelity/run_fidelity.py
@@ -9,8 +9,12 @@ deployed RFC 9162 code EXHAUSTIVELY OVER all size/index (and old/new
 size) pairs through 256 FOR the two fixed generated datasets and the
 listed mutation classes (honest, wrong-leaf, wrong-index, wrong-root,
 truncated/padded proof, and out-of-range m≥n / n0>n1 / n0=0). It is not
-a proof of extensional equality over all inputs; the Lean-to-Python
-bridge remains trusted quoted-source inspection (see KNOWN-GAPS).
+a proof of extensional equality over all inputs — and extensional
+equality is in fact FALSE for consistency: the lied-size family below
+pins the known one-sided divergence (deployed accepts claimed sizes an
+honest proof was never generated for; the mechanized ConsRec rejects —
+KNOWN-GAPS gap 14). The Lean-to-Python bridge remains trusted
+quoted-source inspection (see KNOWN-GAPS).
 
 Requires the pacta repo on PYTHONPATH (its src/). Bound NMAX matches the
 paper.
@@ -34,6 +38,11 @@ from pacta.transparency import (            # noqa: E402
 import lean_defs as L                       # noqa: E402
 
 NMAX = int(os.environ.get("FIDELITY_NMAX", "256"))
+# lied-size family pins (gap 14; valid for the default FIDELITY_LIED_NMAX=60):
+# 73,573 boundary cases, 3,867 expected one-sided divergences
+# (3,405 lied-old-size + 462 lied-new-size), smallest witness (n=3, m=2 claimed 1)
+LIED_PIN_TOTAL = 73_573
+LIED_PIN_DIV = 3_867
 
 
 def _h(b):
@@ -100,17 +109,74 @@ def consistency():
     return total
 
 
+def lied_sizes():
+    """Lied-size boundary family (round-3 review, Claude F1* / gap 14).
+
+    The deployed RFC 9162 iterative verify_consistency accepts honest
+    proofs under CLAIMED sizes the proof was never generated for (when
+    the claimed old size is a power of two it seeds the walk with the
+    old root and uses the sizes only as bit-navigation state); the
+    mechanized ConsRec binds the split geometry to the sizes and
+    rejects. Divergences in this family are therefore EXPECTED and
+    documented — what this pins is:
+      (a) the DIRECTION: every divergence must be deployed=True /
+          lean=False (the mechanized model is the stricter one; a
+          lean=True/deployed=False case would break soundness transfer
+          and fails the run immediately), and
+      (b) the exact divergence COUNT, so any drift in either verifier
+          shows up as a pin failure.
+    Inclusion showed zero divergences under identical abuse (round-3
+    addendum); the inclusion side is covered by the m>=n families above.
+    """
+    lied_nmax = int(os.environ.get("FIDELITY_LIED_NMAX", "60"))
+    total = 0
+    div = 0
+    for n in range(2, lied_nmax):
+        data = [bytes([i % 251]) for i in range(n)]
+        r1 = merkle_root(data)
+        for m_true in range(1, n):
+            P = consistency_proof(data, m_true)
+            r0 = merkle_root(data[:m_true])
+            for m_lie in range(0, n + 1):          # lied OLD size
+                if m_lie == m_true:
+                    continue
+                total += 1
+                dep = verify_consistency(m_lie, n, r0, r1, P)
+                lean = L.accept_cons(m_lie, n, r0, r1, P)
+                if dep != lean:
+                    div += 1
+                    assert dep and not lean, (
+                        "ONE-SIDEDNESS BROKEN: lean accepts, deployed rejects",
+                        n, m_true, m_lie)
+            for n_lie in (n - 1, n + 1, n + 7):     # lied NEW size
+                if n_lie < m_true or n_lie == n or n_lie < 1:
+                    continue
+                total += 1
+                dep = verify_consistency(m_true, n_lie, r0, r1, P)
+                lean = L.accept_cons(m_true, n_lie, r0, r1, P)
+                if dep != lean:
+                    div += 1
+                    assert dep and not lean, (
+                        "ONE-SIDEDNESS BROKEN: lean accepts, deployed rejects",
+                        n, m_true, "n_lie", n_lie)
+    return total, div
+
+
 def main():
     print(f"S7 fidelity: Lean defs vs deployed pacta, NMAX={NMAX}")
     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")
+    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)
     assert ti == 230_271, ti   # re-pinned after adding out-of-range families (F1)
     assert tc == 230_016, tc
-    print(f"  PINNED: inclusion={ti} (230,271)  consistency={tc} (230,016)")
-    print("=== FIDELITY GREEN: mechanized defs agree with deployed verifier ===")
+    assert (tl, dl) == (LIED_PIN_TOTAL, LIED_PIN_DIV), (tl, dl)
+    print(f"  PINNED: inclusion={ti} (230,271)  consistency={tc} (230,016)  lied-sizes={tl}/{dl}")
+    print("=== FIDELITY GREEN: agreement over the pinned case families "
+          "(not extensional equality; KNOWN-GAPS gap 14) ===")
 
 
 if __name__ == "__main__":
diff --git a/verification/inventory-allowlist.txt b/verification/inventory-allowlist.txt
index 65e14c7..e8b6fd2 100644
--- a/verification/inventory-allowlist.txt
+++ b/verification/inventory-allowlist.txt
@@ -15,20 +15,59 @@
 #
 # Invariant checked by check.sh on top of the diff:
 #   exactly ONE axiom line in this file, and it is LTLAcc.sha256.
+INV|LTLAcc.Bytes|def|
+INV|LTLAcc.ConsRec._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.ConsRec._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.ConsRec._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec._unary|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec.induct|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec.match_1|def|
+INV|LTLAcc.ConsRec|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Hash|def|
+INV|LTLAcc.IsCollision|def|LTLAcc.sha256
+INV|LTLAcc.MTH._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.MTH._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.MTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.MTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.MTH_single|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.MTH_split._proof_1_2|theorem|Quot.sound,propext
+INV|LTLAcc.MTH_split._proof_1_3|theorem|Quot.sound,propext
+INV|LTLAcc.MTH_split|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.MTH|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Path._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.Path._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.Path._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Path._unary.induct|theorem|Quot.sound,propext
+INV|LTLAcc.Path._unary|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Path.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Path.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Path.induct|theorem|Quot.sound,propext
+INV|LTLAcc.Path|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.Root._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.Root._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root._unary|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root.match_1|def|
+INV|LTLAcc.Root_left._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.Root_left._proof_1_2|theorem|Quot.sound,propext
+INV|LTLAcc.Root_left|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root_one_cons|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root_one|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root_right._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.Root_right._proof_1_2|theorem|Quot.sound,propext
+INV|LTLAcc.Root_right|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.Root|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.acceptCons_sound._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.acceptCons_sound|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.acceptCons|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.acceptIncl|def|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.acceptIncl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.acceptIncl_sound|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Bytes|def|
-INV|LTLAcc.ConsRec|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRec_base_false_eq|theorem|Classical.choice,Quot.sound,propext
-INV|LTLAcc.consRec_base_false_eq.match_1|def|propext
-INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_1|def|propext
-INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_2|def|propext
-INV|LTLAcc.consRec_base_true_eq|theorem|propext
-INV|LTLAcc.consRec_base_true_eq.match_1|def|propext
-INV|LTLAcc.consRecBinding|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRecBinding.match_1|def|
+INV|LTLAcc.acceptIncl|def|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.consRecBinding._proof_1_10|theorem|Quot.sound,propext
 INV|LTLAcc.consRecBinding._proof_1_11|theorem|Quot.sound,propext
 INV|LTLAcc.consRecBinding._proof_1_12|theorem|Quot.sound,propext
@@ -41,38 +80,44 @@ INV|LTLAcc.consRecBinding._proof_1_5|theorem|Quot.sound,propext
 INV|LTLAcc.consRecBinding._proof_1_6|theorem|Quot.sound,propext
 INV|LTLAcc.consRecBinding._proof_1_7|theorem|Quot.sound,propext
 INV|LTLAcc.consRecBinding._proof_1_8|theorem|Quot.sound,propext
-INV|LTLAcc.ConsRec.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.ConsRec.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.ConsRec.induct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.ConsRec.match_1|def|
-INV|LTLAcc.ConsRec._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.ConsRec._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.ConsRec._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.ConsRec._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.ConsRec._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.consRecBinding.match_1|def|
+INV|LTLAcc.consRecBinding|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_1|def|propext
+INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_2|def|propext
+INV|LTLAcc.consRec_base_false_eq.match_1|def|propext
+INV|LTLAcc.consRec_base_false_eq|theorem|Classical.choice,Quot.sound,propext
+INV|LTLAcc.consRec_base_true_eq.match_1|def|propext
+INV|LTLAcc.consRec_base_true_eq|theorem|propext
+INV|LTLAcc.consRec_some_le._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.consRec_some_le|theorem|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.domsep|theorem|
 INV|LTLAcc.eq_dropLast_append_of_getLast?|theorem|propext
 INV|LTLAcc.exists_singleton_of_length_one|theorem|Classical.choice,Quot.sound,propext
-INV|LTLAcc.extractCons|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractCons_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractCons_correct_paper|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractCons_correct_paper._proof_1_1|theorem|Quot.sound,propext
-INV|LTLAcc.extractCons_correct._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractCons_correct._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.extractCons.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractCons.match_1|def|
-INV|LTLAcc.extractConsNode|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary|def|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractConsNode.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractConsNode.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractConsNode.match_1|def|
-INV|LTLAcc.extractConsNode._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractConsNode._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractConsNode._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.extractConsNode._unary._proof_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractCons_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractConsNode|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractCons_correct._proof_1_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractCons_correct._proof_1_3|theorem|Quot.sound,propext
+INV|LTLAcc.extractCons_correct_paper._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractCons_correct_paper|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractCons_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractCons_nonvacuous._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractIncl|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractCons_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractCons|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractIncl._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl._unary|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl.match_1|def|
 INV|LTLAcc.extractIncl_correct._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.extractIncl_correct._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.extractIncl_correct._proof_1_4|theorem|Quot.sound,propext
@@ -81,17 +126,18 @@ INV|LTLAcc.extractIncl_correct._proof_1_6|theorem|Quot.sound,propext
 INV|LTLAcc.extractIncl_correct._proof_1_7|theorem|Quot.sound,propext
 INV|LTLAcc.extractIncl_correct._proof_1_8|theorem|Quot.sound,propext
 INV|LTLAcc.extractIncl_correct._proof_1_9|theorem|Quot.sound,propext
-INV|LTLAcc.extractIncl.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl.match_1|def|
-INV|LTLAcc.extractIncl_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractIncl_nonvacuous._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractIncl._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractMTH._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractMTH._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH._unary|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH.induct|theorem|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractMTH_correct._proof_1_10|theorem|Quot.sound,propext
 INV|LTLAcc.extractMTH_correct._proof_1_4|theorem|Quot.sound,propext
 INV|LTLAcc.extractMTH_correct._proof_1_5|theorem|Quot.sound,propext
@@ -99,114 +145,72 @@ INV|LTLAcc.extractMTH_correct._proof_1_6|theorem|Quot.sound,propext
 INV|LTLAcc.extractMTH_correct._proof_1_7|theorem|Quot.sound,propext
 INV|LTLAcc.extractMTH_correct._proof_1_8|theorem|Quot.sound,propext
 INV|LTLAcc.extractMTH_correct._proof_1_9|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH.induct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.extractMTH_nonvacuous._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractMTH_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH|def|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.fork_distinct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.getD_drop|theorem|Quot.sound,propext
 INV|LTLAcc.getD_drop._proof_1_1|theorem|Quot.sound,propext
-INV|LTLAcc.getD_take|theorem|Quot.sound,propext
+INV|LTLAcc.getD_drop|theorem|Quot.sound,propext
 INV|LTLAcc.getD_take._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.getD_take._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.Hash|def|
+INV|LTLAcc.getD_take|theorem|Quot.sound,propext
 INV|LTLAcc.hleaf|def|LTLAcc.sha256
-INV|LTLAcc.hnode|def|LTLAcc.sha256
 INV|LTLAcc.hnode_preimage_inj|theorem|propext
-INV|LTLAcc.incl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.hnode|def|LTLAcc.sha256
 INV|LTLAcc.incl_complete._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.incl_complete._proof_1_5|theorem|Quot.sound,propext
 INV|LTLAcc.incl_complete._proof_1_6|theorem|Quot.sound,propext
 INV|LTLAcc.incl_complete._proof_1_7|theorem|Quot.sound,propext
 INV|LTLAcc.incl_complete._proof_1_8|theorem|Quot.sound,propext
 INV|LTLAcc.incl_complete._proof_1_9|theorem|Quot.sound,propext
-INV|LTLAcc.instDecidableEqHash|def|
+INV|LTLAcc.incl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.instDecidableEqHash._proof_1|theorem|
-INV|LTLAcc.instInhabitedHash|def|propext
+INV|LTLAcc.instDecidableEqHash|def|
 INV|LTLAcc.instInhabitedHash._proof_1|theorem|propext
-INV|LTLAcc.IsCollision|def|LTLAcc.sha256
-INV|LTLAcc.kbelow|def|Quot.sound,propext
+INV|LTLAcc.instInhabitedHash|def|propext
+INV|LTLAcc.kbelow._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow._unsafe_rec|def|
 INV|LTLAcc.kbelow.eq_1|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow.eq_def|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow_eq_of_pow2_between|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_2|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_4|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow_lt|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow_eq_of_pow2_between|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_lt._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_lt._proof_1_4|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_lt._proof_1_5|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow_lt|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_pos|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_pow2|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow_prefix_eq|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_prefix_eq._proof_1_1|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow._unsafe_rec|def|
-INV|LTLAcc.le_two_kbelow|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow_prefix_eq|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow|def|Quot.sound,propext
 INV|LTLAcc.le_two_kbelow._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.le_two_kbelow._proof_1_4|theorem|Quot.sound,propext
-INV|LTLAcc.MTH|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.MTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.MTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.MTH._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.MTH._proof_2|theorem|Quot.sound,propext
-INV|LTLAcc.MTH_single|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.MTH_split|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.MTH_split._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.MTH_split._proof_1_3|theorem|Quot.sound,propext
-INV|LTLAcc.Path|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Path.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Path.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Path.induct|theorem|Quot.sound,propext
-INV|LTLAcc.Path._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Path._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Path._unary.induct|theorem|Quot.sound,propext
-INV|LTLAcc.Path._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.Path._unary._proof_2|theorem|Quot.sound,propext
-INV|LTLAcc.pinAccept|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.pinAccept_monotone|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.le_two_kbelow|theorem|Quot.sound,propext
 INV|LTLAcc.pinAccept_monotone._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.pinAccept_monotone._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.pinExtract|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.pinAccept_monotone|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.pinAccept|def|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.pinExtract.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.pin_prefix_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.pinExtract|def|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.pin_prefix_correct._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.pin_prefix_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.pin_prefix_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.pin_prefix_nonvacuous._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.pow2_exp_unique|theorem|Quot.sound,propext
+INV|LTLAcc.pin_prefix_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
 INV|LTLAcc.pow2_exp_unique._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.pow2_exp_unique._proof_1_2|theorem|Quot.sound,propext
 INV|LTLAcc.pow2_exp_unique._proof_1_3|theorem|Quot.sound,propext
-INV|LTLAcc.Root|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root_left|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root_left._proof_1_1|theorem|Quot.sound,propext
-INV|LTLAcc.Root_left._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.Root.match_1|def|
-INV|LTLAcc.Root_one|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root_one_cons|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root_right|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root_right._proof_1_1|theorem|Quot.sound,propext
-INV|LTLAcc.Root_right._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.Root._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.Root._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.Root._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.pow2_exp_unique|theorem|Quot.sound,propext
 INV|LTLAcc.sha256|axiom|LTLAcc.sha256
 INV|LTLAcc.take_all|theorem|propext
 INV|LTLAcc.take_append_drop|theorem|
 INV|LTLAcc.take_drop_prefix|theorem|Classical.choice,Quot.sound,propext
-INV|LTLAcc.take_take_le|theorem|Quot.sound,propext
 INV|LTLAcc.take_take_le._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.take_take_le|theorem|Quot.sound,propext
 INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.eq_1|theorem|
 INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.eq_2|theorem|
 INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.splitter|def|
@@ -214,15 +218,15 @@ INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.eq_1|theorem|
 INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.eq_2|theorem|
 INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.splitter|def|
 INV|_private.Proofs.Basic.0.PSigma.casesOn._arg_pusher|theorem|
-INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_1|theorem|
-INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_2|theorem|
-INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.splitter|def|
 INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.eq_1|theorem|
 INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.eq_2|theorem|
 INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.splitter|def|
 INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.eq_1|theorem|
 INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.eq_2|theorem|
 INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.splitter|def|
+INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_1|theorem|
+INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_2|theorem|
+INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.splitter|def|
 INV|_private.Proofs.Completeness.0.PSigma.casesOn._arg_pusher|theorem|
 INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.eq_1|theorem|
 INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.eq_2|theorem|
diff --git a/verification/lean-toolchain b/verification/lean-toolchain
new file mode 100644
index 0000000..6c7e31f
--- /dev/null
+++ b/verification/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.30.0-rc2
diff --git a/verification/run_bare.sh b/verification/run_bare.sh
new file mode 100755
index 0000000..03a1454
--- /dev/null
+++ b/verification/run_bare.sh
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# ─────────────────────────────────────────────────────────────────────────────
+# run_bare.sh — REVIEWER's standalone runner (review round 3, Claude F3).
+#
+# Compiles, axiom-audits, and inventory-gates the corpus with a plain
+# public `lean` binary — no lake, no Aeneas checkout, no operator
+# environment. The corpus is Mathlib-free and needs only the toolchain
+# pinned in ./lean-toolchain (elan users: `elan default $(cat lean-toolchain)`
+# or run inside this directory and let elan pick it up).
+#
+# This runner exists so a reviewer can go from "trust the transcripts"
+# to "run the button" on any machine. It is NOT the operator's button:
+# check.sh remains the release gate (memory-guarded lean-guard, cone
+# table, fidelity phase, ATTESTATION marker). This script covers the
+# kernel-facing phases only: compile, #print-axioms audit, inventory
+# gate.
+# ─────────────────────────────────────────────────────────────────────────────
+set -euo pipefail
+HERE="$(cd "$(dirname "$0")" && pwd)"
+command -v lean >/dev/null || { echo "FATAL: no 'lean' on PATH (want $(cat "$HERE/lean-toolchain"))"; exit 1; }
+echo "toolchain: $(lean --version)"
+echo "pinned:    $(cat "$HERE/lean-toolchain")"
+
+export LEAN_PATH="${LEAN_PATH:+$LEAN_PATH:}$HERE/gen:$HERE"
+
+echo "=== compile (gen + 9 proof modules) ==="
+( cd "$HERE/gen" && lean -o LTLAcc/HashExternal.olean LTLAcc/HashExternal.lean )
+cd "$HERE"
+for m in Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore; do
+  echo "  · Proofs/$m"
+  lean -o "Proofs/$m.olean" "Proofs/$m.lean"
+done
+
+echo "=== axiom audit (#print axioms, compare against check.sh CONES yourself) ==="
+lean Proofs/AxiomCheck.lean | tee bare-axcheck.out | grep -c "depends on axioms\|does not depend" \
+  | xargs -I{} echo "  {} cone lines printed (full output: bare-axcheck.out)"
+
+echo "=== inventory gate (environment == allowlist) ==="
+lean Proofs/Inventory.lean > bare-inventory.out
+"$HERE/inventory_gate.sh" bare-inventory.out "$HERE/inventory-allowlist.txt"
+
+echo "=== BARE RUN GREEN (compile + axiom print + inventory gate) ==="
diff --git a/verification/selftest_audit.sh b/verification/selftest_audit.sh
index 8308cc7..1272d44 100755
--- a/verification/selftest_audit.sh
+++ b/verification/selftest_audit.sh
@@ -27,7 +27,9 @@
 # All Lean work goes through lean-guard (memory-capped, single-flight).
 # ─────────────────────────────────────────────────────────────────────────────
 set -euo pipefail
-source ~/aeneas-toolchain/env.sh
+AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
+[ -f "$AENEAS_ENV" ] || { echo "FATAL: Aeneas environment not found: $AENEAS_ENV"; exit 1; }
+source "$AENEAS_ENV"
 SRC="$(cd "$(dirname "$0")" && pwd)"
 AENEAS_LEAN="$AENEAS_HOME/backends/lean"
 CORES="${LEAN_MAX_CORES:-0-3}"