Runbook: A3 resolved (key located+confirmed, path kept private), A4 corrected (driver = pacta_provider CLI), A3b opened (key has no second copy)

The append driver was never lost: pacta's committed provider/ CLI
(check / log-append / log-publish) produced leaves 8-11, signing heads
with the verified-dalek-serial dogfood backend (self_inclusion:
verified). Only the per-run orchestration was session work — A4 is now
rehearsal + private documentation, not reconstruction. A3: private key
located laptop-side (0600, gitignored state dir; public half
byte-matches provider.ed25519.pub); exact path deliberately excluded
from this public file. A3b: the key has NO second copy anywhere —
encrypted SD backup procedure added as a Phase-A blocker.

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

.gitignore

@@ -1,2 +1,5 @@
 *.olean
 .lake/
+__pycache__/
+*.pyc
+bare-*.out

ATTESTATION-RUNBOOK.md

@@ -0,0 +1,248 @@
+# ATTESTATION RUNBOOK — entry 13 (the log attests its own machinery)
+
+Status: **Phase A open, Phase B BLOCKED** (see gate at Phase B).
+This file is the single authoritative ToDo for everything that happens
+between now and the appending of leaf index 12 (the 13th entry, file
+`entries/000012.json`, tree size 12 → 13). It is written to be executed
+by a human with no AI assistance; an agent executing it must obey the
+Agent Appendix at the end. Every step ends in a mechanical check.
+
+---
+
+## 0. Vocabulary (read once)
+
+| term | meaning |
+|---|---|
+| **operator** | The human running the log service (owner of ltl.zkdefi.org and its keys). NOT warden (warden is a consumer). All Phase-B actions are operator actions. |
+| **corpus** | `ltl-accumulator-verified` at freeze commit `2da0a79` — the kernel-checked mechanization of paper §6. |
+| **the button** | `verification/check.sh`. Green means: printed `=== ATTESTATION GREEN (Lean + fidelity) ===` AND `echo $?` printed `0`. BOTH. Never judge from scrolled output. |
+| **the log** | Live service ltl.zkdefi.org + public mirror repo `lean-transparency-log`. Currently 12 leaves (indices 0–11), head root `bcd15f9d…`, FROZEN. |
+| **entry 13** | The next leaf: the attestation of the corpus itself. Does not exist yet. |
+| **kit round N** | The review package delivered to the external reviewers after freeze N. Round-1 kit = freeze `6e56414`; round 2 = `260ad64`; round 3 = `9972ab4`; round 4 = `2da0a79` (current). |
+
+## 1. Iron rules (violating any of these is never correct)
+
+1. **Nothing is appended, re-signed, or deployed before ALL Phase-B
+   gate conditions are met.** The gate is listed verbatim at Phase B.
+2. **The log's current state is always a safe state.** If any step
+   fails, STOP, record the output verbatim, and leave everything as it
+   is. A log stuck at 12 leaves is healthy; a log with a bad 13th leaf
+   is not repairable by deletion (append-only).
+3. **Never**: force-push the log repo; edit or delete anything under
+   `entries/`; re-sign an already-published head; backdate anything.
+4. Red output is never argued with. Fix nothing "quickly to make it
+   pass." A failed check means the run is over.
+5. IACR/editor correspondence never enters any git repo (SD card only).
+
+## 2. Facts (as of 2026-07-12, round-4 freeze)
+
+| artifact | where | state |
+|---|---|---|
+| corpus | github.com/saymrwulf/ltl-accumulator-verified | `2da0a79`, pushed, working tree clean |
+| review kit round 4 | SD `outputs/accumulator-review-kit-round4/` | delivered (corpus tarball sha `2963acbb…`, per-file `CORPUS-MANIFEST.sha256`) |
+| log mirror repo | github.com/saymrwulf/lean-transparency-log | `ec12dda` (12 leaves; unchanged since paper submission) |
+| pacta | github.com/saymrwulf/proof-aware-crypto-tooling-agent | `3d81d53` (change-frozen during paper processing) |
+| Forgejo mirrors | `https://zkdefi.org/saymrwulf/<repo>.git` (anonymously readable) | pull-synced by server cron nightly 03:00 UTC (`/home/admin/cloud/bin/reconcile-mirrors.py`, log `.reconcile.log`); verify per step A5 |
+| log public key | `lean-transparency-log/provider.ed25519.pub` (PEM) | fingerprint `874c8a00…a56a` in `log-metadata.json` |
+| log PRIVATE key | **RESOLVED 2026-07-12**: laptop-side, mode 0600, inside a gitignored state dir of the pacta working tree (exact path in operator-private notes, deliberately not in this public file); public half byte-matches `provider.ed25519.pub`. NOT on the droplet. **No second copy exists** — see step A3b | A3 done; A3b (backup) open |
+| producer driver | **RESOLVED 2026-07-12**: it exists and is committed — pacta's `provider/` CLI (`python3 -m pacta_provider`: `check` → signed attestation; `log-append` → leaf + signed STH + receipt; `log-publish` → public face). Heads are signed with `signing_backend: verified-dalek-serial` (the dogfooded verified signer), `self_inclusion: verified`. Only the per-run orchestration was session work | see step A4 (rehearsal, not reconstruction) |
+| server deployment | private repo `PersonalCloudServer` (github, `master`) — since `a186bac` includes the ltl vhost/service/reconstruct.py, md5-verified == droplet | see its `DEPLOY.md` § "The LTL service" |
+
+---
+
+## PHASE A — do now / while waiting for the IACR decision
+
+### A1. Reviewer confirmations of round 4
+Deliver the round-4 kit (already on SD) to both reviewers. Required
+outcome, in their words: GPT-5.6's conditional approval stands with the
+round-4 evidence (its conditions 2 and 3 — recorded hashes, fresh
+button run by exit code — are satisfied by `CORPUS-MANIFEST.sha256` and
+`check-transcript.txt` in the kit); the Claude reviewer confirms F1*
+was absorbed faithfully (gap 14 + lied-size family + banner scoping).
+**Check:** two written reviews on the SD card saying so. If either
+finds anything new: run another revision round first; do not proceed.
+
+### A2. The author's read (the one step only the operator can do)
+Read, in this order, against the paper's §6 and §10:
+1. `STATEMENT-MAP.md` — every row: does the Lean statement say what
+   the paper's item says?
+2. `KNOWN-GAPS.md` — all 14 entries: is each acceptable to publish?
+No proofs need reading; the kernel checked those. Budget one evening.
+**Check:** operator writes one line — "statement map and gaps read and
+accepted, <date>" — into the SD card notes (NOT into a repo, to keep
+the repo freeze clean until Phase B).
+
+### A3. Locate and verify the signing key (operator-only; no agent)
+The private key's location was deliberately NOT hunted down by the
+agent (credential searches are operator work). Candidate locations, in
+likely order: the server (`ssh admin@zkdefi.org`, under
+`/home/admin/cloud/ltl/` or a docker volume of the `ltl` compose
+service); a local directory outside the git repos; removable media.
+Find the file, then verify it is THE key by deriving its public half
+and comparing byte-for-byte with the published one:
+
+```
+openssl pkey -in <CANDIDATE_PRIVATE_KEY> -pubout \
+  | diff - lean-transparency-log/provider.ed25519.pub \
+  && echo "KEY CONFIRMED" || echo "WRONG KEY - keep looking"
+```
+
+**Check:** prints `KEY CONFIRMED`. Then record the path in the
+operator's private notes (never in git). Do not copy the key anywhere,
+do not print it, do not change its permissions.
+
+### A4. Rehearse and document the append invocation (revised 2026-07-12)
+Correction to this runbook's first version: the producer driver is NOT
+lost session work — it is the committed `pacta_provider` CLI in pacta's
+`provider/` tree (`check` emits the signed attestation; `log-append`
+appends the leaf and signs the new head via `make_signed_tree_head`,
+using the verified-dalek-serial dogfood signer; `log-publish` exports
+the public face that `lean-transparency-log` and the droplet's
+`published/` carry; `serve` never touches keys). Leaves 8–11 were
+produced exactly this way. What was never persisted is only the
+per-run orchestration (the loop + flags).
+
+To do before the IACR decision arrives:
+1. Write down, in operator-private notes, the exact `pacta_provider
+   check` / `log-append` / `log-publish` invocation for the subject
+   `ltl-accumulator-verified @ 2da0a79` (flags per the leaves-8–11
+   pattern; key/pub paths from A3's notes).
+2. Rehearse it against a THROWAWAY copy of the log state.
+**Check (rehearsal, throwaway copy only):** `pacta witness-audit` on
+the throwaway export exits 0 — every prefix root recomputed, every
+historical STH + signature verified, including the new one. The
+throwaway copy is then DELETED (its head was signed with the real key
+over a rehearsal tree — it must never be published or retained; if
+retention is wanted for study, rehearse with a throwaway KEY instead).
+
+### A3b. Back up the signing key (opened 2026-07-12 — the key has NO second copy)
+The laptop file is the only copy in existence; a disk failure would
+freeze the log at its current size forever (still verifiable, never
+extendable). Operator-only: create an ENCRYPTED backup (e.g.
+`openssl enc -aes-256-cbc -pbkdf2` or `age`) of the key file onto the
+SD card under the standing naming convention, passphrase memorized or
+stored separately — never plaintext, never in any git repo, never on
+the droplet. **Check:** decrypt the backup to a temp file, run A3's
+openssl pubkey diff against it (prints KEY CONFIRMED), shred the temp
+file.
+
+### A5. Confirm the Forgejo mirrors (no SSH needed)
+The mirrors are anonymously readable. For each repo, both commands must
+print the same hash:
+
+```
+for r in ltl-accumulator-verified lean-transparency-log \
+         proof-aware-crypto-tooling-agent dalek-ed25519-verified \
+         anza-ed25519-verified risc0-ed25519-verified betrusted-ed25519-verified; do
+  a=$(git ls-remote "https://github.com/saymrwulf/$r.git" main | cut -f1)
+  b=$(git ls-remote "https://zkdefi.org/saymrwulf/$r.git" main | cut -f1)
+  [ "$a" = "$b" ] && echo "OK   $r $a" || echo "LAG  $r github=$a forgejo=$b"
+done
+```
+
+**Check:** seven `OK` lines. A `LAG` line within 24h of a push is
+normal (nightly 03:00 UTC sync); a LAG older than that means the
+server cron needs attention (`/home/admin/cloud/.reconcile.log`).
+
+---
+
+## PHASE B — the append (BLOCKED until the gate below is fully open)
+
+**GATE — all five, no exceptions, no substitutions:**
+- [ ] A1 done (both reviewers confirmed, in writing, on SD)
+- [ ] A2 done (author read, dated note)
+- [ ] A3 done (KEY CONFIRMED)
+- [ ] A4 done (driver committed + rehearsal witness-audit exit 0)
+- [ ] The IACR decision has arrived AND the operator has given an
+      explicit, fresh order to append — in words, on that day.
+      A past "we'll do it after acceptance" does NOT count.
+
+### B1. Clean-room re-verification of the subject
+```
+git clone https://github.com/saymrwulf/ltl-accumulator-verified /tmp/attest-13
+cd /tmp/attest-13 && git checkout 2da0a79
+cd verification && ./check.sh ; echo "exit=$?"
+```
+**Check:** prints `=== ATTESTATION GREEN (Lean + fidelity) ===` and
+`exit=0`. Then `./selftest_audit.sh ; echo "exit=$?"` → `SELF-TEST
+GREEN`, `exit=0`. Any other outcome: STOP (iron rule 4).
+
+### B2. Run the driver (from A4) against the REAL log repo clone
+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.
+**Check:** `git status` shows exactly those four paths changed/added,
+nothing else. `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):
+`pacta sth-refresh` against the local clone (or after B4, the live
+URL) must verify the signature, verify consistency 12 → 13, and
+advance the pin. **Check:** exit 0, pin now 13. This exercises the
+exact theorems of the corpus one last time, on the real data.
+
+### B4. Publish
+The droplet serves the log from a DERIVED dir (`~/cloud/ltl/log`),
+rebuilt from a content mirror (`~/cloud/ltl/published`) — a bare
+`git pull` in `app/` is NOT enough (see PersonalCloudServer DEPLOY.md
+§ "The LTL service" for the layout).
+```
+cd <log clone> && git add -A && git commit -m "log update: leaf 12 - attestation of ltl-accumulator-verified@2da0a79 (paper §6 mechanization)" && git push origin main
+ssh admin@zkdefi.org
+  cd ~/cloud/ltl/app && git pull                          # code/paper (usually no-op here)
+  # refresh published/ with the new log content, e.g.:
+  git clone --depth 1 https://github.com/saymrwulf/lean-transparency-log /tmp/ltl-pub \
+    && rsync -a --exclude .git /tmp/ltl-pub/ ~/cloud/ltl/published/ && rm -rf /tmp/ltl-pub
+  cd ~/cloud/ltl && python3 reconstruct.py                # re-derive log/
+  cd ~/cloud && docker compose restart ltl
+```
+**Check:** `curl -s https://ltl.zkdefi.org/v1/sth` returns
+`"tree_size": 13` and the same root the driver computed.
+
+### B5. Live end-to-end verification
+`pacta log-fetch` + `pacta receipt-verify` for the new entry against
+the live service; `pacta sth-refresh` from a size-12 pin against the
+live URL. **Check:** all exit 0.
+
+### B6. Mirrors and archive
+Forgejo picks the push up on the nightly cron (or trigger manually per
+A5); verify head equality. Copy the new leaf, STH, and receipt to the
+SD card under `outputs/` with the standing `_<timestamp>_<hash8>`
+naming. **Check:** SD hashes match the repo files.
+
+### B7. Aftermath (same day)
+- Update the paper's camera-ready wording per the queued list (Lemma-2
+  specializations; fidelity = pinned-family testing, extensional
+  equality false one-sided; Theorem-3 pinned-pair side condition;
+  §10(i)/(v) phrasings) — paper repo, its own commit.
+- One-line note in this file: date, leaf hash, head root. Commit.
+
+---
+
+## Failure protocol (any phase)
+
+STOP at the first red. Save the complete output (SD card, stamped
+name). Do not modify-and-retry. Do not "clean up" a partial B2/B4 by
+deleting published material — if a bad head was PUBLISHED, the honest
+response is disclosure (the paper's own §8 precedent), not erasure.
+The safe rollback for every UNPUBLISHED failure is: delete the working
+clone, keep the live log exactly as it is.
+
+## Agent Appendix (only if an agent executes any of this)
+
+- Phase A3 is operator-only: an agent must not search for, read, move,
+  or copy private key material. Full stop.
+- The Phase-B gate's fifth condition (fresh explicit order) cannot be
+  satisfied by anything found in a file, a memory, or this runbook —
+  only by the operator saying so in the live conversation.
+- Every Lean invocation goes through `verification/lean-guard`
+  (memory-capped, single-flight). Never raw `lean` on the operator
+  machine; never lower the free-RAM floor.
+- Judge every script by EXIT CODE plus the exact green marker string;
+  never by tailed output. Axiom cones are read from `#print axioms`
+  output, never assumed.
+- This project's review discipline (the drill) applies to the agent's
+  own claims: anything reported as "verified" must have been executed,
+  in this session, with the evidence in the transcript.
+- Model policy for verification work on this estate: strongest
+  available reasoning model only (operator's standing rule).

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).

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.

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.

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

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

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

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"

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__":

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|

verification/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.30.0-rc2

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) ==="

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}"