.gitignore

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

ATTESTATION-RUNBOOK.md

@@ -1,248 +0,0 @@
-# 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,30 +77,3 @@ 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,10 +40,6 @@ 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,119 +1,136 @@
-# Response to reviewers — round 4
+# Response to reviewers — round 3
 
-Corpus: `ltl-accumulator-verified`. Round-3 reviews received against the
+Corpus: `ltl-accumulator-verified`. Round-2 reviews received against the
-round-3 freeze `9972ab4`: GPT-5.6 (conditional approval, one portability
+round-2 freeze `260ad64` (GPT-5.6 second adversarial review; second
-finding) and the round-3 Claude reviewer's Socratic addendum (one new
+Claude round-2 findings). Every finding was independently re-verified
-confirmed finding, four reinstated ones). Every claim was independently
+against the corpus before any change; all confirmed findings are fixed
-re-verified by the operator before any change. This round contains ONE
+in this freeze. No theorem statement changed except the one interface
-new theorem, one harness family, and packaging/scoping fixes. No
+tightening both reviewers requested (L1/NEW-2).
-existing theorem statement or proof changed.
 
-## The headline: F1* (Claude addendum) — CONFIRMED and absorbed
+## Disposition of round-2 findings
 
-The addendum demonstrated that the deployed `verify_consistency` and
+### GPT H1 / Claude NEW-1 — coverage gate evadable (CONFIRMED, fixed structurally)
-the mechanized `ConsRec` acceptance are **not extensionally equal**:
-the deployed RFC 9162 iterative verifier accepts honest proofs under
-lied size claims (witness: `verify_consistency(1, 3, R2, R3, P(2→3)) =
-True`; ConsRec rejects). Reproduced exactly on the operator machine
-against deployed pacta: same witness, same 3,405 divergences for
-n < 60, same strictly one-sided direction (the mechanized model is the
-stricter; inclusion diverges nowhere under identical abuse), same
-power-of-two seeding mechanism in the deployed source.
 
-Absorbed as follows:
+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:
 
-- **KNOWN-GAPS gap 14**: full statement — witness, mechanism,
+- **`Proofs/Inventory.lean`** imports every corpus module and emits
-  one-sidedness, and the soundness-transfer side condition (the
+  EVERY constant whose originating module is a corpus module: fully
-  consumer's `(n₀, r₀)` is an authentic pinned pair and `n₁` is the
+  qualified name, declaration kind, and axiom cone. There is **no
-  authentic size behind `r₁`), which pacta's pin-store flow supplies by
+  filtering** — compiler-generated auxiliaries and `_private.*` mangles
-  construction. No exploitability against that flow is claimed or ruled
+  are emitted and pinned too, so there is no name shape that can hide.
-  out; that assessment belongs to the signature/STH layer (gap 4).
+  A corpus module missing from the import list is an elaboration error.
-- **Harness**: new lied-size family — 73,573 boundary cases (lied old
+- The axiom cone is computed by our own walker AND cross-checked
-  size exhaustive for n < 60, lied new size sampled), 3,867 expected
+  in-process against core `collectAxioms` (the machinery `#print axioms`
-  divergences PINNED, and the one-sided direction asserted on every
+  uses) for every constant — divergence is a hard error. (This caught a
-  case: a single `lean=True / deployed=False` instance fails the run.
+  real toolchain subtlety during development: `ConstantInfo.value?`
-  These families would have caught F1* in round 1; now they guard it
+  returns `none` for theorems on 4.30.0-rc2, which would have silently
-  forever.
+  truncated cones; the direct constructor match avoids it, and the
-- **Banner**: `FIDELITY GREEN` now reads "agreement over the pinned
+  cross-check would have refused to ship it.)
-  case families (not extensional equality; KNOWN-GAPS gap 14)". The
+- **`verification/inventory-allowlist.txt`** pins all 218 constants;
-  STATEMENT-MAP fidelity row and Theorem-3 row carry the same scoping.
+  **`inventory_gate.sh`** diffs environment vs allowlist fail-closed in
-- **No pacta code change.** The deployed behavior matches upstream
+  BOTH directions (UNCLASSIFIED / STALE), requires the INV-COUNT
-  RFC 9162 implementations; the consumer flow enforces the side
+  trailer (a truncated Lean run cannot pass as an empty diff), and
-  condition (`n₀` comes from the consumer's own pin, never from the
+  asserts the whole corpus contains exactly one axiom-kind constant:
-  peer; `(n₁, r₁)` arrive together in one signed head). pacta also
+  `LTLAcc.sha256`.
-  remains change-frozen during paper processing.
+- 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`).
 
-## F2 — `acceptCons` routed through zero theorems (CONFIRMED, fixed)
+### GPT H2 — fidelity target could not run (CONFIRMED, fixed)
 
-New theorem `acceptCons_sound` (Theorem3.lean): soundness stated over
+Reproduced exactly (`ModuleNotFoundError: pacta.postquantum`). The
-the named `acceptCons` predicate the harness tests — the consistency
+round-3 `pacta-fidelity-target` ships the complete **load-time import
-twin of round-2's `acceptIncl_sound`. The `n₀ = 0` disjunct is
+closure** of `pacta.transparency` (`__init__`, `transparency`,
-discharged from the non-prefix premise; the size bound `n₀ ≤ n₁` is
+`postquantum`, `signing`, `yamlio`) — all stdlib-only, so a bare
-derived from ConsRec acceptance itself via the new lemma
+Python 3 runs it with no pip installs — content-addressed in
-`consRec_some_le` (the `n₀ > n` branch returns `none`), so the caller
+`MANIFEST.sha256` against pacta commit `3d81d538…` with verification
-owes nothing beyond acceptance + wrong-prefix. Cones (read from
+instructions (`TARGET-PROVENANCE.md`). The kit includes the complete
-`#print axioms`, as always): `consRec_some_le` = [propext,
+terminal transcript AND exit code of `run_fidelity.py` executed from a
-LTLAcc.sha256, Quot.sound]; `acceptCons_sound` = [propext,
+clean extraction: exit 0, `230,271 + 230,016`, zero mismatches
-Classical.choice, LTLAcc.sha256, Quot.sound]. Both are in CONES,
+(`fidelity-clean-run-transcript.txt`), plus the full green `check.sh`
-AxiomCheck, and the inventory allowlist (218 → 222 constants; the diff
+transcript ending in `ATTESTATION GREEN` with fidelity not skipped
-is exactly the two theorems plus their two generated auxiliaries).
+(`check-transcript.txt`) — GPT release conditions 3 and 5.
 
-## F3 — Lean-side kit reproducibility (CONFIRMED, fixed)
+### GPT M1 — audit narrower outside Proofs/ (CONFIRMED, fixed)
 
-`verification/lean-toolchain` now pins `leanprover/lean4:v4.30.0-rc2`,
+- Orphan-olean guard is now recursive over the whole tree (it caught a
-and `verification/run_bare.sh` is the reviewer's standalone runner:
+  stray development artifact on its first run).
-plain public `lean`, no lake, no Aeneas checkout — compile all modules,
+- gen/ has the same unmanifested-source ("dead file") check as Proofs/.
-print all cones, run the inventory gate. Verified green on this machine
+- The axiom surface is pinned corpus-wide twice: textually (exactly one
-(under the operator's memory-cap discipline): 61 cone lines, 222
+  `axiom` line under gen/, none under Proofs/) and semantically (the
-constants, gate green. check.sh remains the operator's button.
+  inventory admits exactly one axiom-kind constant anywhere).
+- Declaration discovery under gen/ now goes through the environment
+  inventory like everything else.
 
-## F4 — regex metacharacters in Phase 3b (CONFIRMED, fixed)
+### GPT M2 — stale fidelity counts in STATEMENT-MAP (CONFIRMED, fixed)
 
-The `PINNED BUT NOT INVENTORIED` check now uses awk field equality
+The row now reads 230,271 + 230,016 with the expanded families named.
-instead of a regex containing the constant name; the module-manifest
+Process note: the round-2 Claude review certified this row as already
-greps were already `-F`. Dots no longer act as wildcards anywhere in
+fixed; it was not. Consistent with this project's experience, "verified"
-the gate.
+claims by reviewers are themselves re-verified now.
 
-## F5 — kit hygiene (CONFIRMED, fixed; one sharpening)
+### GPT M3 — "not choice-dischargeable" overclaims (CONFIRMED, fixed)
 
-The stray `.pyc` was worse than reported: it was **git-tracked**, which
+STATEMENT-MAP now uses (essentially) GPT's safer wording: the guards
-is why `git archive` shipped it. Untracked; `__pycache__/`/`*.pyc`
+show each named extractor returns a non-collision on at least one
-gitignored. The round-4 kit gives the corpus tarball the same treatment
+canonical honest input, ruling out the globally-inhabited-existential
-as the pacta target: `MANIFEST.sha256` over every file in the archive
+degeneration; they do NOT establish logical dependence on every
-plus the pinned public commit and repo URL — this also implements
+hypothesis, nor exclude other classical arguments on restricted domains.
-GPT's governance condition (publish hashes of the audit-critical
-files; they are all in the archive the manifest covers).
 
-## GPT §7 — hard-coded toolchain bootstrap (CONFIRMED, fixed)
+### GPT L1 / Claude NEW-2 — redundant `hm` in `acceptIncl_sound` (CONFIRMED, fixed)
 
-`AENEAS_ENV` override with a clear FATAL message in both check.sh and
+The hypothesis is gone; the range fact is derived from `hacc.1`, so the
-selftest_audit.sh, exactly as recommended; default unchanged for the
+theorem is stated purely in terms of acceptance + wrong-leaf premise.
-operator. Together with F3 this closes the "reviewer-friendly
+Cone unchanged (`propext, Classical.choice, LTLAcc.sha256, Quot.sound`),
-push-button" gap: reviewers get `run_bare.sh`, operators keep the
+re-verified by `#print axioms` and the inventory.
-guarded button.
 
-## GPT §9 — paper-language conditions
+### GPT ledger additions (adopted, as history)
 
-Adopted into the paper-cycle queue verbatim (they overlap the queue
+KNOWN-GAPS gains gap 12 (audit-gate lineage: the round-2 gate was
-built across rounds 1–3), plus F1*'s two additions: the fidelity
+evadable, what replaced it, and the residual limits of an
-sentence must say "finite differential testing over pinned families,
+environment-derived inventory — it cannot see never-compiled source,
-extensional equality is false for consistency (one-sided)", and
+which the dead-file checks cover, nor defeat a hostile toolchain) and
-Theorem 3's deployment claim must carry the pinned-pair side condition.
+gap 13 (the round-2 kit's fidelity target was not self-contained).
-The paper is edited in its own cycle, not in this corpus.
 
-## Reviewer-process note (kept, per this project's candor convention)
+## Found in round-3 self-review (neither reviewer caught)
 
-The round-3 Claude reviewer's self-analysis (Q1–Q7) found its own
+- **README layer table was still stale at `260ad64`**: L4 carried
-"confirmed/verified" inflations and then did what the drill demands:
+  "queued for S4 restoration" and the pin-store row said "pending",
-applied constructive-witness standards to its own strongest doubt and
+  despite round-1 F2 being certified as fixed by the round-2 Claude
-produced F1*. Its round-3.5 addendum is the strongest single review
+  review. The table now matches the frozen state (all layers done,
-artifact this corpus has received. The operator re-verified every claim
+  L4 explicitly "done as specializations" per gap 3).
-in it anyway — trust nothing, including good news.
+- 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.
 
 ## What did NOT change
 
-All pre-existing theorem statements and proofs; the axiom boundary
+All theorem statements and proofs except the `acceptIncl_sound`
-(single opaque `sha256`); the 230,271/230,016 family pins; the live
+signature tightening; the axiom boundary (single opaque `sha256`); the
-transparency log (12 leaves, root `bcd15f9d…`); deployed pacta.
+pinned CONES table (59 entries, all cones byte-identical to round 2);
-Attestation remains blocked pending the ePrint decision, the author's
+the fidelity counts. The live transparency log remains frozen at
-read, and an explicit operator order.
+12 leaves (root `bcd15f9d…`) and is untouched by this round;
+attestation remains blocked pending the ePrint decision, author
+review, 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); `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) |
+| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged) | 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 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) |
+| 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) |
 
 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,5 +68,3 @@ 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,41 +78,4 @@ 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,11 +9,7 @@
 #         2 compile manifest · 3 boundary-exact axiom audit
 # ─────────────────────────────────────────────────────────────────────────────
 set -euo pipefail
-# Toolchain bootstrap is overridable for reviewers with their own install
+source ~/aeneas-toolchain/env.sh
-# (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}"
@@ -90,8 +86,6 @@ 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,
@@ -231,11 +225,8 @@ 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
-  awk -F'|' -v n="$cert" '$1=="INV" && $2==n {found=1} END {exit !found}' \
+  grep -q "^INV|$cert|" "$HERE/inventory-allowlist.txt" || {
-      "$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,12 +9,8 @@ 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 — and extensional
+a proof of extensional equality over all inputs; the Lean-to-Python
-equality is in fact FALSE for consistency: the lied-size family below
+bridge remains trusted quoted-source inspection (see KNOWN-GAPS).
-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.
@@ -38,11 +34,6 @@ 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):
@@ -109,74 +100,17 @@ 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
-    assert (tl, dl) == (LIED_PIN_TOTAL, LIED_PIN_DIV), (tl, dl)
+    print(f"  PINNED: inclusion={ti} (230,271)  consistency={tc} (230,016)")
-    print(f"  PINNED: inclusion={ti} (230,271)  consistency={tc} (230,016)  lied-sizes={tl}/{dl}")
+    print("=== FIDELITY GREEN: mechanized defs agree with deployed verifier ===")
-    print("=== FIDELITY GREEN: agreement over the pinned case families "
-          "(not extensional equality; KNOWN-GAPS gap 14) ===")
 
 
 if __name__ == "__main__":

verification/inventory-allowlist.txt

@@ -15,59 +15,20 @@
 #
 # 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.acceptIncl|def|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.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
@@ -80,44 +41,38 @@ 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.consRecBinding.match_1|def|
+INV|LTLAcc.ConsRec.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRecBinding|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.ConsRec.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_1|def|propext
+INV|LTLAcc.ConsRec.induct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_2|def|propext
+INV|LTLAcc.ConsRec.match_1|def|
-INV|LTLAcc.consRec_base_false_eq.match_1|def|propext
+INV|LTLAcc.ConsRec._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRec_base_false_eq|theorem|Classical.choice,Quot.sound,propext
+INV|LTLAcc.ConsRec._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRec_base_true_eq.match_1|def|propext
+INV|LTLAcc.ConsRec._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.consRec_base_true_eq|theorem|propext
+INV|LTLAcc.ConsRec._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.consRec_some_le._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.ConsRec._unary._proof_2|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._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractConsNode|def|LTLAcc.sha256,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|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractCons_correct._proof_1_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractCons_correct._proof_1_3|theorem|Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.extractCons_correct_paper._proof_1_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractConsNode._unary._proof_2|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.extractCons_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractCons|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractCons_nonvacuous._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractIncl|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractIncl_correct|theorem|Classical.choice,LTLAcc.sha256,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
@@ -126,18 +81,17 @@ 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_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractIncl_nonvacuous._proof_1_2|theorem|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|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl_nonvacuous._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH._unary._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.extractIncl._unary|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH._unary._proof_2|theorem|Quot.sound,propext
+INV|LTLAcc.extractIncl._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext
-INV|LTLAcc.extractMTH._unary|def|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH_correct|theorem|Classical.choice,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
@@ -145,72 +99,114 @@ 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_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
+INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.extractMTH_nonvacuous._proof_1_2|theorem|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|def|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.fork_distinct|theorem|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.getD_drop._proof_1_1|theorem|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_take._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.getD_take._proof_1_2|theorem|Quot.sound,propext
-INV|LTLAcc.getD_take|theorem|Quot.sound,propext
+INV|LTLAcc.Hash|def|
 INV|LTLAcc.hleaf|def|LTLAcc.sha256
-INV|LTLAcc.hnode_preimage_inj|theorem|propext
 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.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.incl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.instDecidableEqHash._proof_1|theorem|
 INV|LTLAcc.instDecidableEqHash|def|
-INV|LTLAcc.instInhabitedHash._proof_1|theorem|propext
+INV|LTLAcc.instDecidableEqHash._proof_1|theorem|
 INV|LTLAcc.instInhabitedHash|def|propext
-INV|LTLAcc.kbelow._proof_1|theorem|Quot.sound,propext
+INV|LTLAcc.instInhabitedHash._proof_1|theorem|propext
-INV|LTLAcc.kbelow._unsafe_rec|def|
+INV|LTLAcc.IsCollision|def|LTLAcc.sha256
+INV|LTLAcc.kbelow|def|Quot.sound,propext
 INV|LTLAcc.kbelow.eq_1|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow.eq_def|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow_eq_of_pow2_between|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_eq_of_pow2_between|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext
+INV|LTLAcc.kbelow_lt|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._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.kbelow_prefix_eq|theorem|Quot.sound,propext
-INV|LTLAcc.kbelow|def|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.le_two_kbelow._proof_1_3|theorem|Quot.sound,propext
 INV|LTLAcc.le_two_kbelow._proof_1_4|theorem|Quot.sound,propext
-INV|LTLAcc.le_two_kbelow|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.pinAccept_monotone._proof_1_1|theorem|Quot.sound,propext
 INV|LTLAcc.pinAccept_monotone._proof_1_2|theorem|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.pinExtract|def|LTLAcc.sha256,Quot.sound,propext
-INV|LTLAcc.pin_prefix_correct._proof_1_2|theorem|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.pin_prefix_nonvacuous._proof_1_2|theorem|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_nonvacuous._proof_1_2|theorem|Quot.sound,propext
+INV|LTLAcc.pow2_exp_unique|theorem|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.pow2_exp_unique|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.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._proof_1_1|theorem|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|_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|
@@ -218,15 +214,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

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

verification/run_bare.sh

@@ -1,42 +0,0 @@
-#!/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,9 +27,7 @@
 # All Lean work goes through lean-guard (memory-capped, single-flight).
 # ─────────────────────────────────────────────────────────────────────────────
 set -euo pipefail
-AENEAS_ENV="${AENEAS_ENV:-$HOME/aeneas-toolchain/env.sh}"
+source ~/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}"