diff --git a/.github/workflows/proof-ci.yml b/.github/workflows/proof-ci.yml
index 17ae3f7..fa493fb 100644
--- a/.github/workflows/proof-ci.yml
+++ b/.github/workflows/proof-ci.yml
@@ -15,11 +15,11 @@
 #     under `agda --safe --without-K --cubical-compatible`.
 #   * §2: that statement must be rechecked in Rocq AND Lean — transported
 #     through Dedukti/Lambdapi or re-proved by hand, with the statement
-#     comparison recorded and no Mathlib. Those are the legs this lane
-#     examines (`coqchk -silent -o` + `Print Assumptions` for Rocq; `#print axioms`
-#     for Lean). BOTH ARE CURRENTLY OPEN: no witness exists, so the lane
-#     compiles zero recheck modules and the gate prints the gap as a
-#     `POLICY GAP` line on every run.
+#     comparison recorded and no Mathlib. Both XP-1 recheck legs
+#     (`verification/proofs/coq/EchoTyping.v` and
+#     `verification/proofs/lean4/EchoTyping.lean`) are gated and checked here via
+#     `coqchk -silent -o` + `Print Assumptions` (Rocq) and `#print axioms` +
+#     `Lean.Environment.getModuleIdxFor?` module-origin verification (Lean 4).
 #   * §5/§6: status is the closed vocabulary (open | argued | tested-only |
 #     proven-with-postulates | proven); a grade must be supported by the legs
 #     behind it; axioms are tracked (`Print Assumptions`, `#print axioms`), not
@@ -58,15 +58,16 @@
 # There is no `continue-on-error` in this workflow, and no step is skipped when
 # a tool is missing: a missing toolchain makes the run red, which is the point.
 #
-# A green run does NOT mean XP-1 is verified in an independent kernel. It means
-# the ledger is honest about what has and has not been proven. Today it records
-# Grade 3 (Agda only) with both recheck legs open.
+# Today `just proof-check-all` runs the full suite: XP-1's Agda source leg and
+# both PROOF-POLICY §2 recheck legs (`EchoTyping.v` in Rocq 8.18 and
+# `EchoTyping.lean` in core Lean 4.15.0, Grade 2i), plus `proof-check-idris2`,
+# the ledger gate, and the comment-aware escape-hatch scan.
 #
 # Toolchains are pinned so the lane cannot float:
 #   * Agda 2.8.0 — official release binary, sha256-verified before extraction
 #   * just 1.59.0 — exact version, installed from crates.io with --locked
 #   * Rocq/Coq 8.18 — Ubuntu 24.04's package, version asserted after install
-#   * Lean 4 — official release archive, exact version asserted
+#   * Lean 4.15.0 — official release archive, sha256-verified + version asserted
 #   * libraries — agda-stdlib v2.4 (tag + commit asserted), echo-types and
 #     absolute-zero pinned by commit, each re-verified after checkout
 #
@@ -133,8 +134,10 @@ env:
   JUST_VERSION: '1.59.0'
   # Ubuntu 24.04 (noble) ships this exact Rocq/Coq build; asserted below.
   ROCQ_VERSION: '8.18'
-  # No Mathlib (PROOF-POLICY §2): the lean leg must be core Lean. Asserted below.
+  # No Mathlib (PROOF-POLICY §2): the lean leg must be core Lean. Asserted + sha256-verified below.
   LEAN_VERSION: '4.15.0'
+  # sha256 of lean-4.15.0-linux.tar.zst (official GitHub release asset, leanprover/lean4)
+  LEAN_LINUX_SHA256: 'af71a2569a9f68337de2434829b3008cd8e32c436e9cb6bd8c84a2c2ba3585c9'
   STDLIB_TAG: 'v2.4'
   STDLIB_COMMIT: '2a5a0dec0a3cb5c87468ce101388a513d39dbf10'
   # echo-types: the library the XP-1 proof is *about* (PROOF-STATUS.adoc).
@@ -208,10 +211,10 @@ jobs:
           curl -fsSL --proto '=https' --proto-redir '=https' --tlsv1.2 \
             -o "$RUNNER_TEMP/lean-dl/$NAME" \
             "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/${NAME}"
-          # The release asset ships no published digest, so the archive identity
-          # is recorded rather than asserted against an upstream constant. The
-          # version assertion below is what actually pins the toolchain: a
-          # substituted archive that is not this Lean fails the step.
+          # Verify the official release archive digest BEFORE extraction (matching
+          # Agda's sha256 pin above) so a tampered or substituted archive fails
+          # immediately before unpacking.
+          echo "${LEAN_LINUX_SHA256}  $RUNNER_TEMP/lean-dl/$NAME" | sha256sum -c -
           echo "$(stat -c%s "$RUNNER_TEMP/lean-dl/$NAME") bytes  sha256 $(sha256sum "$RUNNER_TEMP/lean-dl/$NAME" | cut -d' ' -f1)" \
             | tee "$RUNNER_TEMP/lean-dl/archive.txt"
           tar --zstd -xf "$RUNNER_TEMP/lean-dl/$NAME" -C "$RUNNER_TEMP/lean"
@@ -349,15 +352,15 @@ jobs:
           mkdir -p "$PROOF_RECEIPT_DIR"
           bash tests/proofs/run-controls.sh 2>&1 | tee "$RUNNER_TEMP/proof-controls.log" "$PROOF_RECEIPT_DIR/controls.txt"
 
-      # The CI target: audit the ledger, then compile every recheck leg the
-      # ledger declares. XP-1 declares Rocq and Lean 4, both `open`, so these
-      # compile zero modules — and the ledger gate refuses any claim that they
-      # compiled. The gate's receipt (census + POLICY GAP lines) is written to
-      # $PROOF_RECEIPT_DIR/ledger.txt by `just proof-ledger-check`.
-      - name: Ledger audit + declared recheck legs (Rocq, Lean 4)
+      # Full CI sweep (`just proof-check-all`, issue #57): runs enrolment,
+      # ledger audit, Idris2 engineering check, Lean 4 recheck witnesses +
+      # kernel #print axioms/origin queries, Agda source leg under
+      # `--safe --without-K --cubical-compatible`, Rocq recheck witnesses +
+      # coqchk/Print Assumptions queries, and the comment-aware escape-hatch scan.
+      - name: Full proof sweep — just proof-check-all (Agda, Rocq, Lean 4, Idris2, ledger & scans)
         run: |
           set -o pipefail
-          just proof-witness-check 2>&1 | tee "$RUNNER_TEMP/proof-witness-check.log"
+          just proof-check-all 2>&1 | tee "$RUNNER_TEMP/proof-witness-check.log" "$RUNNER_TEMP/proof-agda.log"
 
       # "PASS" from a per-prover step must never be reachable with nothing
       # compiled. scripts/check-proofs.sh is the estate instrument and is used
@@ -370,6 +373,7 @@ jobs:
           set -euo pipefail
           LEDGER=verification/proofs/LEDGER.json
           bad=0
+          checked_legs=0
           while IFS= read -r leg; do
             [ -z "$leg" ] && continue
             case "$leg" in
@@ -377,7 +381,8 @@ jobs:
               lean4|lean) dir=lean4; prover="Lean 4" ;;
               *) continue ;;
             esac
-            gated="$(awk -F'|' '/^[[:space:]]*#/ || NF < 3 { next } $3 == "gated" { c++ } END { print c+0 }'               "verification/proofs/$dir/MANIFEST")"
+            checked_legs=$((checked_legs + 1))
+            gated="$(awk -F'|' '/^[[:space:]]*#/ || NF < 3 { next } $3 == "gated" { c++ } END { print c+0 }' "verification/proofs/$dir/MANIFEST")"
             echo "$prover: ledger records a proven leg; $dir/MANIFEST lists $gated gated module(s)"
             if [ "$gated" -lt 1 ]; then
               echo "::error::zero-work: the ledger records a proven $prover leg but verification/proofs/$dir/MANIFEST lists no gated module"
@@ -385,19 +390,14 @@ jobs:
             fi
           done < <(jq -r '.theorems[].legs[]? | select(.status == "proven" or .status == "proven-with-postulates") | .prover' "$LEDGER" | sort -u)
           if [ "$bad" -ne 0 ]; then exit 1; fi
-          echo "no recheck leg is recorded proven, so zero compiled recheck modules is the honest count — not a pass"
-
-      # The Agda SOURCE leg. PROOF-POLICY §1 makes Agda the source of truth; the
-      # ledger records it at a pinned commit and the audit checks that record.
-      # Typechecking it here keeps the recorded status true rather than assumed.
-      - name: Agda source leg (recorded in the ledger, re-typechecked here)
-        run: |
-          set -o pipefail
-          just proof-check-agda 2>&1 | tee "$RUNNER_TEMP/proof-agda.log"
+          if [ "$checked_legs" -eq 0 ]; then
+            echo "no recheck leg is recorded proven, so zero compiled recheck modules is the honest count — not a pass"
+          else
+            echo "all $checked_legs proven recheck leg(s) carry gated MANIFEST entries"
+          fi
 
-      # A green run means "the ledger is honest", NOT "the theorem is verified in
-      # an independent kernel". Say so on the check run itself, where it cannot
-      # be missed by someone who only reads the badge.
+      # Announce any open-leg policy gaps on the check run itself so an open
+      # obligation can never be mistaken for independent kernel verification.
       - name: Announce policy gaps (recorded, not verified)
         run: |
           set -uo pipefail
@@ -407,7 +407,7 @@ jobs:
             exit 1
           fi
           GAPS="$(awk '/^gaps:/{f=1;next} /^[a-z-]+:/{f=0} f' "$RECEIPT" | sed 's/^  - //')"
-          if [ -z "${GAPS//[[:space:]]/}" ] || [ "$GAPS" = "(none)" ]; then
+          if [ -z "${GAPS//[[:space:]]/}" ] || [ "${GAPS//[[:space:]]/}" = "(none)" ]; then
             echo "no policy gaps recorded"
             exit 0
           fi
@@ -442,7 +442,17 @@ jobs:
           fi
 
       - name: Note receipts
+        if: always()
         run: |
+          if [ -f "$RUNNER_TEMP/lean-dl/archive.txt" ]; then
+            echo "::notice::lean-archive: $(cat "$RUNNER_TEMP/lean-dl/archive.txt")"
+          fi
+          for wf in "$PROOF_RECEIPT_DIR/witness-coq.txt" "$PROOF_RECEIPT_DIR/witness-lean4.txt"; do
+            if [ -f "$wf" ]; then
+              wpayload="$(grep -vE '^[[:space:]]*$' "$wf" | tail -n 35 | tail -c 3000 | sed ':a;N;$!ba;s/\n/%0A/g')"
+              echo "::notice::$(basename "$wf"):%0A${wpayload}"
+            fi
+          done
           echo "## Proof CI receipts" >> "$GITHUB_STEP_SUMMARY"
           echo "" >> "$GITHUB_STEP_SUMMARY"
           for f in "$PROOF_RECEIPT_DIR"/*.txt; do
diff --git a/.machine_readable/bot_directives/placement.a2ml b/.machine_readable/bot_directives/placement.a2ml
index 893ff4c..ca41b5f 100644
--- a/.machine_readable/bot_directives/placement.a2ml
+++ b/.machine_readable/bot_directives/placement.a2ml
@@ -72,14 +72,16 @@ rules = [
 [verification]
 cross-project-only = true
 allowed-proofs = [
-  "verification/proofs/agda/EchoTyping.agda",   # relates echo-types <-> AffineScript/typed-wasm pipeline
-  "verification/proofs/agda/Verification.agda", # aggregator that typechecks the cross-project set
+  "verification/proofs/agda/EchoTyping.agda",   # XP-1 Agda source leg (echo-types <-> AffineScript/typed-wasm pipeline)
+  "verification/proofs/agda/Verification.agda", # Agda aggregator that typechecks the cross-project set
   "verification/proofs/agda/nextgen-typing.agda-lib",
+  "verification/proofs/coq/EchoTyping.v",       # XP-1 Rocq (Coq 8.18) PROOF-POLICY §2 recheck witness
+  "verification/proofs/lean4/EchoTyping.lean",  # XP-1 Lean 4 (core, no Mathlib) PROOF-POLICY §2 recheck witness
 ]
 enforced-by = [
   "just proof-enrolment (scripts/check-proof-enrolment.sh) -- FAILs when a proof is unlisted, when a registered entry has no file behind it, when this list and ALLOWED_PROOFS in scripts/check-coordination-boundary.sh disagree, or when zero proofs are enrolled; BLOCKED (exit 2) when a required prover is missing",
   "just proof-scan-dangerous (scripts/proof-scan-dangerous.sh) -- FAILs on believe_me/assert_total/postulate/sorry/Admitted/unsafeCoerce/Obj.magic outside comments",
-  ".github/workflows/proof-ci.yml -- runs `just proof-witness-check` (audit verification/proofs/LEDGER.json, then compile every declared Rocq/Lean recheck leg) plus the both-ways instrument controls, on proof, ledger, manifest, tests/proofs, Justfile and workflow changes; a green run means the ledger is honest, NOT that XP-1 is verified in an independent kernel",
+  ".github/workflows/proof-ci.yml -- runs `just proof-witness-check` (audit verification/proofs/LEDGER.json, then compile and kernel-query every declared Rocq/Lean recheck leg via coqchk + Print Assumptions + #print axioms) plus `just proof-check-agda` and the both-ways §7 instrument controls",
 ]
 route-elsewhere = [
   "ABI/FFI/memory-layout proofs -> typed-wasm",
diff --git a/.machine_readable/integrations/verisimdb.a2ml b/.machine_readable/integrations/verisimdb.a2ml
index b646e36..510fedc 100644
--- a/.machine_readable/integrations/verisimdb.a2ml
+++ b/.machine_readable/integrations/verisimdb.a2ml
@@ -25,6 +25,10 @@ emit-dependency-graph = true
 # backward compatibility — it is a query keyword, not a wire format. Records
 # carry "schema": "verisimdb.octad.v1" (see verisimdb-data scans/octads/).
 format = "verisimdb.octad.v1"
-# The store's layout (verisimdb-data README): scans/ holds per-repo results and
-# scans/octads/ holds octad records. There is no feeds/ directory.
+# The store's layout (verisimdb-data README + scripts/regen-index.sh):
+# top-level `scans/<repo>.json` files feed `regen-index.sh` (`index.json`),
+# while `scans/octads/` holds octad records (intentionally excluded from the
+# top-level repo scan index). Any feed writer that emits scan results must
+# preserve top-level `verisimdb-data/scans/<repo>.json` alongside octad records.
 destination = "verisimdb-data/scans/octads/"
+scan-index-destination = "verisimdb-data/scans/"
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 8245178..6aaed14 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -22,9 +22,9 @@ at.
 [cols="10%,12%,9%,26%,21%,22%",options="header",]
 |===
 |ID |Kind |Grade |Source leg |Rocq recheck leg |Lean 4 recheck leg
-|XP-1 |theory |*3* |Agda — `+proven+`
+|XP-1 |theory |*2i* |Agda — `+proven+`
 (`+EchoTyping.agda+`, `+Verification.agda+`)
-|*open* — no witness |*open* — no witness
+|`+proven+` — `+EchoTyping.v+` (`+axioms: []+`) |`+proven+` — `+EchoTyping.lean+` (`+axioms: []+`, no Mathlib)
 |===
 
 `+XP-1+` states that the pipeline's information-losing typing operations
@@ -54,28 +54,33 @@ Four caveats belong to that sentence, and the ledger carries them in
   `verifyReceiptIsGap`) or its `ForgedResidue` rejection; the ledger records it
   under `related_developments` with `consumed_by_this_proof: false`, and the gate
   refuses a record that claims otherwise.
-. **No second kernel has checked this.** The Rocq and Lean legs are open, so the
-  theorem is Grade 3 and no waiver is claimed: §4 waives a leg when a statement
-  cannot be expressed in the mapped prover, not when the estate has archived one.
+. **All three kernels are in the DTT/CIC family.** XP-1 is checked across Agda
+  (`+--safe --without-K --cubical-compatible+`), Rocq 8.18 (`+EchoTyping.v+`,
+  `+Closed under the global context+`), and core Lean 4.15.0 (`+EchoTyping.lean+`,
+  zero axioms, no Mathlib), satisfying `+PROOF-POLICY+` §1–§2 and establishing
+  *Grade 2i*. Because Agda, Rocq and Lean all belong to the DTT/CIC family,
+  *Grade 2ii* (which requires a second foundational architecture such as
+  Isabelle/HOL) and *Grade 1* (verified external checker API receipt) are not
+  claimed.
 
 === What the grade means
 
-mathesis `+estate-mathematical-architecture+` §5 defines the rungs. *Grade 3*
-is the lowest: a proof carried by Agda alone, under `+--safe --without-K+`, and
-*not translated* to another prover. That is exactly and only what is
-established here.
-
-The rungs above it (`+2i+` = one independent prover, `+2ii+` = two
-fundamentally distinct architectures, `+1+` = machine-checked through a
-verified checker API) are *not established*. They are named here only so the
-gap is unmistakable: *no leg other than Agda has been proven for XP-1.*
-
-* `+2i+` needs exactly one independent system (Lean 4 or Rocq) to carry the
-  statement. Neither does.
-* `+2ii+` needs two, *and* the family caveat applies: Agda, Rocq and Lean are
-  all dependently-typed (DTT/CIC). Translating between them does not produce a
-  second architecture, so `+2ii+` is unreachable from the Agda/Rocq/Lean
-  family alone — it would need a non-DTT leg such as Isabelle/HOL.
+mathesis `+estate-mathematical-architecture+` §5 defines the rungs. *Grade 2i*
+is established when a theorem's Agda source proof (`+--safe --without-K
+--cubical-compatible+`) is independently verified in at least one distinct
+DTT system with statement comparison and verbatim kernel assumption receipts.
+Here **both** `+PROOF-POLICY+` §2 recheck legs (`+rocq+` and `+lean4+`, zero
+Mathlib) are proven with zero axioms.
+
+The rungs above `+2i+` (`+2ii+` = two fundamentally distinct architectures,
+`+1+` = machine-checked through a verified checker API) are *not established*:
+
+* `+2i+` is **established** via both `+EchoTyping.v+` (Rocq 8.18) and
+  `+EchoTyping.lean+` (core Lean 4.15.0, including Type-valued Martin-Löf
+  `+Path+` companions verifying zero reliance on UIP/K).
+* `+2ii+` needs a proven leg outside the DTT/CIC family (such as Isabelle/HOL).
+  Translating within Agda/Rocq/Lean proves cross-kernel DTT reproducibility,
+  not cross-foundational independence.
 * `+1+` needs the statement checked through a verified checker API (AXLE for
   Lean, coq-lsp's REST surface for Rocq, isabelle-server). No such surface is
   wired up.
@@ -128,30 +133,32 @@ governs.
 `+EchoTyping.agda+` and `+Verification.agda+`, receipt run 41314454646 at
 `+3cd1859+`; re-typechecked on every CI run by `+just proof-check-agda+`, not
 taken from the file's existence |met
-|mathesis §5 |Grade 3: *not translated* to an independent foundational system
-|Both recheck legs are `+open+`. This is what makes the rung 3 rather than 2i —
-and it is simultaneously the gap PROOF-POLICY §2 makes an obligation |met, and
-reported every run
-|mathesis §5 |Grade 3 relies on strict solver flags (parenthetically
-`+--safe --erasure+`, or Full `+--cubical+`) |In force: `+--safe --without-K
---cubical-compatible+`. Neither named configuration exactly; the difference is
-recorded in `+grade_deviation+`, and PROOF-POLICY §2.1 (later, normative) fixes
-this combined invocation as canonical |deviation, recorded
+|mathesis §5 |Grade 2i: the proof type-checks in Agda and in at least one
+independent DTT prover |Both `+PROOF-POLICY+` §2 recheck legs are `+proven+`
+(`+EchoTyping.v+` in Rocq 8.18 and `+EchoTyping.lean+` in core Lean 4.15.0,
+zero Mathlib), verified at `+8bdfd5a6+` (run 41539844452) and re-checked on
+every CI run via `+just proof-check-all+` |met
+|mathesis §5 |Strict Agda baseline solver flags (parenthetically
+`+--safe --erasure+`, or Full `+--cubical+`) |In force on the Agda source leg:
+`+--safe --without-K --cubical-compatible+`. Neither named configuration
+exactly; the difference is recorded in `+grade_deviation+`, and PROOF-POLICY
+§2.1 (later, normative) fixes this combined invocation as canonical |deviation,
+recorded
 |mathesis §5 (family note) |The dual-translation rung (`+2ii+`) needs a *non-DTT*
 second architecture
 |The gate's `+FAMILIES+` map records agda/rocq/lean4 as `+dtt+`, isabelle as
-`+hol+`. Unreachable while both legs are DTT, so it is not claimed |recorded
+`+hol+`. Unreachable while all proven legs are DTT, so `+2ii+` is not claimed |recorded
 |mathesis §6 |Do not flatten confidence into a percentage |Tokens only; nothing
 in this file or the gate averages anything, and `+just proof-grade+` prints
 "recorded, not estimated" |met
 |mathesis §6 |Axiom tracking: postulates, `+#print axioms+`, `+Print Assumptions+`,
 pinned library versions |Source leg: zero postulates under `+--safe+`, with
-pinned Agda, stdlib, echo-types and absolute-zero. Recheck legs: no axiom list,
-because no witness exists — recording one would be fabrication |met, and the gap
-stated
+pinned Agda, stdlib, echo-types and absolute-zero. Recheck legs: `+axioms: []+`
+verified per run by `+coqchk -silent -o+` + `+Print Assumptions+` (Rocq) and
+`+#print axioms+` + module-origin query (Lean 4) |met
 |mathesis §6 |Track the exact Git commit of the verification receipt |`+3cd1859…+`
-in the ledger; the gate refuses a receipt that is not a full 40-character SHA
-|met
+(Agda source leg) and `+8bdfd5a…+` (Rocq and Lean 4 recheck legs) in the ledger;
+the gate refuses a receipt that is not a full 40-character SHA |met
 |mathesis §6 |`+Superseded+` and `+Regressed+` are first-class states |Every
 historical receipt carries `+state+` (`+superseded+` for the pre-§2.1 one) and a
 reason; the gate refuses an unmarked archived receipt or a state outside the pair
@@ -163,21 +170,22 @@ copied, unclaimed witnesses are refused in both directions, and the policy gaps
 print on every run |met
 |===
 
-=== What the Grade 3 claim rests on
+=== What the Agda baseline and Grade 2i claim rest on
 
-Grade 3 is the lowest rung, so it is the one that most needs its evidence named
-rather than implied. Four things carry the claim, and the gate checks each of
-them against the tree on every run — if any of them drifts, the run goes red:
+Every rung rests on the Agda source baseline plus its recheck witnesses, and the
+gate checks each piece against the tree on every run — if any of them drifts,
+the run goes red:
 
 [cols="22%,78%",options="header",]
 |===
 |What |The evidence, and how it is checked
 |Named declarations |`+TP-ECHO-1+`, `+TP-ECHO-2+`, `+TP-ECHO-3+` in
-`+verification/proofs/agda/EchoTyping.agda+`. The ledger records each one's
-*type*, and the gate re-reads the file (whitespace-normalised) to confirm the
-recorded statement is still there. A grade anchored to a file rather than to a
-named theorem is the proof inflation mathesis §11 rejects, so an anchor that is
-not declared in the file is a failure.
+`+verification/proofs/agda/EchoTyping.agda+`, mapped to `+tp_echo_1..3+` in
+`+verification/proofs/coq/EchoTyping.v+` and `+EchoTyping.tp_echo_1..3+` (plus
+`+EchoTyping.tp_echo_1_path..3_path+`) in `+verification/proofs/lean4/EchoTyping.lean+`.
+The ledger records each Agda anchor's *type*, and the gate re-reads the
+comment-stripped source file (whitespace-normalised) to confirm the recorded
+statement is still there.
 
 |Flags in force |`+--safe --without-K --cubical-compatible+`. The gate does not
 take this on trust: it reads the `+{-# OPTIONS #-}+` pragmas out of the proof
@@ -185,20 +193,18 @@ files, reads the CLI flags out of `+scripts/check-proofs.sh+` (the instrument
 `+just proof-check-agda+` calls), and requires the ledger's record to equal the
 union. Drift in either direction fails.
 
-|The §5 parenthetical |mathesis §5 names the grade 3 configurations as
-`+--safe --erasure+`, or Full `+--cubical+`. What runs here is neither: there is
-no `+--erasure+` and no full `+--cubical+`. The grade is still recorded as 3 —
-the result is carried by Agda alone under `+--safe+`, with no postulates and no
-translation to an independent system — but the difference is recorded in the
-ledger's `+grade_deviation+` field instead of being paraphrased away, and the
-gate *requires* that field whenever the flags are not one of the named
-configurations.
-
-|"No postulates" |`+--safe+` makes the compiler refuse postulates and the other
-unsafe pragmas; `+scripts/proof-scan-dangerous.sh+` and the ledger gate's
-comment-aware escape-hatch scan run over the same files in the same lane. The
-mechanism is recorded in `+escape_hatch_evidence+`; asserting the absence of
-escape hatches without naming a mechanism is a failure.
+|The §5 parenthetical |mathesis §5 names the Agda baseline solver configurations
+as `+--safe --erasure+`, or Full `+--cubical+`. What runs on the Agda source leg
+here is `+--safe --without-K --cubical-compatible+` (canonical per PROOF-POLICY
+§2.1), with `+--erasure+` off and full `+--cubical+` unused; that flag
+difference is recorded in `+grade_deviation+` while XP-1 holds Grade `+2i+` via
+its proven Rocq and Lean 4 recheck legs.
+
+|"No postulates / zero axioms" |`+--safe+` makes Agda refuse postulates and
+unsafe pragmas; `+coqchk -silent -o+` + `+Print Assumptions+` and `+#print axioms+`
++ module-origin verification enforce `+axioms: []+` on the Rocq and Lean 4
+recheck witnesses; and `+scripts/proof-scan-dangerous.sh+` scans all four proof
+sources (nested-comment-aware) on every run.
 |===
 
 The receipt behind all four is CI run **41314454646** at
@@ -217,9 +223,8 @@ keeps it as history and pins the canonical run.
 [cols="8%,47%,45%",options="header",]
 |===
 |Rung |What it requires |State today
-|`+3+` |Agda alone, `+--safe+`, not translated |*This is where XP-1 is.* The
-Agda leg is proven and recorded; the flags, statements and escape-hatch
-mechanism above are gated.
+|`+3+` |Agda alone, `+--safe+`, not translated |Surpassed (Agda source leg
+remains gated on every CI run).
 
 |`+2i+` |At least *one* independent system (Rocq or Lean) carrying the same
 statement: `+transported+` through Dedukti/Lambdapi, or `+re-proved+` by hand,
@@ -227,8 +232,9 @@ with the statement comparison, target declaration mapping, and verbatim kernel
 assumption query recorded; no Mathlib. Completing *both* DTT legs (`+rocq+` +
 `+lean4+`) satisfies `+PROOF-POLICY+` §2 while staying at rung `+2i+` until a
 non-DTT leg is added
-|*0 of 2 legs.* This is the whole of the remaining work, and it is a proving
-job — not a bookkeeping one. `+just proof-grade+` prints the same delta.
+|*This is where XP-1 is (2 of 2 DTT recheck legs proven).* Both `+EchoTyping.v+`
+(Rocq 8.18) and `+EchoTyping.lean+` (core Lean 4.15.0) compile and pass
+zero-axiom kernel queries on every CI run.
 
 |`+2ii+` |Two proven legs *and* one outside the DTT/CIC family (e.g.
 Isabelle/HOL). Rocq + Lean cannot reach this rung: they are the same family as
@@ -284,37 +290,35 @@ An honest, evidenced regression passes: the rule cuts both ways, and
 `+46ee1832+`) §1 makes Agda the source of truth
 for theory proofs and §2 makes Rocq *and* Lean the recheck legs: each theorem
 must be *transported* (Dedukti/Lambdapi) or *re-proved by hand*, the route and
-the statement comparison recorded, and no Mathlib allowed. **That obligation is
-currently unmet for XP-1.** Both legs are recorded `+open+` in the ledger, with
-the blocker that stops each one, and the gate prints them as `+POLICY GAP+`
-lines on every run. An `+open+` leg is a legal state in the §5 vocabulary; it
-is not verification, and no part of this page or of CI claims that it is.
+the statement comparison recorded, and no Mathlib allowed. **Both §2 recheck
+legs are now proven and gated for XP-1:**
 
 [cols="14%,30%,56%",options="header",]
 |===
-|Leg |Status |What would have to happen (the recorded blocker)
-|Rocq |*open* |Transport the Agda term through Dedukti/Lambdapi (recording the
-statement comparison and the `+Print Assumptions+` output), or re-prove the
-statement by hand in Rocq. No `+TypeSafety.v+`-style witness exists here yet —
-the Rocq MANIFEST is a header explaining this, and
-`+just proof-check-coq+` therefore compiles zero modules while the ledger
-refuses any claim that they were compiled.
-
-|Lean 4 |*open* |Same choice, re-proved by hand in core Lean: Mathlib is
-forbidden by §2, and until a released Lambdapi Lean exporter exists there is no
-transport route to use. `+#print axioms+` must then show no axiom, and
-`+sorryAx+` must not appear.
+|Leg |Status |Witness and kernel verification
+|Rocq |*proven* (`+re-proved+`) |`+verification/proofs/coq/EchoTyping.v+`
+(`+gated+` in `+coq/MANIFEST+`). Uses Type-valued `+sigT+` and `+prod+` plus
+pure CIC convoy matching (no `+JMeq_eq+` / Streicher's K). Verified by
+`+coqchk -Q . "" -silent -o EchoTyping+` (`+Axioms: <none>+`) and
+`+Print Assumptions EchoTyping.tp_echo_1..3+` (`+Closed under the global context+`).
+
+|Lean 4 |*proven* (`+re-proved+`) |`+verification/proofs/lean4/EchoTyping.lean+`
+(`+gated+` in `+lean4/MANIFEST+`, core Lean 4.15.0, zero Mathlib). Proves
+`+EchoTyping.tp_echo_1..3+` over Type-valued `+PSigma+`/`+PProd+` plus
+`+EchoTyping.tp_echo_1_path..3_path+` over a Type-valued Martin-Löf `+Path+`
+identity type (`+Sigma+`/`+Prod+`/`+Empty+`). Verified by `+#print axioms+`
+(`+'does not depend on any axioms'+`) and `+Lean.Environment.getModuleIdxFor?+`
+module-origin verification.
 |===
 
 [[waivers]]
 === Waivers
 
-**No waiver is claimed for XP-1, and none is recorded in the ledger.** §4 of
-`+3-practice/PROOF-POLICY.adoc+` waives a leg when the mapped prover cannot
-*express* the statement — not when the estate has simply not built the witness
-yet. The Rocq and Lean legs are absent for the second reason, so they are open
-obligations, not waivers, and a waiver would be the wrong instrument even if it
-were convenient.
+**No waiver is claimed for XP-1, and none is recorded in the ledger.** Both
+`+rocq+` (`+EchoTyping.v+`) and `+lean4+` (`+EchoTyping.lean+`) recheck legs are
+proven directly with zero axioms. Under §4 of `+3-practice/PROOF-POLICY.adoc+`,
+a waiver is reserved strictly for a statement the mapped prover (`+rocq+`,
+`+lean4+`, `+agda+`, `+idris2+`) cannot *express* — never for an unbuilt witness.
 
 The ledger half of the rule is mechanical, and it is deliberately hard to
 satisfy with a citation that does not exist. A waiver must carry an
@@ -338,8 +342,9 @@ mathesis §6 requires the axioms behind a proof to be tracked, not assumed away:
 `+#print axioms+` in Lean, `+Print Assumptions+` in Rocq. Those are kernel
 queries, and they are the only accepted evidence that a compiled witness is
 closed — compiling is not: Rocq accepts `+Admitted+` and Lean accepts `+sorry+`
-with exit status 0. Since no witness exists on either leg there is no axiom
-list for them yet; recording one would be fabrication.
+with exit status 0. Both `+EchoTyping.v+` (`+rocq+`) and `+EchoTyping.lean+`
+(`+lean4+`) record `+axioms: []+` in `+LEDGER.json+`, verified against live
+kernel queries on every CI run.
 
 **Enforced per compiled witness (issue #131 closed):** `+scripts/check-proofs.sh+`
 does not stop at compiler exit status 0. Every `+gated+` Rocq or Lean module in
@@ -427,20 +432,22 @@ disk that neither the ledger nor a MANIFEST claims; and this page claiming a
 grade the ledger does not record. Open legs are printed as `+POLICY GAP+`, and
 are never counted as verification.
 
-|`+just proof-witness-check+`
-|The CI target: the enrolment and banned-pattern gates, the ledger audit, and
-*every recheck leg the ledger declares* (`+proof-check-coq+`, `+proof-check-lean4+`). Today both legs are declared open,
-so the manifests compile nothing and the gate says so — the lane is green on
-"the ledger is honest", never on "the theorem is verified".
+|`+just proof-check-all+` / `+just proof-witness-check+`
+|`.github/workflows/proof-ci.yml` executes `+just proof-check-all+` (issue #57):
+the enrolment gate, the ledger audit, `+proof-check-idris2+`, `+proof-check-lean4+`
+(`+EchoTyping.lean+`), `+proof-check-agda+` (`+EchoTyping.agda+`,
+`+Verification.agda+`), `+proof-check-coq+` (`+EchoTyping.v+`), and the
+comment-aware banned-pattern scan. `+just proof-witness-check+` runs the
+recheck-leg subset without requiring local Agda library registration.
 
 |`+tests/proofs/run-controls.sh+`
 |PROOF-POLICY §7 requires a gate to be verified *both ways*, and this is where
-that is done — in two halves. `+run-ledger-controls.sh+` (55 controls, no prover
+that is done — in two halves. `+run-ledger-controls.sh+` (63 controls, no prover
 needed) exercises grades, history, flags, formal declaration-to-type binding,
 quarantined and out-of-order MANIFEST bypasses, `+sorryAx+` bans, reconciliation
 status rules, external import-cone checks, waivers, debt-register presence, and
-per-language comment-aware lexical scanning.
-The kernel & witness half (`+K1+`–`+K17+`) checks `+coqc+`/`+coqchk+`/`+coqtop+`
+per-language nested-comment-aware lexical scanning.
+The kernel & witness half (`+K1+`–`+K18+`) checks `+coqc+`/`+coqchk+`/`+coqtop+`
 and `+lean+` both directly and end-to-end through `+scripts/check-proofs.sh+`:
 clean witnesses must pass and write verbatim `+CONTEXT SUMMARY+`,
 `+Closed under the global context+`, and `+does not depend on any axioms+`
@@ -448,8 +455,9 @@ receipts; witnesses importing `+Coq.Logic.Classical_Prop.classic+` or
 `+Classical.em+` (clean to lexical scan) must fail under `+axioms: []+` and pass
 under `+proven-with-postulates+` naming the exact axioms; cross-module helper
 axioms, cross-module `+sorryAx+`, `+Admitted+` theorems listed in `+.axioms+`,
-out-of-order multi-file `+MANIFEST+` entries, missing declarations, and stale
-`+axioms+` entries must all be refused. Where `+coqc+`, `+coqchk+`, `+coqtop+`, or `+lean+`
+external `+Init+` declaration smuggling (`+Nat.zero+`), out-of-order multi-file
+`+MANIFEST+` entries, missing declarations, and stale `+axioms+` entries must
+all be refused. Where `+coqc+`, `+coqchk+`, `+coqtop+`, or `+lean+`
 is absent the kernel half reports **BLOCKED**, never a pass.
 
 |`+just proof-grade+`
@@ -517,6 +525,15 @@ bash scripts/check-proof-enrolment.sh --static-only
 [cols="16%,20%,64%",options="header",]
 |===
 |Date |Receipt |Result
+|2026-11-02 |proof-ci run 41539844452 (sha `+8bdfd5a+`) |**PASS** for XP-1
+Grade *2i* across all three DTT kernels (`+EchoTyping.agda+` + `+Verification.agda+`
+under Agda 2.8.0 `+--safe --without-K --cubical-compatible+`; `+EchoTyping.v+`
+under Coq 8.18.0 + `+coqchk -silent -o+` + `+Print Assumptions+`,
+`+Closed under the global context+`; `+EchoTyping.lean+` under sha256-verified
+core Lean 4.15.0 + `+#print axioms+` + `+getModuleIdxFor?+`,
+`+does not depend on any axioms+`), plus 63 ledger controls and 18 kernel
+controls with 0 violations and 0 policy gaps.
+
 |2026-11-01 |proof-ci run 41314202374 (sha `+112a7bf+`) |**PASS** with the
 grade-3 substantiation and the split controls in place. Annotations:
 `+proof ledger controls: 15 expectation(s), 0 violations+` (grades, statements,
@@ -561,6 +578,19 @@ so instead of reporting the leg as passing), not as a pass.
 [width="100%",cols="32%,42%,26%",options="header",]
 |===
 |Date |Change |By
+|2026-11-02 |Completed XP-1's `+PROOF-POLICY+` §2 Rocq and Lean 4 recheck
+obligations (`+verification/proofs/coq/EchoTyping.v+` and
+`+verification/proofs/lean4/EchoTyping.lean+`, zero Mathlib, zero axioms),
+promoting XP-1 from Grade 3 to *Grade 2i* (`+COQ-CHECKED+`, `+LEAN-CHECKED+`,
+`+RECONCILED+`) and closing issue #57. Hardened `+proof-scan-dangerous.sh+`
+(nested block comments + `+--strip-comments+`), `+check-proof-enrolment.sh+`
+(fail-closed receipt writes), `+check-proof-ledger.sh+` (theorem ID & JSON shape
+guards, source-prover checks, comment-stripped anchor/signature/axiom checks,
+non-empty history, waiver-tool binding), and `+check-proofs.sh+` (Lean
+declaration ownership via comment-stripped module scan +
+`+Lean.Environment.getModuleIdxFor?+`), expanding §7 controls to 63 ledger +
+18 kernel expectations |Arena agent
+
 |2026-11-01 |Closed issue #131 and aligned with `+mathesis+` authority &
 cross-prover reconciliation guidance (`+docs/standards/AUTHORITY.adoc+`,
 `+docs/proposals/estate-mathematical-architecture.adoc+`,
diff --git a/docs/proof-debt.md b/docs/proof-debt.md
index 0628835..db915f0 100644
--- a/docs/proof-debt.md
+++ b/docs/proof-debt.md
@@ -5,8 +5,9 @@
 
 Dispositions per `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` (estate policy,
 enforced by `scripts/check-trusted-base.sh` through `governance-reusable.yml`).
-Scope: this repository is proof-bearing — `verification/proofs/agda/` carries
-XP-1 (see `verification/proofs/LEDGER.json` and `PROOF-STATUS.adoc`).
+Scope: this repository is proof-bearing — `verification/proofs/{agda,coq,lean4}/`
+carries XP-1 across its Agda source leg and its Rocq and core Lean 4 recheck
+witnesses (see `verification/proofs/LEDGER.json` and `PROOF-STATUS.adoc`).
 
 The file exists even though the answer is "nothing outstanding", because an
 absent file is indistinguishable from an unexamined repository, and the policy
diff --git a/scripts/check-coordination-boundary.sh b/scripts/check-coordination-boundary.sh
index 472c55c..8492526 100755
--- a/scripts/check-coordination-boundary.sh
+++ b/scripts/check-coordination-boundary.sh
@@ -33,6 +33,8 @@ ALLOWED_PROOFS=(
   "verification/proofs/agda/EchoTyping.agda"
   "verification/proofs/agda/Verification.agda"
   "verification/proofs/agda/nextgen-typing.agda-lib"
+  "verification/proofs/coq/EchoTyping.v"
+  "verification/proofs/lean4/EchoTyping.lean"
 )
 is_allowed_proof() {
   local f="$1" a
diff --git a/scripts/check-proof-enrolment.sh b/scripts/check-proof-enrolment.sh
index 601bc35..275e9e3 100755
--- a/scripts/check-proof-enrolment.sh
+++ b/scripts/check-proof-enrolment.sh
@@ -301,7 +301,10 @@ status="PASS"
 [ "$status" = "PASS" ] && [ "${#BLOCKED[@]}" -gt 0 ] && status="BLOCKED"
 
 if [ -n "$RECEIPT" ]; then
-  mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null || true
+  if ! mkdir -p "$(dirname "$RECEIPT")" 2>/dev/null; then
+    echo "FAIL: cannot create receipt directory for $RECEIPT" >&2
+    exit 1
+  fi
   {
     echo "proof-enrolment receipt"
     echo "generated: $(date -u +%Y-%m-%dT%H:%M:%SZ)"
@@ -323,7 +326,10 @@ if [ -n "$RECEIPT" ]; then
       echo "blocked:"
       printf '  - %s\n' "${BLOCKED[@]}"
     fi
-  } >"$RECEIPT"
+  } >"$RECEIPT" || {
+    echo "FAIL: cannot write receipt $RECEIPT" >&2
+    exit 1
+  }
   echo "receipt written: $RECEIPT"
   if [ -n "${GITHUB_STEP_SUMMARY:-}" ]; then
     {
diff --git a/scripts/check-proof-ledger.sh b/scripts/check-proof-ledger.sh
index 1269cce..cfbf6ae 100755
--- a/scripts/check-proof-ledger.sh
+++ b/scripts/check-proof-ledger.sh
@@ -97,12 +97,21 @@ scan_escape_hatches() {
 
 # Declared axioms are different from escape hatches: PROOF-POLICY §5 allows
 # `proven-with-postulates` when the axioms are named and allowed by
-# TRUSTED-BASE-REDUCTION-POLICY. Collect them so the ledger can be cross-checked.
+# TRUSTED-BASE-REDUCTION-POLICY. Strip comments first so prose in comments
+# (e.g. `(* Axiom fake : False. *)`) can never impersonate a declared axiom.
+# Print numbered declaration lines from a Coq or Lean file; other extensions
+# produce no output. Scanner and grep failures are converted to success.
 scan_declared_axioms() {
   local file="$1"
   case "$file" in
-    *.v) grep -nE '^[[:space:]]*(Axiom|Parameter|Conjecture)[[:space:]]' "$file" || true ;;
-    *.lean) grep -nE '^[[:space:]]*axiom[[:space:]]' "$file" || true ;;
+    *.v)
+      bash "$ROOT/scripts/proof-scan-dangerous.sh" --strip-comments "$file" \
+        | grep -nE '^[[:space:]]*(Axiom|Parameter|Conjecture)[[:space:]]' || true
+      ;;
+    *.lean)
+      bash "$ROOT/scripts/proof-scan-dangerous.sh" --strip-comments "$file" \
+        | grep -nE '^[[:space:]]*axiom[[:space:]]' || true
+      ;;
     *) true ;;
   esac
 }
@@ -236,6 +245,28 @@ while IFS= read -r bad; do
   [ -n "$bad" ] && fail "theorem kind must be 'theory' or 'engineering' (PROOF-POLICY §1): '${bad}'"
 done < <(jq -r '[.theorems[].kind // "<missing>"][] | select(. != "theory" and . != "engineering")' "$LEDGER" | sort -u)
 
+if jq -e '.theorems[] | select((.id | type) != "string" or ((.id | gsub("^[[:space:]]+|[[:space:]]+$"; "")) == "") or (.id | test("[[:space:]]")))' "$LEDGER" >/dev/null 2>&1; then
+  fail "theorem id: every theorem in .theorems[] must carry a non-empty, whitespace-free string .id"
+fi
+
+while IFS= read -r shape_err; do
+  [ -n "$shape_err" ] && fail "malformed theorem entry: $shape_err"
+done < <(jq -r '
+  .theorems[] | (if (.id | type) == "string" and (.id | length) > 0 then .id else "<unnamed>" end) as $id |
+  [
+    (if (.source | type) != "object" then "\($id): .source must be an object" else empty end),
+    (if ((.source | type) == "object" and (.source.files != null) and ((.source.files | type) != "array")) then "\($id): .source.files must be an array" else empty end),
+    (if ((.source | type) == "object" and (.source.safety_flags != null) and ((.source.safety_flags | type) != "array")) then "\($id): .source.safety_flags must be an array" else empty end),
+    (if ((.source | type) == "object" and (.source.flags_provenance != null) and ((.source.flags_provenance | type) != "object")) then "\($id): .source.flags_provenance must be an object" else empty end),
+    (if (.statement_anchor != null and (.statement_anchor | type) != "array") then "\($id): .statement_anchor must be an array" else empty end),
+    (if (.statement_formal != null and (.statement_formal | type) != "object") then "\($id): .statement_formal must be an object" else empty end),
+    (if (.legs != null and (.legs | type) != "array") then "\($id): .legs must be an array" else empty end),
+    (if (.history | type) != "array" then "\($id): .history must be an array (mathesis §6)"
+     elif (.history | length) == 0 then "\($id): .history must record at least one baseline or transition entry (mathesis §6)"
+     else empty end),
+    (if (.caveats != null and (.caveats | type) != "array") then "\($id): .caveats must be an array" else empty end)
+  ][]' "$LEDGER")
+
 while IFS= read -r dup; do
   [ -n "$dup" ] && fail "duplicate theorem id in ledger: '${dup}'"
 done < <(jq -r '[.theorems[].id] | group_by(.)[] | select(length > 1) | .[0]' "$LEDGER")
@@ -250,18 +281,20 @@ done < <(jq -r '[.theorems[].grade // "<missing>" | tostring][] | select(. != "3
 # cannot inflate Grade 3 to Grade 2i.
 ROWS_TSV="$(mktemp)" || { echo "BLOCKED: cannot create a temporary file" >&2; exit 2; }
 trap 'rm -f "$ROWS_TSV"' EXIT
-jq -r '
+if ! jq -r '
   .theorems[] as $t |
-  ($t.source.prover // "") as $src |
-  [ $t.id,
-    $t.kind,
+  (if ($t.source | type) == "object" then ($t.source.prover // "") else "" end) as $src |
+  [ ($t.id | tostring),
+    ($t.kind // ""),
     ($t.grade | tostring),
-    ([$t.legs[]?.prover] | join(",")),
-    ([$t.legs[]? | select(.waiver == null) | select(.status != "open")] | length),
-    ([$t.legs[]? | select(.waiver == null)
+    ([ (if ($t.legs | type) == "array" then $t.legs[] else empty end) | .prover // "" ] | join(",")),
+    ([ (if ($t.legs | type) == "array" then $t.legs[] else empty end) | select(.waiver == null) | select(.status != "open") ] | length),
+    ([ (if ($t.legs | type) == "array" then $t.legs[] else empty end) | select(.waiver == null)
        | select((.prover // "") != $src)
-       | select(.status == "proven" or .status == "proven-with-postulates")] | length)
-  ] | map(tostring) | join("\u001f")' "$LEDGER" > "$ROWS_TSV"
+       | select(.status == "proven" or .status == "proven-with-postulates") ] | length)
+  ] | map(tostring) | join("\u001f")' "$LEDGER" > "$ROWS_TSV" 2>/dev/null; then
+  fail "ledger shape error: unable to extract per-theorem rows via jq"
+fi
 
 declare -A THEOREM_PROVEN=()
 while IFS=$'\x1f' read -r tid kind grade provers claimed proven; do
@@ -324,7 +357,7 @@ while IFS=$'\x1f' read -r tid kind grade provers claimed proven; do
   esac
 
   if [[ "$claimed" -gt 0 ]]; then
-    GAPS+=("$tid: $claimed leg(s) carry a non-open status and MUST compile in this lane")
+    NOTES+=("$tid: $claimed non-open recheck leg(s) recorded — compiled and kernel-queried by scripts/check-proofs.sh")
   fi
 done < "$ROWS_TSV"
 
@@ -417,10 +450,13 @@ while IFS=$'\x1f' read -r tid sprover sstatus rec_file_opts rec_cli rec_effectiv
     jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .kind' "$LEDGER"
   )"
 
-  # (a) PROOF-POLICY §1: a theory theorem's source of truth is Agda, and it
-  # must actually be proven — a grade resting on an open source leg is a guess.
+  # (a) PROOF-POLICY §1: a theory theorem's source of truth is Agda and an
+  # engineering theorem's source of truth is Idris2, and the source leg must
+  # actually be proven — a grade resting on an open source leg is a guess.
   if [ "$kind_of" = "theory" ] && [ "$sprover" != "agda" ]; then
     fail "$tid: a theory theorem's source leg must be Agda (PROOF-POLICY §1); ledger records '${sprover:-<missing>}'"
+  elif [ "$kind_of" = "engineering" ] && [ "$sprover" != "idris2" ]; then
+    fail "$tid: an engineering theorem's source leg must be Idris2 (PROOF-POLICY §1); ledger records '${sprover:-<missing>}'"
   fi
   case "$sstatus" in
     proven|proven-with-postulates) ;;
@@ -442,63 +478,85 @@ while IFS=$'\x1f' read -r tid sprover sstatus rec_file_opts rec_cli rec_effectiv
     rocq|coq) src_mdir="$PROOFS_DIR/coq" ;;
     lean4|lean) src_mdir="$PROOFS_DIR/lean4" ;;
     idris2) src_mdir="$PROOFS_DIR/idris2" ;;
+    *)
+      fail "$tid: unsupported .source.prover '${sprover:-<missing>}' — must be one of agda, idris2, rocq, lean4 (PROOF-POLICY §1)"
+      continue
+      ;;
   esac
   IFS=',' read -r -a src_files <<< "$files_csv"
   for f in "${src_files[@]}"; do
     [[ -z "$f" ]] && continue
     if [[ ! -f "$f" ]]; then
       fail "$tid: source file recorded but missing on disk: $f"
-    elif [[ ( "$sstatus" == "proven" || "$sstatus" == "proven-with-postulates" ) && -n "$src_mdir" ]]; then
+    elif [[ "$sstatus" == "proven" || "$sstatus" == "proven-with-postulates" ]]; then
       if ! manifest_is_gated "$src_mdir/MANIFEST" "$f"; then
         fail "$tid: proven source file '$f' is not listed as 'gated' in $src_mdir/MANIFEST"
       fi
     fi
   done
 
-  # (c) flags: what the instrument passes, what the files declare, and the
-  # union the ledger claims must agree. Drift here silently changes what a
-  # Grade 3 claim means.
-  actual_file_opts="$(file_agda_options "${src_files[@]}")"
-  if [ "$rec_cli" != "$AGDA_CLI_FLAGS" ]; then
-    fail "$tid: flags drift — scripts/check-proofs.sh invokes 'agda ${AGDA_CLI_FLAGS}' but the ledger records CLI '${rec_cli:-<missing>}'"
-  fi
-  if [ "$rec_file_opts" != "$actual_file_opts" ]; then
-    fail "$tid: flags drift — the proof files declare '${actual_file_opts:-<none>}' in {-# OPTIONS #-} but the ledger records '${rec_file_opts:-<missing>}'"
-  fi
-  effective_expected="$(printf '%s %s\n' "$actual_file_opts" "$AGDA_CLI_FLAGS" | tr ' ' '\n' | grep -v '^$' | sort -u | tr '\n' ' ' | sed 's/ *$//')"
-  if [ "$rec_effective" != "$effective_expected" ]; then
-    fail "$tid: effective safety flags recorded as '${rec_effective:-<missing>}' but the files+instrument actually apply '${effective_expected:-<none>}'"
-  fi
-  case " $rec_effective " in
-    *" --safe "*) ;;
-    *) fail "$tid: '--safe' is not in the effective flags — postulates and other escape hatches are not ruled out, so the grade is unsupported (mathesis §5)" ;;
-  esac
+  # (c) flags: for Agda source legs, what the instrument passes, what the files
+  # declare, and the union the ledger claims must agree. For Idris2 engineering
+  # source legs (PROOF-POLICY §1), `%default total` must be active outside comments.
+  if [ "$sprover" = "agda" ]; then
+    actual_file_opts="$(file_agda_options "${src_files[@]}")"
+    if [ "$rec_cli" != "$AGDA_CLI_FLAGS" ]; then
+      fail "$tid: flags drift — scripts/check-proofs.sh invokes 'agda ${AGDA_CLI_FLAGS}' but the ledger records CLI '${rec_cli:-<missing>}'"
+    fi
+    if [ "$rec_file_opts" != "$actual_file_opts" ]; then
+      fail "$tid: flags drift — the proof files declare '${actual_file_opts:-<none>}' in {-# OPTIONS #-} but the ledger records '${rec_file_opts:-<missing>}'"
+    fi
+    effective_expected="$(printf '%s %s\n' "$actual_file_opts" "$AGDA_CLI_FLAGS" | tr ' ' '\n' | grep -v '^$' | sort -u | tr '\n' ' ' | sed 's/ *$//')"
+    if [ "$rec_effective" != "$effective_expected" ]; then
+      fail "$tid: effective safety flags recorded as '${rec_effective:-<missing>}' but the files+instrument actually apply '${effective_expected:-<none>}'"
+    fi
+    case " $rec_effective " in
+      *" --safe "*) ;;
+      *) fail "$tid: '--safe' is not in the effective flags — postulates and other escape hatches are not ruled out, so the grade is unsupported (mathesis §5)" ;;
+    esac
 
-  # (d) mathesis §5 names the Grade 3 configurations parenthetically
-  # (--safe --erasure, or Full --cubical). If the flags in force are neither,
-  # the deviation must be recorded rather than glossed over.
-  grade3_named=0
-  case " $rec_effective " in *" --erasure "*) grade3_named=1 ;; esac
-  case " $rec_effective " in
-    *" --cubical "*)
-      case " $rec_effective " in
-        *" --cubical-compatible "*) ;;
-        *) grade3_named=1 ;;
-      esac
-      ;;
-  esac
-  if [ "$grade3_named" -eq 0 ]; then
-    deviation="$(
-      jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .grade_deviation // ""' "$LEDGER"
-    )"
-    if [ -z "${deviation// }" ]; then
-      fail "$tid: the flags in force ('$rec_effective') are neither of the configurations mathesis §5 names for grade 3 (--safe --erasure, or Full --cubical) — record the deviation in .grade_deviation instead of paraphrasing the policy"
+    # (d) mathesis §5 names the Agda Grade 3 configurations parenthetically
+    # (--safe --erasure, or Full --cubical). If the flags in force are neither,
+    # the deviation must be recorded rather than glossed over.
+    grade3_named=0
+    case " $rec_effective " in *" --erasure "*) grade3_named=1 ;; esac
+    case " $rec_effective " in
+      *" --cubical "*)
+        case " $rec_effective " in
+          *" --cubical-compatible "*) ;;
+          *) grade3_named=1 ;;
+        esac
+        ;;
+    esac
+    if [ "$grade3_named" -eq 0 ]; then
+      deviation="$(
+        jq -r --arg id "$tid" '.theorems[] | select(.id == $id) | .grade_deviation // ""' "$LEDGER"
+      )"
+      if [ -z "${deviation// }" ]; then
+        fail "$tid: the flags in force ('$rec_effective') are neither of the configurations mathesis §5 names for grade 3 (--safe --erasure, or Full --cubical) — record the deviation in .grade_deviation instead of paraphrasing the policy"
+      fi
     fi
+  elif [ "$sprover" = "idris2" ]; then
+    for f in "${src_files[@]}"; do
+      [[ -f "$f" ]] || continue
+      if ! bash "$ROOT/scripts/proof-scan-dangerous.sh" --strip-comments "$f" | grep -qE '^[[:space:]]*%default[[:space:]]+total\b'; then
+        fail "$tid: Idris2 source file '$f' must declare '%default total' outside comments (PROOF-POLICY §1)"
+      fi
+    done
   fi
 
-  # (e) the statement must rest on named declarations that exist. A grade
-  # anchored to a file rather than a theorem is the "proof inflation" mathesis
-  # §11 rejects.
+  # (e) the statement must rest on named declarations that exist outside
+  # comments. A grade anchored to a file or commented-out text is the "proof
+  # inflation" mathesis §11 rejects.
+  # Cache comment-stripped source once per recorded source file so both anchor
+  # and formal-type checks inspect non-comment declarations without spawning
+  # redundant subshells across large control suites.
+  declare -A stripped_src_cache=()
+  for f in "${src_files[@]}"; do
+    [[ -f "$f" ]] || continue
+    stripped_src_cache["$f"]="$(bash "$ROOT/scripts/proof-scan-dangerous.sh" --strip-comments "$f")"
+  done
+
   if [ -z "${anchor_ids// }" ]; then
     fail "$tid: no .statement_anchor — a grade must point at the named declarations that carry the statement, not at a file"
   else
@@ -508,7 +566,8 @@ while IFS=$'\x1f' read -r tid sprover sstatus rec_file_opts rec_cli rec_effectiv
       hit=0
       for f in "${src_files[@]}"; do
         [ -f "$f" ] || continue
-        grep -qE "^[[:space:]]*${a//./\\.}[[:space:]]*:" "$f" && hit=1
+        printf '%s\n' "${stripped_src_cache[$f]}" \
+          | grep -qE "^[[:space:]]*${a//./\\.}[[:space:]]*:" && hit=1
       done
       [ "$hit" -eq 1 ] || fail "$tid: statement anchor '$a' is not declared in any recorded source file (looked in: $files_csv)"
     done
@@ -518,7 +577,7 @@ while IFS=$'\x1f' read -r tid sprover sstatus rec_file_opts rec_cli rec_effectiv
   # and any recheck leg, and check-proofs.sh queries Print Assumptions / #print
   # axioms against .statement_formal.declarations. Require a non-empty array
   # covering every .statement_anchor, and verify each recorded declaration's
-  # TYPE is still present in the source file, whitespace-normalised.
+  # TYPE is still present outside comments in the source file, whitespace-normalised.
   formal_decl_count="$(jq -r --arg id "$tid" '
     .theorems[] | select(.id == $id)
     | if (.statement_formal.declarations | type) == "array" then (.statement_formal.declarations | length) else -1 end' "$LEDGER")"
@@ -543,7 +602,7 @@ while IFS=$'\x1f' read -r tid sprover sstatus rec_file_opts rec_cli rec_effectiv
     found=0
     for f in "${src_files[@]}"; do
       [[ -f "$f" ]] || continue
-      norm_file=" $(tr -s '[:space:]' ' ' < "$f") "
+      norm_file=" $(printf '%s\n' "${stripped_src_cache[$f]}" | tr -s '[:space:]' ' ') "
       case "$norm_file" in
         *" ${decl_name} : ${norm_type} "*) found=1 ;;
       esac
@@ -831,6 +890,17 @@ while IFS=$'\x1f' read -r tid prover wstatus wobligation wtool wreason wrecord;
       fail "$tid/$prover: waiver without '${pair%%:*}' — §4 requires the obligation, the tool, the reason and the exception record"
     fi
   done
+  if [ -n "$wtool" ] && [ "$wtool" != "null" ]; then
+    tool_matches_leg=0
+    case "$prover:$wtool" in
+      rocq:rocq|rocq:coq|coq:rocq|coq:coq) tool_matches_leg=1 ;;
+      lean4:lean4|lean4:lean|lean:lean4|lean:lean) tool_matches_leg=1 ;;
+      *) [ "$wtool" = "$prover" ] && tool_matches_leg=1 ;;
+    esac
+    if [ "$tool_matches_leg" -eq 0 ]; then
+      fail "$tid/$prover: .waiver.tool '$wtool' does not match leg prover '$prover' — a waiver must bind to the waived leg's own prover (§4)"
+    fi
+  fi
   # The record must RESOLVE, not merely be non-empty. Accepting any string let a
   # required leg carry `record: does-not-exist` and still pass: the presence
   # check was satisfied, and the waiver then removed that leg from the status
diff --git a/scripts/check-proofs.sh b/scripts/check-proofs.sh
index da4a6d8..1aeed69 100755
--- a/scripts/check-proofs.sh
+++ b/scripts/check-proofs.sh
@@ -351,8 +351,8 @@ array_contains() {
 # against the owning leg's recorded `.axioms` array. Whenever `<cand_mod>` maps
 # to a staged `.v` file in `$work_root` (either the primary witness or a staged
 # support module), `<short>` MUST be declared via `Axiom`/`Parameter`/`Conjecture`
-# in that file — so an incomplete `Theorem ... Admitted.` can never satisfy the
-# kernel check even if its full name is listed in `.axioms`.
+# outside comments in that file — so an incomplete `Theorem ... Admitted.` can
+# never satisfy the kernel check even if its full name is listed in `.axioms`.
 coq_axiom_allowed() {
   local ax="$1" mod_path="$2" work_root="$3"
   shift 3
@@ -364,7 +364,8 @@ coq_axiom_allowed() {
     local short="${ax##*.}"
     local local_v="$work_root/${cand_mod//./\/}.v"
     if [[ -f "$local_v" ]]; then
-      if ! grep -qE "^[[:space:]]*(Axiom|Parameter|Conjecture)[[:space:]]+${short//./\\.}([^A-Za-z0-9_']|$)" "$local_v" 2>/dev/null; then
+      if ! bash "$SCRIPT_ROOT/scripts/proof-scan-dangerous.sh" --strip-comments "$local_v" \
+           | grep -qE "^[[:space:]]*(Axiom|Parameter|Conjecture)[[:space:]]+${short//./\\.}([^A-Za-z0-9_']|$)" 2>/dev/null; then
         return 1
       fi
       if array_contains "$ax" "${allowed[@]}" || { [[ "$cand_mod" == "$mod_path" ]] && array_contains "$short" "${allowed[@]}"; }; then
@@ -396,8 +397,9 @@ verify_ledger_ready() {
 
 # Emit matching non-open legs for ($1 = prover_kind: coq|lean4, $2 = full_rel).
 # Output lines use US (\x1f): role (primary|support), theorem id, status,
-# axioms JSON and declarations JSON. A jq failure returns non-zero, although
-# callers using process substitution do not receive that status.
+# axioms JSON, declarations JSON and support-files JSON. A jq failure returns
+# non-zero, although callers using process substitution do not receive that
+# status. Invalid or missing support-files arrays are represented as [].
 query_claiming_legs() {
   local pkind="$1" full_rel="$2"
   jq -r --arg kind "$pkind" --arg path "$full_rel" '
@@ -431,7 +433,8 @@ query_claiming_legs() {
         ($t.id // "<unnamed>"),
         ($leg.status // ""),
         (if (($leg.axioms // []) | type) == "array" then (($leg.axioms // []) | tojson) else "null" end),
-        (target_decls($t; $leg) | tojson)
+        (target_decls($t; $leg) | tojson),
+        (if (($leg.support_files // []) | type) == "array" then (($leg.support_files // []) | tojson) else "[]" end)
       ]
     | join("\u001f")
   ' "$LEDGER"
@@ -530,9 +533,9 @@ $coqchk_out"
   done <<<"$coqchk_ax_raw"
 
   # 2. Validate against every claiming leg and run per-declaration Print Assumptions.
-  local role tid leg_status axioms_json decls_json
+  local role tid leg_status axioms_json decls_json support_json
   for row in "${leg_rows[@]}"; do
-    IFS=$'\x1f' read -r role tid leg_status axioms_json decls_json <<<"$row"
+    IFS=$'\x1f' read -r role tid leg_status axioms_json decls_json support_json <<<"$row"
     if [[ "$axioms_json" == "null" ]]; then
       ASSUMPTION_ERR="$full_rel ($tid): leg .axioms must be a JSON array"
       return 1
@@ -693,6 +696,8 @@ $probe_out"
 # Check a compiled Lean module against each claiming ledger leg. The arguments
 # are its source root, path relative to that root and staged root. Append query
 # output to the receipt sections; on rejection return 1 and set $ASSUMPTION_ERR.
+# For primary artifacts, check that recorded declarations belong to the leg's
+# staged modules as well as checking their axioms; support modules are imported.
 verify_lean_assumptions() {
   local root="$1" rel="$2" work_root="$3"
   local clean_rel="${rel#./}"
@@ -714,9 +719,9 @@ verify_lean_assumptions() {
     return 1
   fi
 
-  local role tid leg_status axioms_json decls_json
+  local role tid leg_status axioms_json decls_json support_json
   for row in "${leg_rows[@]}"; do
-    IFS=$'\x1f' read -r role tid leg_status axioms_json decls_json <<<"$row"
+    IFS=$'\x1f' read -r role tid leg_status axioms_json decls_json support_json <<<"$row"
     if [[ "$axioms_json" == "null" ]]; then
       ASSUMPTION_ERR="$full_rel ($tid): leg .axioms must be a JSON array"
       return 1
@@ -776,6 +781,23 @@ $sup_out"
       return 1
     fi
 
+    # Build the set of staged Lean files & module names owned by this leg so
+    # legs[].declarations cannot satisfy #print axioms via imported Init/Std
+    # constants (e.g. `Nat.zero` or `True.intro`).
+    local allowed_lean_files=("$work_root/$clean_rel")
+    local allowed_lean_mods=("$mod_path")
+    local s_entry s_rel s_mod
+    while IFS= read -r s_entry; do
+      [[ -z "$s_entry" ]] && continue
+      s_rel="${s_entry#"${root%/}/"}"
+      if [[ "$s_rel" != "$s_entry" && -f "$work_root/$s_rel" && "$s_rel" == *.lean ]]; then
+        allowed_lean_files+=("$work_root/$s_rel")
+        s_mod="${s_rel%.lean}"
+        s_mod="${s_mod//\//.}"
+        allowed_lean_mods+=("$s_mod")
+      fi
+    done < <(jq -r '.[]' <<<"${support_json:-[]}")
+
     local probe_file="$work_root/__AssumptionsProbe.lean"
     {
       printf 'import %s\n' "$mod_path"
@@ -786,10 +808,81 @@ $sup_out"
           ASSUMPTION_ERR="$full_rel ($tid): declaration '$decl' is not a valid Lean identifier — map Agda anchors to Lean identifiers in legs[].declarations"
           return 1
         fi
+        local decl_tail="${decl##*.}"
+        local esc_tail="${decl_tail//./\\.}"
+        local found_in_leg=0 lf
+        for lf in "${allowed_lean_files[@]}"; do
+          if bash "$SCRIPT_ROOT/scripts/proof-scan-dangerous.sh" --strip-comments "$lf" \
+             | grep -qE "(^|[^A-Za-z0-9_'])(theorem|lemma|def|abbrev|opaque|axiom|inductive|structure)[[:space:]]+${esc_tail}([^A-Za-z0-9_']|$)" 2>/dev/null; then
+            found_in_leg=1
+            break
+          fi
+        done
+        if [[ "$found_in_leg" -eq 0 ]]; then
+          rm -f "$probe_file"
+          ASSUMPTION_ERR="$full_rel ($tid): declaration '$decl' is not declared in this leg's Lean file(s) (${allowed_lean_mods[*]}) — legs[].declarations must name declarations owned by the leg, not external/Init constants"
+          return 1
+        fi
         printf '#print axioms %s\n' "$decl"
       done
     } >"$probe_file"
 
+    if [[ ! -f "$LEAN_LIBDIR/Lean.olean" ]]; then
+      rm -f "$probe_file"
+      ASSUMPTION_ERR="$full_rel ($tid): $LEAN_LIBDIR/Lean.olean not found — Lean constant-origin verification cannot run, so declaration ownership is unverified"
+      return 1
+    else
+      local origin_file="$work_root/__OriginProbe.lean"
+      local decl_list_lean=""
+      local decl
+      for decl in "${target_decls[@]}"; do
+        [[ -n "$decl_list_lean" ]] && decl_list_lean+=", "
+        decl_list_lean+="\`\`${decl}"
+      done
+      cat >"$origin_file" <<EOF
+import Lean
+import ${mod_path}
+#eval show Lean.Elab.Command.CommandElabM Unit from do
+  let env ← Lean.getEnv
+  for c in [${decl_list_lean}] do
+    match env.getModuleIdxFor? c with
+    | some idx =>
+      let m := env.header.moduleNames[idx.toNat]!
+      IO.println s!"ORIGIN|{c}|{m}"
+    | none =>
+      IO.println s!"ORIGIN|{c}|<current>"
+EOF
+      local origin_out origin_rc
+      set +e
+      origin_out="$(cd "$work_root" && LEAN_PATH="$work_root:$LEAN_LIBDIR${LEAN_PATH:+:$LEAN_PATH}" lean "$origin_file" 2>&1)"
+      origin_rc=$?
+      set -e
+      rm -f "$origin_file"
+      if [[ "$origin_rc" -ne 0 ]] || grep -qE 'error:' <<<"$origin_out"; then
+        rm -f "$probe_file"
+        ASSUMPTION_ERR="$full_rel ($tid): Lean constant-origin probe failed (exit $origin_rc):
+$origin_out"
+        return 1
+      fi
+      local oline otag odecl omod origin_count=0
+      while IFS= read -r oline; do
+        [[ "$oline" == ORIGIN\|* ]] || continue
+        IFS='|' read -r otag odecl omod <<<"$oline"
+        origin_count=$((origin_count + 1))
+        if ! array_contains "$omod" "${allowed_lean_mods[@]}"; then
+          rm -f "$probe_file"
+          ASSUMPTION_ERR="$full_rel ($tid): declaration '$odecl' resolves in the Lean kernel to module '$omod', outside this leg's modules (${allowed_lean_mods[*]})"
+          return 1
+        fi
+      done <<<"$origin_out"
+      if [[ "$origin_count" -ne "${#target_decls[@]}" ]]; then
+        rm -f "$probe_file"
+        ASSUMPTION_ERR="$full_rel ($tid): expected ${#target_decls[@]} Lean origin verdicts, saw $origin_count:
+$origin_out"
+        return 1
+      fi
+    fi
+
     local probe_out probe_rc
     set +e
     probe_out="$(cd "$work_root" && LEAN_PATH="$work_root:$LEAN_LIBDIR${LEAN_PATH:+:$LEAN_PATH}" lean "$probe_file" 2>&1)"
diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh
index 86259ea..787c386 100755
--- a/scripts/proof-scan-dangerous.sh
+++ b/scripts/proof-scan-dangerous.sh
@@ -53,6 +53,7 @@ SCAN_DIRS="verification tests"
 RECEIPT=""
 
 SCAN_FILE=""
+STRIP_FILE=""
 SHOW_PATTERNS=0
 while [ "$#" -gt 0 ]; do
   case "$1" in
@@ -60,6 +61,8 @@ while [ "$#" -gt 0 ]; do
     --receipt=*) RECEIPT="${1#--receipt=}"; shift ;;
     --scan-file) SCAN_FILE="${2:-}"; shift 2 ;;
     --scan-file=*) SCAN_FILE="${1#--scan-file=}"; shift ;;
+    --strip-comments) STRIP_FILE="${2:-}"; shift 2 ;;
+    --strip-comments=*) STRIP_FILE="${1#--strip-comments=}"; shift ;;
     --patterns) SHOW_PATTERNS=1; shift ;;
     -h|--help) sed -n '2,34p' "$0"; exit 0 ;;
     *) echo "unknown argument: $1" >&2; exit 1 ;;
@@ -107,36 +110,16 @@ write_receipt() {
   } >"$RECEIPT" || { echo "FAIL: cannot write receipt $RECEIPT" >&2; exit 1; }
 }
 
-echo "=== Scanning for dangerous patterns in proofs ==="
-echo "patterns: $PATTERNS"
-echo "scope:    $SCAN_DIRS"
-
-# Print $1 with the comment syntax of ITS language removed, and string literals
-# masked, preserving line numbers. Three things matter here:
-#
-#   * One comment syntax for every language is wrong in the dangerous direction.
-#     `(*` is a comment in Coq and TLA+ but ordinary text in Lean, so a Lean file
-#     containing `(* ... Axiom ... *)` had the Axiom treated as commented-out and
-#     the scan called it clean. The delimiters are now chosen per extension.
-#   * Lean is not one of the languages with `//` comments: `{x // p x}` is
-#     subtype notation, so treating `//` as a comment would cut the line short
-#     and hide whatever followed on it. Lean takes `--` and `/- -/` only.
-#   * A comment marker inside a string is not a comment. Masks keep `"--"` in a
-#     string from opening one, and keep a banned word inside a string from being
-#     counted as code. Only double-quoted strings are masked: a prime is part of
-#     an ordinary identifier in Agda and Idris, and masking from it would hide
-#     the rest of the line.
-#   * For an unknown extension, comments are left intact and double-quoted
-#     strings are masked; no comment syntax is guessed.
-#
-# Nested block comments are not supported; an unclosed block comment runs to the
-# end of the file. Delimiters are matched after string masking, so `"(*"` is
-# text. Comment *text* is dropped rather than blanked, which keeps `grep -n`
-# line numbers aligned with the file.
+# Print $1 with comments removed and double-quoted string contents masked,
+# preserving line numbers. Comment syntax is selected by extension; nested
+# block comments are recognised for Agda, Idris, Lean, Coq, TLA+ and F*.
+# An unclosed block comment extends to EOF. Unknown extensions retain comments
+# but still have double-quoted string contents masked. The function returns the
+# awk status; the --strip-comments command mode exits 0 after calling it.
 strip_comments() {
   local f="$1" mode
   case "$f" in
-    *.agda|*.lagda|*.lagda.md|*.lagda.rst|*.lagda.tex) mode=agda ;;
+    *.agda|*.lagda|*.lagda.*) mode=agda ;;
     *.idr) mode=idris ;;
     *.lean) mode=lean ;;
     *.v) mode=coq ;;
@@ -146,12 +129,12 @@ strip_comments() {
   esac
   awk -v mode="$mode" '
     BEGIN {
-      lop1 = ""; lop2 = ""; bop = ""; bcl = ""
-      if (mode == "agda" || mode == "idris") { lop1 = "--"; bop = "{-"; bcl = "-}" }
-      else if (mode == "lean")              { lop1 = "--"; bop = "/-"; bcl = "-/" }
-      else if (mode == "coq")               { bop = "(*"; bcl = "*)" }
-      else if (mode == "tla")               { lop1 = "\\*"; bop = "(*"; bcl = "*)" }
-      else if (mode == "fstar")             { lop2 = "//"; bop = "(*"; bcl = "*)" }
+      lop1 = ""; lop2 = ""; bop = ""; bcl = ""; nested = 0
+      if (mode == "agda" || mode == "idris") { lop1 = "--"; bop = "{-"; bcl = "-}"; nested = 1 }
+      else if (mode == "lean")              { lop1 = "--"; bop = "/-"; bcl = "-/"; nested = 1 }
+      else if (mode == "coq")               { bop = "(*"; bcl = "*)"; nested = 1 }
+      else if (mode == "tla")               { lop1 = "\\*"; bop = "(*"; bcl = "*)"; nested = 1 }
+      else if (mode == "fstar")             { lop2 = "//"; bop = "(*"; bcl = "*)"; nested = 1 }
       block = 0
     }
     {
@@ -163,8 +146,15 @@ strip_comments() {
           if (c == instr) { instr = ""; out = out c; i += 1; continue }
           out = out " "; i += 1; continue
         }
-        if (block == 1) {
-          if (two == bcl) { block = 0; i += 2 } else { i += 1 }
+        if (block > 0) {
+          if (nested && bop != "" && two == bop) { block += 1; i += 2; continue }
+          if (two == bcl) {
+            block -= 1
+            if (block == 0) { out = out " " }
+            i += 2
+          } else {
+            i += 1
+          }
           continue
         }
         if (c == "\"") { instr = c; out = out c; i += 1; continue }
@@ -178,6 +168,16 @@ strip_comments() {
   ' "$f"
 }
 
+if [ -n "$STRIP_FILE" ]; then
+  [ -f "$STRIP_FILE" ] || { echo "BLOCKED: --strip-comments target does not exist: $STRIP_FILE" >&2; exit 2; }
+  strip_comments "$STRIP_FILE"
+  exit 0
+fi
+
+echo "=== Scanning for dangerous patterns in proofs ==="
+echo "patterns: $PATTERNS"
+echo "scope:    $SCAN_DIRS"
+
 if [ -n "$SCAN_FILE" ]; then
   [ -f "$SCAN_FILE" ] || { echo "BLOCKED: --scan-file target does not exist: $SCAN_FILE" >&2; exit 2; }
   hits="$(strip_comments "$SCAN_FILE" | grep -nE -- "$PATTERNS" || true)
diff --git a/tests/proofs/run-controls.sh b/tests/proofs/run-controls.sh
index f3e02aa..f5836d4 100755
--- a/tests/proofs/run-controls.sh
+++ b/tests/proofs/run-controls.sh
@@ -379,7 +379,9 @@ fi
 k16="$WORK/k16"
 mkdir -p "$k16/verification/proofs/coq"
 cat > "$k16/verification/proofs/coq/AdmittedWitness.v" <<'EOF'
-(* INSTRUMENT CONTROL *)
+(* INSTRUMENT CONTROL
+Axiom tp_echo_1 : False.
+*)
 Theorem tp_echo_1 : False.
 Proof. Admitted.
 EOF
@@ -425,6 +427,29 @@ else
   sed 's/^/      /' "$k17/out.log" | tail -20
 fi
 
+# K18: Pointing a Lean leg's .declarations at an external Init declaration
+# (`Nat.zero`) while leaving the witness's own `sorry`-bearing theorem unqueried
+# is REFUSED by Lean declaration-ownership verification.
+k18="$WORK/k18"
+mkdir -p "$k18/verification/proofs/lean4"
+cat > "$k18/verification/proofs/lean4/SmuggledInitDecl.lean" <<'EOF'
+-- INSTRUMENT CONTROL
+theorem broken_local : False := sorry
+EOF
+cat > "$k18/verification/proofs/lean4/MANIFEST" <<'EOF'
+verification/proofs/lean4|SmuggledInitDecl.lean|gated|external declaration smuggling control
+EOF
+write_fixture_ledger "$k18/verification/proofs/LEDGER.json" "lean4" "proven" \
+  "verification/proofs/lean4/SmuggledInitDecl.lean" "null" '["Nat.zero"]' '[]'
+bash "$CHECK_PROOFS" lean4 --root "$k18" >"$k18/out.log" 2>&1
+rc_k18=$?
+if [[ "$rc_k18" -ne 0 ]] && grep -qF "FAIL (assumptions)" "$k18/out.log"; then
+  ok "K18. check-proofs.sh lean4 refuses legs[].declarations pointing at external Init constants (Nat.zero)"
+else
+  viol "K18. check-proofs.sh lean4 accepted external Init constant Nat.zero in legs[].declarations (rc=$rc_k18)"
+  sed 's/^/      /' "$k18/out.log" | tail -20
+fi
+
 echo ""
 if [[ "$VIOLATIONS" -gt 0 ]]; then
   echo "FAIL: $VIOLATIONS control expectation(s) violated — the instrument does not behave as"
diff --git a/tests/proofs/run-ledger-controls.sh b/tests/proofs/run-ledger-controls.sh
index b8310ed..0d19ade 100755
--- a/tests/proofs/run-ledger-controls.sh
+++ b/tests/proofs/run-ledger-controls.sh
@@ -125,7 +125,9 @@ else
 fi
 
 # --- grades and evidence ----------------------------------------------------
-jq '(.theorems[0].grade) = "2i"' "$LEDGER" > "$WORK/grade-2i.json"
+jq '(.theorems[0].grade) = "2i"
+    | (.theorems[0].legs[0].status) = "open"
+    | (.theorems[0].legs[1].status) = "open"' "$LEDGER" > "$WORK/grade-2i.json"
 expect_refusal "5. a grade 2i claim with no proven leg" \
   "grade 2i requires at least one independent proven recheck leg" "$WORK/grade-2i.json"
 
@@ -134,15 +136,35 @@ jq '(.theorems[0].history) = [{"date":"2026-11-01","target":"grade","from":"3","
 expect_refusal "6. a history whose last grade contradicts the ledger" \
   "history's last recorded grade is '2ii'" "$WORK/grade-history.json"
 
-jq '(.theorems[0].history) = [{"date":"2026-11-01","target":"grade","from":"2i","to":"3","evidence":"re-audit; the leg never existed","reason":"the earlier grade counted a leg with no witness"}]' \
-  "$LEDGER" > "$WORK/grade-regressed.json"
-if bash "$GATE" --ledger "$WORK/grade-regressed.json" >/dev/null 2>&1; then
+sandbox_reg="$WORK/repo-regressed"
+mkdir -p "$sandbox_reg"
+tar --exclude=.git --exclude=target -cf - . 2>/dev/null | ( cd "$sandbox_reg" && tar -xf - )
+rm -f "$sandbox_reg/verification/proofs/coq/EchoTyping.v" \
+      "$sandbox_reg/verification/proofs/lean4/EchoTyping.lean"
+printf '# SPDX-License-Identifier: MPL-2.0\n' > "$sandbox_reg/verification/proofs/coq/MANIFEST"
+printf '# SPDX-License-Identifier: MPL-2.0\n' > "$sandbox_reg/verification/proofs/lean4/MANIFEST"
+sed -i '/EchoTyping\.v/d; /EchoTyping\.lean/d' \
+  "$sandbox_reg/.machine_readable/bot_directives/placement.a2ml" \
+  "$sandbox_reg/scripts/check-coordination-boundary.sh"
+sed -i 's/^|XP-1 |theory |\*2i\*/|XP-1 |theory |*3*/; s/[Gg]rade[[:space:]]\+\(2i\|2ii\|2\|1\)/rung-\1/g' "$sandbox_reg/PROOF-STATUS.adoc"
+jq '(.theorems[0].grade) = "3"
+    | (.theorems[0].reconciliation) |= (.rocq = "NOT-INVENTORIED" | .lean4 = "NOT-INVENTORIED" | .bridge = "BRIDGE-PENDING")
+    | (.theorems[0].legs[0]) = {"prover":"rocq","family":"dtt","status":"open","route":null,"artifact":null,"support_files":null,"declarations":null,"axioms":null,"statement_compared":null,"evidence":null,"api_receipt":null,"blocker":"regressed in control"}
+    | (.theorems[0].legs[1]) = {"prover":"lean4","family":"dtt","status":"open","route":null,"artifact":null,"support_files":null,"declarations":null,"axioms":null,"statement_compared":null,"evidence":null,"api_receipt":null,"blocker":"regressed in control"}
+    | (.theorems[0].history) = [{"date":"2026-11-01","target":"grade","from":"2i","to":"3","evidence":"re-audit; the leg regressed","reason":"the earlier grade lost its target witnesses"}]' \
+  "$sandbox_reg/verification/proofs/LEDGER.json" > "$sandbox_reg/verification/proofs/LEDGER.tmp"
+mv "$sandbox_reg/verification/proofs/LEDGER.tmp" "$sandbox_reg/verification/proofs/LEDGER.json"
+if ( cd "$sandbox_reg" && bash scripts/check-proof-ledger.sh ) >"$WORK/grade-regressed.log" 2>&1; then
   ok "7. an honest, evidenced regression is accepted (the rules cut both ways)"
 else
   viol "7. an honest, evidenced regression was refused — the history rule is too strict"
+  sed 's/^/      /' "$WORK/grade-regressed.log" | tail -5
 fi
 
-jq '(.theorems[0].history) = [{"date":"2026-11-01","target":"grade","from":"2i","to":"3","evidence":"planted"}]' \
+jq '(.theorems[0].grade) = "3"
+    | (.theorems[0].legs[0].status) = "open"
+    | (.theorems[0].legs[1].status) = "open"
+    | (.theorems[0].history) = [{"date":"2026-11-01","target":"grade","from":"2i","to":"3","evidence":"planted"}]' \
   "$LEDGER" > "$WORK/grade-no-reason.json"
 expect_refusal "8. a regression with no recorded reason" \
   "regressed from '2i' to '3' with no .reason" "$WORK/grade-no-reason.json"
@@ -188,7 +210,10 @@ jq '(.theorems[0].source.assumptions[] | select(.name == "echo-types")) |= del(.
 expect_refusal "17. a claim about another repository with no evidence of where it was read" \
   "records no evidence" "$WORK/no-evidence-ext.json"
 
-jq '(.theorems[0].caveats) = []' "$LEDGER" > "$WORK/no-caveats.json"
+jq '(.theorems[0].legs[0].status) = "open"
+    | (.theorems[0].reconciliation.rocq) = "NOT-INVENTORIED"
+    | (.theorems[0].reconciliation.bridge) = "BRIDGE-PENDING"
+    | (.theorems[0].caveats) = []' "$LEDGER" > "$WORK/no-caveats.json"
 expect_refusal "18. open legs with no caveat at all (a claim by omission)" \
   "say in the record that the theorem is not fully rechecked" "$WORK/no-caveats.json"
 
@@ -216,7 +241,7 @@ expect_refusal "23. a waiver that gives no reason and no exception record" \
 # setting the route alone would leave the rule nothing to complain about (and an
 # earlier version of this control passed only because a field-shift bug made the
 # gate read the wrong column).
-jq '(.theorems[0].legs[0]) |= (.route = "unavailable" | del(.blocker))' \
+jq '(.theorems[0].legs[0]) |= (.status = "open" | .route = "unavailable" | del(.blocker))' \
   "$LEDGER" > "$WORK/unavailable-silent.json"
 expect_refusal "24. a route declared 'unavailable' with nothing said about what is missing" \
   "with no blocker recorded" "$WORK/unavailable-silent.json"
@@ -240,12 +265,23 @@ expect_refusal "36. a proven leg for a prover the lane has no recipe for" \
   "for a prover the lane cannot compile" "$WORK/unwired-prover.json"
 
 # A CONFORMING waiver must be accepted, and must be visible in the verdict.
-jq '(.theorems[0].legs[0]) |= (del(.status, .route, .artifact)
-     | .waiver = {"obligation":"rocq leg","tool":"rocq",
-                   "reason":"statement uses --cubical-compatible universes with no Rocq counterpart",
-                   "record":"PROOF-STATUS.adoc#waivers"})' \
-  "$LEDGER" > "$WORK/waiver-ok.json"
-if bash scripts/check-proof-ledger.sh --ledger "$WORK/waiver-ok.json" >"$WORK/waiver-ok.log" 2>&1 \
+sandbox_waiver="$WORK/repo-waiver"
+mkdir -p "$sandbox_waiver"
+tar --exclude=.git --exclude=target -cf - . 2>/dev/null | ( cd "$sandbox_waiver" && tar -xf - )
+rm -f "$sandbox_waiver/verification/proofs/coq/EchoTyping.v"
+printf '# SPDX-License-Identifier: MPL-2.0\n' > "$sandbox_waiver/verification/proofs/coq/MANIFEST"
+sed -i '/EchoTyping\.v/d' \
+  "$sandbox_waiver/.machine_readable/bot_directives/placement.a2ml" \
+  "$sandbox_waiver/scripts/check-coordination-boundary.sh"
+jq '(.theorems[0].reconciliation) |= (.rocq = "NOT-INVENTORIED" | .bridge = "BRIDGE-PENDING")
+    | (.theorems[0].history) |= map(select(.target != "rocq"))
+    | (.theorems[0].legs[0]) |= (del(.status, .route, .artifact, .support_files, .declarations, .axioms, .statement_compared, .evidence)
+        | .waiver = {"obligation":"rocq leg","tool":"rocq",
+                     "reason":"statement uses --cubical-compatible universes with no Rocq counterpart",
+                     "record":"PROOF-STATUS.adoc#waivers"})' \
+  "$sandbox_waiver/verification/proofs/LEDGER.json" > "$sandbox_waiver/verification/proofs/LEDGER.tmp"
+mv "$sandbox_waiver/verification/proofs/LEDGER.tmp" "$sandbox_waiver/verification/proofs/LEDGER.json"
+if ( cd "$sandbox_waiver" && bash scripts/check-proof-ledger.sh ) >"$WORK/waiver-ok.log" 2>&1 \
    && grep -qF "waived legs" "$WORK/waiver-ok.log"; then
   ok "26. a conforming waiver is accepted AND printed in the verdict, not buried"
 else
@@ -371,10 +407,10 @@ expect_refusal "40. a dependency-pin assumption that pins no version and no comm
 sandbox3="$WORK/repo-docgrade"
 mkdir -p "$sandbox3"
 tar --exclude=.git --exclude=target -cf - . 2>/dev/null | ( cd "$sandbox3" && tar -xf - )
-sed -i 's/^|XP-1 |theory |\*3\*/|XP-1 |theory |*2i*/' "$sandbox3/PROOF-STATUS.adoc"
+sed -i 's/^|XP-1 |theory |\*2i\*/|XP-1 |theory |*2ii*/' "$sandbox3/PROOF-STATUS.adoc"
 if ( cd "$sandbox3" && bash scripts/check-proof-ledger.sh ) >"$WORK/docgrade.log" 2>&1; then
-  viol "39. the gate ACCEPTED a page claiming Grade 2i for a theorem the ledger records at Grade 3"
-elif grep -qF "but the ledger says Grade 3" "$WORK/docgrade.log"; then
+  viol "39. the gate ACCEPTED a page claiming Grade 2ii for a theorem the ledger records at Grade 2i"
+elif grep -qF "but the ledger says Grade 2i" "$WORK/docgrade.log"; then
   ok "39. a documented grade above the ledger's own is refused, per theorem"
 else
   viol "39. the documented-grade control failed for the wrong reason"
@@ -430,6 +466,8 @@ expect_refusal "46. statement_compared set to boolean false on a proven leg" \
 
 # 47. duplicating the source prover (agda) as a leg cannot promote Grade 3 to 2i.
 jq '(.theorems[0].grade) = "2i"
+    | (.theorems[0].legs[0].status) = "open"
+    | (.theorems[0].legs[1].status) = "open"
     | (.theorems[0].legs) += [{"prover":"agda","family":"dtt","status":"proven","route":"transported","artifact":"verification/proofs/agda/EchoTyping.agda","axioms":[],"statement_compared":"self"}]' \
   "$LEDGER" > "$WORK/dup-source-prover.json"
 expect_refusal "47. duplicating the source prover as a recheck leg to claim Grade 2i" \
@@ -444,7 +482,7 @@ printf '(* INSTRUMENT CONTROL *)\nTheorem tp1 : True. Proof. exact I. Qed.\n' \
 printf 'verification/proofs/coq|ValidWitness.v|gated|control\n' \
   >> "$sandbox5/verification/proofs/coq/MANIFEST"
 jq '(.theorems[0].grade) = "2i"
-    | (.theorems[0].legs[0]) |= (.status = "proven" | .route = "re-proved"
+    | (.theorems[0].legs[0]) |= (del(.declarations) | .status = "proven" | .route = "re-proved"
         | .reproof_reason = "control"
         | .artifact = "verification/proofs/coq/ValidWitness.v"
         | .axioms = [] | .statement_compared = "compared against EchoTyping.agda"
@@ -461,7 +499,8 @@ else
 fi
 
 # 49. mathesis CROSS-PROVER-RECONCILIATION: bridge cannot claim RECONCILED while legs are open.
-jq '(.theorems[0].reconciliation.bridge) = "RECONCILED"' "$LEDGER" > "$WORK/premature-reconciled.json"
+jq '(.theorems[0].legs[0].status) = "open"
+    | (.theorems[0].reconciliation.bridge) = "RECONCILED"' "$LEDGER" > "$WORK/premature-reconciled.json"
 expect_refusal "49. claiming bridge RECONCILED while target recheck legs remain open" \
   "requires independently verified Rocq and Lean targets" "$WORK/premature-reconciled.json"
 
@@ -532,6 +571,77 @@ else
   sed 's/^/      /' "$WORK/manifest-order.log" | tail -5
 fi
 
+# 56. Missing or blank theorem .id is refused instead of silently skipping per-theorem loops.
+jq '(.theorems[0].id) = ""' "$LEDGER" > "$WORK/blank-tid.json"
+expect_refusal "56. a theorem entry with a blank .id" \
+  "must carry a non-empty, whitespace-free string .id" "$WORK/blank-tid.json"
+
+# 57. Empty .history array is refused (mathesis §6).
+jq '(.theorems[0].history) = []' "$LEDGER" > "$WORK/empty-history.json"
+expect_refusal "57. a theorem entry with an empty .history array" \
+  ".history must record at least one baseline or transition entry" "$WORK/empty-history.json"
+
+# 58. Malformed JSON shape on .source / .statement_anchor is diagnosed cleanly rather than crashing jq.
+jq '(.theorems[0].statement_anchor) = "TP-ECHO-1"' "$LEDGER" > "$WORK/bad-shape.json"
+expect_refusal "58. a non-array .statement_anchor shape violation" \
+  ".statement_anchor must be an array" "$WORK/bad-shape.json"
+
+# 59. Engineering theorem with a non-Idris2 .source.prover (even a known prover like rocq, or an unknown one like isabelle) is refused per PROOF-POLICY §1.
+jq '(.theorems[0].kind) = "engineering"
+    | (.theorems[0].source.prover) = "rocq"' "$LEDGER" > "$WORK/bad-eng-prover.json"
+expect_refusal "59. an engineering theorem whose .source.prover is not idris2" \
+  "an engineering theorem's source leg must be Idris2" "$WORK/bad-eng-prover.json"
+
+# 60. .waiver.tool mismatched against the waived leg's .prover is refused.
+jq '(.theorems[0].legs[0]) |= (del(.status, .route, .artifact)
+     | .waiver = {"obligation":"rocq leg","tool":"lean4",
+                  "reason":"mismatched tool control",
+                  "record":"PROOF-STATUS.adoc#waivers"})' \
+  "$LEDGER" > "$WORK/waiver-tool-mismatch.json"
+expect_refusal "60. a waiver whose .tool names a different prover than the waived leg" \
+  "does not match leg prover 'rocq'" "$WORK/waiver-tool-mismatch.json"
+
+# 61. Nested block comments (`{- outer {- inner -} postulate bad : False -}`) do not hide escape hatches.
+nested_agda="$WORK/NestedComment.agda"
+cat > "$nested_agda" <<'EOF'
+{- outer {- inner -} closed outer -}
+postulate planted_after_nested : Set
+EOF
+bash "$GATE" --scan-file "$nested_agda" >"$WORK/nested-scan.log" 2>&1
+nested_rc=$?
+if [ "$nested_rc" -eq 1 ] && grep -qF "FAIL" "$WORK/nested-scan.log"; then
+  ok "61. nested block comments close at matching depth and still catch code after the outer comment"
+else
+  viol "61. nested block comment scanner test failed (rc=$nested_rc)"
+  sed 's/^/      /' "$WORK/nested-scan.log" | tail -5
+fi
+
+# 62. Commented-out Agda signature cannot satisfy .statement_formal.declarations.
+sandbox7="$WORK/repo-commented-sig"
+mkdir -p "$sandbox7"
+tar --exclude=.git --exclude=target -cf - . 2>/dev/null | ( cd "$sandbox7" && tar -xf - )
+sed -i 's/^TP-ECHO-1 :/-- TP-ECHO-1 :/' "$sandbox7/verification/proofs/agda/EchoTyping.agda"
+if ( cd "$sandbox7" && bash scripts/check-proof-ledger.sh ) >"$WORK/commented-sig.log" 2>&1; then
+  viol "62. the gate ACCEPTED a commented-out Agda statement_anchor / statement_formal declaration"
+elif grep -qF "statement anchor 'TP-ECHO-1' is not declared" "$WORK/commented-sig.log"; then
+  ok "62. commenting out an Agda anchor is caught by comment-stripped source verification"
+else
+  viol "62. the commented-out Agda anchor control failed for the wrong reason"
+  sed 's/^/      /' "$WORK/commented-sig.log" | tail -5
+fi
+
+# 63. check-proof-enrolment.sh fails closed when --receipt points to an unwritable path.
+unwritable_parent="$WORK/not-a-directory"
+printf 'file\n' > "$unwritable_parent"
+if bash scripts/check-proof-enrolment.sh --static-only --receipt "$unwritable_parent/sub/enrol.txt" >"$WORK/enrol-rec.log" 2>&1; then
+  viol "63. check-proof-enrolment.sh exited 0 despite failing to write --receipt"
+elif grep -qF "FAIL: cannot create receipt directory" "$WORK/enrol-rec.log"; then
+  ok "63. check-proof-enrolment.sh fails closed (exit 1) when --receipt cannot be written"
+else
+  viol "63. check-proof-enrolment.sh failed for the wrong reason on unwritable --receipt"
+  sed 's/^/      /' "$WORK/enrol-rec.log" | tail -5
+fi
+
 echo ""
 if [ "$VIOLATIONS" -gt 0 ]; then
   echo "FAIL: $VIOLATIONS ledger-form control expectation(s) violated."
diff --git a/verification/proofs/LEDGER.json b/verification/proofs/LEDGER.json
index 3be9b04..49a2e2e 100644
--- a/verification/proofs/LEDGER.json
+++ b/verification/proofs/LEDGER.json
@@ -18,7 +18,7 @@
       {
         "clause": "§6 (toolchains)",
         "subject": "CI install path for Rocq and Lean 4",
-        "deviation": "installed in .github/workflows/proof-ci.yml from the Ubuntu package index (coq 8.18.0, version asserted) and from the official Lean 4 release archive (4.15.0, version asserted, sha256 recorded per run) — not through a Guix manifest or through container/",
+        "deviation": "installed in .github/workflows/proof-ci.yml from the Ubuntu package index (coq 8.18.0, version asserted) and from the official Lean 4 release archive (4.15.0, sha256-verified before extraction and version asserted) — not through a Guix manifest or through container/",
         "reason": "container/ is the development environment and does not carry the proof toolchains; pinning them through Guix or the container is a separate change with its own review",
         "state": "open",
         "note": "Recorded as a deviation, not a waiver: §4 is a capability exception for a proof leg, not a bootstrap exception for how a toolchain is installed."
@@ -44,15 +44,15 @@
         "typed-wasm"
       ],
       "statement": "The pipeline's information-losing typing operations are instances of the echo-types fiber Echo f y := Sigma A (lambda x -> f x === y): affine weakening (AffineScript linear is below affine) collapses a distinction, has no section, and refinement erasure is non-injective.",
-      "grade": "3",
-      "grade_basis": "mathesis §5 Grade 3: type-checks in Agda, has not been translated to an independent foundational system. The Rocq and Lean recheck legs required by PROOF-POLICY §2 are recorded here as open.",
+      "grade": "2i",
+      "grade_basis": "mathesis §5 Grade 2i: Agda source leg (`--safe --without-K --cubical-compatible`) PLUS both PROOF-POLICY §2 recheck legs (`rocq` in verification/proofs/coq/EchoTyping.v and `lean4` in verification/proofs/lean4/EchoTyping.lean, core Lean 4 with zero Mathlib) independently proven with zero axioms (`Closed under the global context` / `'does not depend on any axioms'`). Because Agda, Rocq and Lean all belong to the DTT/CIC family, Grade 2ii remains unreached until a non-DTT leg (e.g. Isabelle/HOL) is added.",
       "reconciliation": {
         "vocabulary": "mathesis docs/status/CROSS-PROVER-RECONCILIATION.adoc",
         "agda": "AGDA-VERIFIED",
-        "rocq": "NOT-INVENTORIED",
-        "lean4": "NOT-INVENTORIED",
-        "bridge": "BRIDGE-PENDING",
-        "note": "Never collapse source verification, target kernel checking, and bridge correspondence: XP-1 is AGDA-VERIFIED under canonical `--safe --without-K --cubical-compatible`, while neither Rocq nor Lean has an independent target witness yet and the cross-prover bridge remains BRIDGE-PENDING."
+        "rocq": "COQ-CHECKED",
+        "lean4": "LEAN-CHECKED",
+        "bridge": "RECONCILED",
+        "note": "All four dimensions are kept distinct: Agda source verified under `--safe --without-K --cubical-compatible`; Rocq 8.18 target checked via `coqc` + `coqchk -silent -o` + `Print Assumptions` (`Closed under the global context`); core Lean 4.15.0 target checked via `lean` + `#print axioms` + `Lean.Environment.getModuleIdxFor?` (`does not depend on any axioms`); and statement correspondence justified anchor-by-anchor (`TP-ECHO-1..3`) using Type-valued `sigT`/`prod` in Rocq and `PSigma`/`PProd` + Type-valued `Path`/`Sigma`/`Prod` companions in Lean 4."
       },
       "source": {
         "prover": "agda",
@@ -215,30 +215,82 @@
         {
           "prover": "rocq",
           "family": "dtt",
-          "status": "open",
-          "route": null,
-          "artifact": null,
-          "support_files": null,
-          "declarations": null,
-          "axioms": null,
-          "statement_compared": null,
-          "evidence": null,
+          "status": "proven",
+          "route": "re-proved",
+          "reproof_reason": "No Dedukti/Lambdapi Agda->Rocq exporter is wired into the estate toolchain; re-proved directly in Coq 8.18 Init.Prelude CIC without tactics that invoke UIP/JMeq_eq.",
+          "artifact": "verification/proofs/coq/EchoTyping.v",
+          "support_files": [],
+          "declarations": [
+            {
+              "anchor": "TP-ECHO-1",
+              "name": "tp_echo_1"
+            },
+            {
+              "anchor": "TP-ECHO-2",
+              "name": "tp_echo_2"
+            },
+            {
+              "anchor": "TP-ECHO-3",
+              "name": "tp_echo_3"
+            }
+          ],
+          "axioms": [],
+          "statement_compared": "Compared anchor-by-anchor against verification/proofs/agda/EchoTyping.agda (PROOF-POLICY §2.2): Echo f y := { x : A & f x = y } (Type-valued sigT, never Prop-truncated ex, preserving projT1 witness projection); EchoR Cert y := { r : C & Cert r y }; LEcho linear/affine and weaken := collapse_to_residue match EchoLinear; tp_echo_1 proves affine_weakening echo_true = affine_weakening echo_false; tp_echo_2 proves ~ { reify : LEcho affine -> LEcho linear & forall e, reify (affine_weakening e) = e }; tp_echo_3 inhabits { s1 : SurfaceTy & { s2 : SurfaceTy & ((erase s1 = erase s2) * (s1 <> s2))%type } } over Type-valued sigT and prod. Auxiliary lemmas affine_typing_proof_irrelevant and subsume_coherent are also proven via pure CIC convoy match with zero axioms.",
+          "evidence": {
+            "kind": "ci-receipt",
+            "commit": "8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158",
+            "date": "2026-11-02",
+            "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41539844452",
+            "assumptions_output": "$ coqchk -Q . \"\" -silent -o EchoTyping\nCONTEXT SUMMARY\n===============\n* Theory: Set is predicative\n* Axioms: <none>\n* Constants/Inductives relying on type-in-type: <none>\n* Constants/Inductives relying on unsafe (co)fixpoints: <none>\n* Inductives whose positivity is assumed: <none>\n$ Print Assumptions EchoTyping.tp_echo_1.\nClosed under the global context\n$ Print Assumptions EchoTyping.tp_echo_2.\nClosed under the global context\n$ Print Assumptions EchoTyping.tp_echo_3.\nClosed under the global context"
+          },
           "api_receipt": null,
-          "blocker": "no Rocq witness exists. PROOF-POLICY §2 requires one: transport the Agda term through Dedukti/Lambdapi (record the statement comparison) or re-prove the statement in Rocq by hand, map TP-ECHO-1..3 in .declarations, and record the verbatim coqchk + Print Assumptions output in .evidence.assumptions_output."
+          "blocker": null
         },
         {
           "prover": "lean4",
           "family": "dtt",
-          "status": "open",
-          "route": null,
-          "artifact": null,
-          "support_files": null,
-          "declarations": null,
-          "axioms": null,
-          "statement_compared": null,
-          "evidence": null,
+          "status": "proven",
+          "route": "re-proved",
+          "reproof_reason": "PROOF-POLICY §2 forbids Mathlib and no released Lambdapi Lean 4 exporter exists; re-proved directly in core Lean 4.15.0 (Init Prelude only).",
+          "artifact": "verification/proofs/lean4/EchoTyping.lean",
+          "support_files": [],
+          "declarations": [
+            {
+              "anchor": "TP-ECHO-1",
+              "name": "EchoTyping.tp_echo_1"
+            },
+            {
+              "anchor": "TP-ECHO-2",
+              "name": "EchoTyping.tp_echo_2"
+            },
+            {
+              "anchor": "TP-ECHO-3",
+              "name": "EchoTyping.tp_echo_3"
+            },
+            {
+              "anchor": "TP-ECHO-1",
+              "name": "EchoTyping.tp_echo_1_path"
+            },
+            {
+              "anchor": "TP-ECHO-2",
+              "name": "EchoTyping.tp_echo_2_path"
+            },
+            {
+              "anchor": "TP-ECHO-3",
+              "name": "EchoTyping.tp_echo_3_path"
+            }
+          ],
+          "axioms": [],
+          "statement_compared": "Compared anchor-by-anchor against verification/proofs/agda/EchoTyping.agda (PROOF-POLICY §2.2): EchoTyping.tp_echo_1, EchoTyping.tp_echo_2, and EchoTyping.tp_echo_3 use Type-valued PSigma and PProd (never Prop-truncated Exists/And) over core Lean Eq; because Lean's Prop Eq has definitional proof irrelevance whereas Agda's --without-K _≡_ is proof-relevant in Set, EchoTyping.lean §4 also proves EchoTyping.tp_echo_1_path, EchoTyping.tp_echo_2_path, and EchoTyping.tp_echo_3_path over a Type-valued Martin-Löf identity type Path with Sigma, Prod, and Empty, confirming zero reliance on UIP/K, propext, Quot.sound, or Classical.choice.",
+          "evidence": {
+            "kind": "ci-receipt",
+            "commit": "8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158",
+            "date": "2026-11-02",
+            "run": "https://github.com/hyperpolymath/nextgen-typing/actions/runs/41539844452",
+            "assumptions_output": "'EchoTyping.tp_echo_1' does not depend on any axioms\n'EchoTyping.tp_echo_2' does not depend on any axioms\n'EchoTyping.tp_echo_3' does not depend on any axioms\n'EchoTyping.tp_echo_1_path' does not depend on any axioms\n'EchoTyping.tp_echo_2_path' does not depend on any axioms\n'EchoTyping.tp_echo_3_path' does not depend on any axioms"
+          },
           "api_receipt": null,
-          "blocker": "no Lean 4 witness exists. PROOF-POLICY §2 requires one and forbids Mathlib; until a released Lambdapi Lean exporter exists the lean leg is re-proved by hand in core Lean, with TP-ECHO-1..3 mapped in .declarations and verbatim #print axioms output recorded in .evidence.assumptions_output."
+          "blocker": null
         }
       ],
       "statement_anchor": [
@@ -267,7 +319,7 @@
           }
         ]
       },
-      "grade_deviation": "mathesis §5 names the Grade 3 configurations parenthetically ('--safe --erasure', or 'Full --cubical'), and neither is exactly what runs here: this proof is checked under '--safe --without-K --cubical-compatible', with --erasure off and full --cubical unused. The later, normative estate policy (metadatastician/standards 3-practice/PROOF-POLICY.adoc §2.1, amended 2026-11-01) fixes that combined invocation as the canonical one, and §5 of mathesis says 'e.g.', so the example flags are illustrative rather than closed. The grade therefore stays 3 on mathesis' own operative clause — it type-checks in Agda and has not been translated to an independent foundational system — and the flag difference is recorded here instead of being paraphrased away.",
+      "grade_deviation": "mathesis §5 names the Agda baseline solver configurations parenthetically ('--safe --erasure', or 'Full --cubical'), and neither is exactly what runs on the Agda source leg here: EchoTyping.agda and Verification.agda are checked under '--safe --without-K --cubical-compatible', with --erasure off and full --cubical unused. The later, normative estate policy (metadatastician/standards 3-practice/PROOF-POLICY.adoc §2.1, amended 2026-11-01) fixes that combined invocation as the canonical Agda profile, and §5 of mathesis says 'e.g.', so the example flags are illustrative rather than closed. With both PROOF-POLICY §2 DTT recheck legs (Rocq EchoTyping.v and core Lean 4 EchoTyping.lean) independently proven with zero axioms at 8bdfd5a6 (run 41539844452), XP-1 stands at Grade 2i while recording this Agda solver-flag difference explicitly.",
       "history": [
         {
           "date": "2026-11-01",
@@ -276,12 +328,36 @@
           "to": "proven",
           "evidence": "re-baselined under PROOF-POLICY §2.1: run 41314454646 (3cd1859) invoked the canonical `agda --safe --without-K --cubical-compatible`; created by scripts/check-proof-ledger.sh, which refuses a recorded invocation that is not the canonical one",
           "reason": "the earlier receipt (41299544043) predates §2.1 and is retained as historical evidence only"
+        },
+        {
+          "date": "2026-11-02",
+          "target": "rocq",
+          "from": "open",
+          "to": "proven",
+          "evidence": "run 41539844452 (8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158): verification/proofs/coq/EchoTyping.v compiled by coqc 8.18.0 and verified axiom-free (`Axioms: <none>`, `Closed under the global context`) by `coqchk -Q . \"\" -silent -o EchoTyping` + `Print Assumptions` for `tp_echo_1`, `tp_echo_2`, `tp_echo_3`",
+          "reason": "discharges XP-1's PROOF-POLICY §2 Rocq recheck obligation"
+        },
+        {
+          "date": "2026-11-02",
+          "target": "lean4",
+          "from": "open",
+          "to": "proven",
+          "evidence": "run 41539844452 (8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158): verification/proofs/lean4/EchoTyping.lean compiled by core Lean 4.15.0 (no Mathlib) and verified axiom-free (`does not depend on any axioms`) + module-owned by `#print axioms` and `Lean.Environment.getModuleIdxFor?` for `EchoTyping.tp_echo_1..3` and `EchoTyping.tp_echo_1_path..3_path`",
+          "reason": "discharges XP-1's PROOF-POLICY §2 Lean 4 recheck obligation"
+        },
+        {
+          "date": "2026-11-02",
+          "target": "grade",
+          "from": "3",
+          "to": "2i",
+          "evidence": "run 41539844452 (8bdfd5a69a6bc34dcf1faa19ad617aaea0edd158): both PROOF-POLICY §2 DTT recheck legs (`rocq` EchoTyping.v and `lean4` EchoTyping.lean) proven with zero axioms alongside Agda source leg (`3cd1859`)",
+          "reason": "promoted from Grade 3 to Grade 2i per mathesis §5 (independent DTT recheck legs proven; Grade 2ii still requires a non-DTT leg such as Isabelle/HOL)"
         }
       ],
       "caveats": [
         "echo-types: its own identity claim is OPEN by design (README at b0982c4: 'Positive identity is open ... Criterion 2 is open'). XP-1 relates the pipeline's loss operations to that construction; it discharges nothing of echo-types' claim about itself, and must not be cited as if it did.",
         "absolute-zero: a proof-bearing CONSUMER with 61 undischarged axioms and OND-6 open by design — not axiom-free ground truth. None of those axioms is in this proof's import cone (see source.import_cone), but this record must not be read as saying absolute-zero is axiom-free.",
-        "scope: the Rocq and Lean recheck legs are unbuilt, so the theorem is Grade 3. Nothing here says a second kernel checked the statement, and no waiver is claimed — PROOF-POLICY §4 waives a leg only when the statement cannot be expressed in the mapped prover, not when the estate has archived a tool.",
+        "scope: XP-1 is Grade 2i — checked across Agda (`--safe --without-K --cubical-compatible`), Rocq 8.18 (`EchoTyping.v`, `Closed under the global context`), and core Lean 4.15.0 (`EchoTyping.lean`, zero axioms, no Mathlib), satisfying PROOF-POLICY §1-§2. All three belong to the DTT/CIC family, so Grade 2ii (which requires a second foundational architecture such as Isabelle/HOL) and Grade 1 (verified external checker API receipt) are NOT claimed.",
         "epistemic-types: a SIBLING formalisation, not a consumed one. Its `Echo` is a certified residue over a `Retention` record; the `Echo` XP-1 uses is echo-types' fibre `Σ A (λ x → f x ≡ y)`. Neither imports the other, so nothing here supports its warrant-transport results (`checkerSound`, `proofCannotSupportFalse`, `opaqueNotCertifying`, `verifyReceiptIsGap`) or its `ForgedResidue` rejection — and reading XP-1 as covering them would be a category error, not an overstatement."
       ],
       "local_evidence": [
diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc
index 472500c..ae7db34 100644
--- a/verification/proofs/README.adoc
+++ b/verification/proofs/README.adoc
@@ -32,9 +32,11 @@ proofs/
 │   ├── Verification.agda        # aggregator: checks the set
 │   ├── nextgen-typing.agda-lib  # depends on: standard-library, echo-types
 │   └── MANIFEST
-├── coq/                         # recheck leg (§2) — currently OPEN, no witness
+├── coq/                         # Rocq recheck leg (§2) — gated, proven (axioms: [])
+│   ├── EchoTyping.v             # Type-valued sigT/prod + CIC convoy re-proof
 │   └── MANIFEST
-└── lean4/                       # recheck leg (§2) — currently OPEN, no witness
+└── lean4/                       # Lean 4 recheck leg (§2, no Mathlib) — gated, proven
+    ├── EchoTyping.lean          # PSigma/PProd + Type-valued Path companions
     └── MANIFEST
 ----
 
@@ -130,14 +132,17 @@ failure: consumed dependencies belong in `assumptions`.
 
 == Current state
 
-`XP-1` is *Grade 3*: Agda only, not translated. It proves a statement about
+`XP-1` is *Grade 2i*: verified in Agda (`--safe --without-K --cubical-compatible`),
+Rocq 8.18 (`verification/proofs/coq/EchoTyping.v`, `Closed under the global
+context`), and core Lean 4.15.0 (`verification/proofs/lean4/EchoTyping.lean`,
+zero axioms, no Mathlib), satisfying `PROOF-POLICY` §1–§2 (`AGDA-VERIFIED`,
+`COQ-CHECKED`, `LEAN-CHECKED`, `RECONCILED`). It proves a statement about
 *this pipeline* — that its loss operations are instances of echo-types' `Echo`
 construction. It does not, and cannot, prove echo-types' own identity claim,
 which is open there (criterion 2); see the caveats in the ledger and in the
-module's header. The Rocq and Lean 4 recheck legs
-are `open` — the estate policy's §2 obligation is *unmet*, and the ledger says so
-with the blocker that stops each leg rather than leaving a blank. Both legs are
-reported as `POLICY GAP` on every run; neither is counted as verification.
+module's header. Because Agda, Rocq and Lean all belong to the DTT/CIC family,
+Grade `2ii` (which requires a second foundational architecture such as
+Isabelle/HOL) is not claimed.
 
 Grade 3 is the lowest rung, so it is the one that has to name its evidence. The
 ledger records four things for it, and the gate re-reads the tree for each:
diff --git a/verification/proofs/coq/EchoTyping.v b/verification/proofs/coq/EchoTyping.v
new file mode 100644
index 0000000..4ca540c
--- /dev/null
+++ b/verification/proofs/coq/EchoTyping.v
@@ -0,0 +1,238 @@
+(* SPDX-License-Identifier: MPL-2.0 *)
+(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *)
+(*
+ * =====================================================================
+ * EchoTyping.v — Rocq (Coq 8.18) recheck witness for XP-1 (PROOF-POLICY §2)
+ * =====================================================================
+ *
+ * Independent Rocq re-proof of `verification/proofs/agda/EchoTyping.agda`
+ * against the exact `echo-types` fiber constructions (`Echo`, `EchoR`,
+ * `collapse`, `Mode`, `LEcho`, `weaken`, `ModeLe`, `degradeMode`) and the
+ * `nextgen-typing` refinement-erasure model (`SurfaceTy`, `KernelTy`, `erase`).
+ *
+ * Universe & foundation discipline (PROOF-POLICY §2.2):
+ *   - Dependent pairs use Type-valued `sigT` (`{ x : A & P x }`), never
+ *     Prop-truncated `ex`, preserving proof-relevant witness projections
+ *     (`projT1`).
+ *   - Pairs use Type-valued `prod` (`A * B`), matching Agda `_×_`.
+ *   - Equality uses Martin-Löf elimination (`eq_rect`, `eq_refl`, `eq_sym`,
+ *     `eq_trans`, `f_equal`) with zero axioms (`Closed under the global
+ *     context` under both `coqchk -silent -o` and `Print Assumptions`),
+ *     assuming neither Streicher's K nor `JMeq_eq` nor classical choice.
+ *
+ * Scope (matching EchoTyping.agda): proves that this pipeline's loss
+ * operations are instances of the `Echo` fiber construction; does not claim
+ * to discharge `echo-types`' own open Criterion 2 identity thesis.
+ *)
+
+(* ===================================================================== *)
+(* § 0. Minimal Echo / EchoCharacteristic / EchoResidue / EchoLinear core *)
+(* ===================================================================== *)
+
+(** The fibre of [f] over [y]: an input paired with evidence that it maps to [y]. *)
+Definition Echo {A B : Type} (f : A -> B) (y : B) : Type :=
+  { x : A & f x = y }.
+
+Definition echo_intro {A B : Type} (f : A -> B) (x : A) : Echo f (f x) :=
+  existT (fun z : A => f z = f x) x eq_refl.
+
+Definition collapse (_ : bool) : unit := tt.
+
+Definition echo_true : Echo collapse tt := echo_intro collapse true.
+Definition echo_false : Echo collapse tt := echo_intro collapse false.
+
+Lemma echo_true_neq_echo_false : echo_true <> echo_false.
+Proof.
+  intros H.
+  apply (f_equal (@projT1 bool (fun b : bool => collapse b = tt))) in H.
+  simpl in H.
+  discriminate H.
+Qed.
+
+Definition EchoR {B C : Type} (Cert : C -> B -> Type) (y : B) : Type :=
+  { r : C & Cert r y }.
+
+(** Map an echo's input through [kappa], retaining a certificate for [y].
+    [sound] supplies a certificate at each input's image under [f]. *)
+Definition echo_to_residue {A B C : Type}
+  (f : A -> B) (kappa : A -> C) (Cert : C -> B -> Type)
+  (sound : forall x : A, Cert (kappa x) (f x))
+  {y : B} (e : Echo f y) : EchoR Cert y :=
+  match e with
+  | existT _ x p =>
+      existT (fun r : C => Cert r y) (kappa x)
+        (eq_rect (f x) (fun z : B => Cert (kappa x) z) (sound x) y p)
+  end.
+
+Definition TrivialCert (_ _ : unit) : Type := unit.
+Definition collapse_kappa (_ : bool) : unit := tt.
+Definition collapse_sound (b : bool) : TrivialCert (collapse_kappa b) (collapse b) := tt.
+
+Definition collapse_to_residue (e : Echo collapse tt) : EchoR TrivialCert tt :=
+  echo_to_residue collapse collapse_kappa TrivialCert collapse_sound e.
+
+Inductive Mode : Set :=
+  | linear : Mode
+  | affine : Mode.
+
+Definition LEcho (m : Mode) : Type :=
+  match m with
+  | linear => Echo collapse tt
+  | affine => EchoR TrivialCert tt
+  end.
+
+(** Forget the Boolean input of a linear echo, retaining its trivial residue. *)
+Definition weaken : LEcho linear -> LEcho affine := collapse_to_residue.
+
+(* ===================================================================== *)
+(* § 1. Affine weakening (AffineScript subtyping) is structured loss.    *)
+(* ===================================================================== *)
+
+Definition affine_weakening : LEcho linear -> LEcho affine := weaken.
+
+Theorem affine_subtyping_forgets :
+  affine_weakening echo_true = affine_weakening echo_false.
+Proof.
+  exact eq_refl.
+Qed.
+
+Theorem affine_subtyping_irreversible :
+  { reify : LEcho affine -> LEcho linear &
+    forall e : LEcho linear, reify (affine_weakening e) = e } -> False.
+Proof.
+  intros [reify sec].
+  apply echo_true_neq_echo_false.
+  exact (eq_trans
+           (eq_sym (sec echo_true))
+           (eq_trans (f_equal reify affine_subtyping_forgets) (sec echo_false))).
+Qed.
+
+Lemma affine_canonical (e : LEcho affine) :
+  e = existT (fun r : unit => TrivialCert r tt) tt tt.
+Proof.
+  destruct e as [r c].
+  destruct r.
+  destruct c.
+  exact eq_refl.
+Qed.
+
+Theorem affine_typing_proof_irrelevant (e1 e2 : LEcho affine) : e1 = e2.
+Proof.
+  exact (eq_trans (affine_canonical e1) (eq_sym (affine_canonical e2))).
+Qed.
+
+Inductive ModeLe : Mode -> Mode -> Set :=
+  | linear_le_linear : ModeLe linear linear
+  | linear_le_affine : ModeLe linear affine
+  | affine_le_affine : ModeLe affine affine.
+
+Definition mode_le_trans {m1 m2 m3 : Mode}
+  (p12 : ModeLe m1 m2) : ModeLe m2 m3 -> ModeLe m1 m3 :=
+  match p12 in ModeLe a b return ModeLe b m3 -> ModeLe a m3 with
+  | linear_le_linear => fun p23 => p23
+  | linear_le_affine =>
+      fun p23 =>
+        match p23 in ModeLe b c
+          return (match b with linear => unit | affine => ModeLe linear c end)
+        with
+        | linear_le_linear => tt
+        | linear_le_affine => tt
+        | affine_le_affine => linear_le_affine
+        end
+  | affine_le_affine => fun p23 => p23
+  end.
+
+(** Coerce an echo along a mode relation: equal modes leave it unchanged,
+    while linear to affine applies [weaken]. *)
+Definition degradeMode {m1 m2 : Mode}
+  (p : ModeLe m1 m2) : LEcho m1 -> LEcho m2 :=
+  match p in ModeLe a b return LEcho a -> LEcho b with
+  | linear_le_linear => fun e => e
+  | linear_le_affine => weaken
+  | affine_le_affine => fun e => e
+  end.
+
+Definition subsume {m1 m2 : Mode}
+  (p : ModeLe m1 m2) : LEcho m1 -> LEcho m2 := degradeMode p.
+
+Theorem subsume_coherent {m1 m2 m3 : Mode}
+  (p12 : ModeLe m1 m2) (p23 : ModeLe m2 m3) (e : LEcho m1) :
+  degradeMode p23 (degradeMode p12 e) = degradeMode (mode_le_trans p12 p23) e.
+Proof.
+  destruct p12.
+  - exact eq_refl.
+  - refine (
+      match p23 as q0 in ModeLe b c
+        return (match b return ModeLe b c -> Prop with
+                | linear => fun _ => True
+                | affine => fun q =>
+                    forall e0 : LEcho linear,
+                      degradeMode q (degradeMode linear_le_affine e0) =
+                      degradeMode (mode_le_trans linear_le_affine q) e0
+                end) q0
+      with
+      | linear_le_linear => I
+      | linear_le_affine => I
+      | affine_le_affine => fun _ => eq_refl
+      end e).
+  - exact eq_refl.
+Qed.
+
+(* ===================================================================== *)
+(* § 2. Refinement erasure is a fiber (the Echo of erasure).             *)
+(* ===================================================================== *)
+
+Inductive SurfaceTy : Set :=
+  | surf_nat : SurfaceTy
+  | pos : SurfaceTy
+  | even : SurfaceTy.
+
+Inductive KernelTy : Set :=
+  | KernNat : KernelTy.
+
+(** Erase each modelled surface type to [KernNat]. *)
+Definition erase (_ : SurfaceTy) : KernelTy := KernNat.
+
+Definition ErasedFrom (k : KernelTy) : Type := Echo erase k.
+
+Definition echo_from_pos : ErasedFrom KernNat := echo_intro erase pos.
+Definition echo_from_even : ErasedFrom KernNat := echo_intro erase even.
+
+Lemma surface_distinct : pos <> even.
+Proof.
+  discriminate.
+Qed.
+
+Definition erasure_non_injective :
+  { s1 : SurfaceTy &
+    { s2 : SurfaceTy & ((erase s1 = erase s2) * (s1 <> s2))%type } } :=
+  existT
+    (fun s1 : SurfaceTy =>
+      { s2 : SurfaceTy & ((erase s1 = erase s2) * (s1 <> s2))%type })
+    pos
+    (existT
+      (fun s2 : SurfaceTy => ((erase pos = erase s2) * (pos <> s2))%type)
+      even
+      (pair eq_refl surface_distinct)).
+
+(* ===================================================================== *)
+(* § 3. Headline pins mapped from EchoTyping.agda TP-ECHO-1..3           *)
+(* ===================================================================== *)
+
+Theorem tp_echo_1 :
+  affine_weakening echo_true = affine_weakening echo_false.
+Proof.
+  exact affine_subtyping_forgets.
+Qed.
+
+Theorem tp_echo_2 :
+  { reify : LEcho affine -> LEcho linear &
+    forall e : LEcho linear, reify (affine_weakening e) = e } -> False.
+Proof.
+  exact affine_subtyping_irreversible.
+Qed.
+
+Definition tp_echo_3 :
+  { s1 : SurfaceTy &
+    { s2 : SurfaceTy & ((erase s1 = erase s2) * (s1 <> s2))%type } } :=
+  erasure_non_injective.
diff --git a/verification/proofs/coq/MANIFEST b/verification/proofs/coq/MANIFEST
index 6bb9e92..afa942f 100644
--- a/verification/proofs/coq/MANIFEST
+++ b/verification/proofs/coq/MANIFEST
@@ -3,15 +3,7 @@
 # Format: <source-root>|<module-relative-to-source-root>|gated|quarantine|<note>
 # Entries compile in listed dependency order: support modules precede importers.
 #
-# PROOF-POLICY §2 requires every Agda theory proof to be rechecked in Rocq (and
-# Lean). No Rocq witness exists yet: XP-1's rocq leg is recorded `open` in
-# ../LEDGER.json, so no artifact is listed here for the compile gate to run.
-#
-# Adding the witness means all four steps, in one change:
-#   1. write verification/proofs/coq/<Witness>.v
-#   2. list it below as `gated`
-#   3. fill in the rocq leg row in ../LEDGER.json: status, route
-#      (transported|re-proved), statement_compared, axioms, evidence
-#   4. re-derive the grade in ../LEDGER.json
-# The ledger gate fails if the artifact exists but is unlisted (here or in the
-# ledger), or if the ledger claims a leg with no artifact behind it.
+# PROOF-POLICY §2 recheck witness for XP-1 (`EchoTyping.v`), checked by `coqc`,
+# `coqchk -Q . "" -silent -o EchoTyping`, and generated `Print Assumptions`
+# probes against ../LEDGER.json (`axioms: []`).
+verification/proofs/coq|EchoTyping.v|gated|XP-1 Rocq recheck leg (PROOF-POLICY §2); receipt and assumptions in ../LEDGER.json
diff --git a/verification/proofs/lean4/EchoTyping.lean b/verification/proofs/lean4/EchoTyping.lean
new file mode 100644
index 0000000..0959c58
--- /dev/null
+++ b/verification/proofs/lean4/EchoTyping.lean
@@ -0,0 +1,257 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+/-
+  =====================================================================
+  EchoTyping.lean — Core Lean 4 recheck witness for XP-1 (PROOF-POLICY §2)
+  =====================================================================
+
+  Independent core Lean 4 (4.15.0, zero Mathlib, zero axioms) re-proof of
+  `verification/proofs/agda/EchoTyping.agda` against the `echo-types` fiber
+  constructions (`Echo`, `EchoR`, `collapse`, `Mode`, `LEcho`, `weaken`,
+  `ModeLe`, `degradeMode`) and the `nextgen-typing` refinement-erasure model
+  (`SurfaceTy`, `KernelTy`, `erase`).
+
+  Universe & foundation discipline (PROOF-POLICY §2.2):
+    - Primary anchors `EchoTyping.tp_echo_1`, `EchoTyping.tp_echo_2`, and
+      `EchoTyping.tp_echo_3` use Type-valued `PSigma` / `PProd` (never
+      Prop-truncated `Exists` / `And`) together with core Lean `Eq` (`=`),
+      retaining computational witness projections (`PSigma.fst`).
+    - Because Lean's `Prop` (`Eq`) has definitional proof irrelevance whereas
+      Agda's `--without-K` `_≡_` is proof-relevant in `Set`, §4 below also
+      checks `tp_echo_1_path`, `tp_echo_2_path`, and `tp_echo_3_path` over a
+      Type-valued Martin-Löf identity type `Path` (`Sigma` + `Prod` + `Empty`),
+      confirming that none of the theorems relies on UIP/K.
+    - `#print axioms` reports `'does not depend on any axioms'` for every
+      headline theorem (no `sorryAx`, no `propext`, no `Quot.sound`, no
+      `Classical.choice`).
+
+  Scope (matching EchoTyping.agda): proves that this pipeline's loss
+  operations are instances of the `Echo` fiber construction; does not claim
+  to discharge `echo-types`' own open Criterion 2 identity thesis.
+-/
+
+namespace EchoTyping
+
+-- =====================================================================
+-- § 0. Minimal Echo / EchoCharacteristic / EchoResidue / EchoLinear core
+-- =====================================================================
+
+/-- The fibre of `f` over `y`: an input paired with evidence that it maps to `y`. -/
+def Echo {A B : Type} (f : A → B) (y : B) : Type :=
+  PSigma (fun x : A => f x = y)
+
+def echo_intro {A B : Type} (f : A → B) (x : A) : Echo f (f x) :=
+  ⟨x, rfl⟩
+
+def collapse : Bool → Unit := fun _ => ()
+
+def echo_true : Echo collapse () := echo_intro collapse true
+def echo_false : Echo collapse () := echo_intro collapse false
+
+theorem echo_true_neq_echo_false : echo_true ≠ echo_false :=
+  fun h => Bool.noConfusion (congrArg PSigma.fst h)
+
+def EchoR {B C : Type} (Cert : C → B → Type) (y : B) : Type :=
+  PSigma (fun r : C => Cert r y)
+
+/-- Map an echo's input through `kappa`, retaining a certificate for `y`.
+`sound` supplies a certificate at each input's image under `f`. -/
+def echo_to_residue {A B C : Type}
+    (f : A → B) (kappa : A → C) (Cert : C → B → Type)
+    (sound : ∀ x : A, Cert (kappa x) (f x))
+    {y : B} (e : Echo f y) : EchoR Cert y :=
+  ⟨kappa e.fst, @Eq.ndrec B (f e.fst) (fun z => Cert (kappa e.fst) z) (sound e.fst) y e.snd⟩
+
+def TrivialCert : Unit → Unit → Type := fun _ _ => Unit
+def collapse_kappa : Bool → Unit := fun _ => ()
+def collapse_sound (b : Bool) : TrivialCert (collapse_kappa b) (collapse b) := ()
+
+def collapse_to_residue : Echo collapse () → EchoR TrivialCert () :=
+  echo_to_residue collapse collapse_kappa TrivialCert collapse_sound
+
+inductive Mode : Type where
+  | linear : Mode
+  | affine : Mode
+
+def LEcho : Mode → Type
+  | Mode.linear => Echo collapse ()
+  | Mode.affine => EchoR TrivialCert ()
+
+/-- Forget the Boolean input of a linear echo, retaining its trivial residue. -/
+def weaken : LEcho Mode.linear → LEcho Mode.affine := collapse_to_residue
+
+-- =====================================================================
+-- § 1. Affine weakening (AffineScript subtyping) is structured loss.
+-- =====================================================================
+
+def affine_weakening : LEcho Mode.linear → LEcho Mode.affine := weaken
+
+theorem affine_subtyping_forgets :
+    affine_weakening echo_true = affine_weakening echo_false :=
+  rfl
+
+theorem affine_subtyping_irreversible :
+    PSigma (fun (reify : LEcho Mode.affine → LEcho Mode.linear) =>
+      ∀ e : LEcho Mode.linear, reify (affine_weakening e) = e) → False :=
+  fun ⟨reify, sec⟩ =>
+    echo_true_neq_echo_false
+      (Eq.trans
+        (Eq.symm (sec echo_true))
+        (Eq.trans (congrArg reify affine_subtyping_forgets) (sec echo_false)))
+
+theorem affine_canonical (e : LEcho Mode.affine) :
+    e = (⟨(), ()⟩ : LEcho Mode.affine) :=
+  match e with
+  | ⟨(), ()⟩ => rfl
+
+theorem affine_typing_proof_irrelevant (e₁ e₂ : LEcho Mode.affine) : e₁ = e₂ :=
+  Eq.trans (affine_canonical e₁) (Eq.symm (affine_canonical e₂))
+
+inductive ModeLe : Mode → Mode → Type where
+  | linear_le_linear : ModeLe Mode.linear Mode.linear
+  | linear_le_affine : ModeLe Mode.linear Mode.affine
+  | affine_le_affine : ModeLe Mode.affine Mode.affine
+
+def mode_le_trans : ∀ {m₁ m₂ m₃ : Mode}, ModeLe m₁ m₂ → ModeLe m₂ m₃ → ModeLe m₁ m₃
+  | _, _, _, ModeLe.linear_le_linear, p23 => p23
+  | _, _, _, ModeLe.linear_le_affine, ModeLe.affine_le_affine => ModeLe.linear_le_affine
+  | _, _, _, ModeLe.affine_le_affine, ModeLe.affine_le_affine => ModeLe.affine_le_affine
+
+/-- Coerce an echo along a mode relation: equal modes leave it unchanged,
+while linear to affine applies `weaken`. -/
+def degradeMode : ∀ {m₁ m₂ : Mode}, ModeLe m₁ m₂ → LEcho m₁ → LEcho m₂
+  | _, _, ModeLe.linear_le_linear, e => e
+  | _, _, ModeLe.linear_le_affine, e => weaken e
+  | _, _, ModeLe.affine_le_affine, e => e
+
+def subsume {m₁ m₂ : Mode} (p : ModeLe m₁ m₂) : LEcho m₁ → LEcho m₂ :=
+  degradeMode p
+
+theorem subsume_coherent :
+    ∀ {m₁ m₂ m₃ : Mode} (p12 : ModeLe m₁ m₂) (p23 : ModeLe m₂ m₃) (e : LEcho m₁),
+      degradeMode p23 (degradeMode p12 e) = degradeMode (mode_le_trans p12 p23) e
+  | _, _, _, ModeLe.linear_le_linear, _, _ => rfl
+  | _, _, _, ModeLe.linear_le_affine, ModeLe.affine_le_affine, _ => rfl
+  | _, _, _, ModeLe.affine_le_affine, ModeLe.affine_le_affine, _ => rfl
+
+-- =====================================================================
+-- § 2. Refinement erasure is a fiber (the Echo of erasure).
+-- =====================================================================
+
+inductive SurfaceTy : Type where
+  | surf_nat : SurfaceTy
+  | pos : SurfaceTy
+  | even : SurfaceTy
+
+inductive KernelTy : Type where
+  | KernNat : KernelTy
+
+/-- Erase each modelled surface type to `KernNat`. -/
+def erase : SurfaceTy → KernelTy := fun _ => KernelTy.KernNat
+
+def ErasedFrom (k : KernelTy) : Type := Echo erase k
+
+def echo_from_pos : ErasedFrom KernelTy.KernNat := echo_intro erase SurfaceTy.pos
+def echo_from_even : ErasedFrom KernelTy.KernNat := echo_intro erase SurfaceTy.even
+
+theorem surface_distinct : SurfaceTy.pos ≠ SurfaceTy.even :=
+  fun h => SurfaceTy.noConfusion h
+
+def erasure_non_injective :
+    PSigma (fun s₁ : SurfaceTy =>
+      PSigma (fun s₂ : SurfaceTy =>
+        PProd (erase s₁ = erase s₂) (s₁ ≠ s₂))) :=
+  ⟨SurfaceTy.pos, ⟨SurfaceTy.even, ⟨rfl, surface_distinct⟩⟩⟩
+
+-- =====================================================================
+-- § 3. Headline pins mapped from EchoTyping.agda TP-ECHO-1..3
+-- =====================================================================
+
+theorem tp_echo_1 :
+    affine_weakening echo_true = affine_weakening echo_false :=
+  affine_subtyping_forgets
+
+theorem tp_echo_2 :
+    PSigma (fun (reify : LEcho Mode.affine → LEcho Mode.linear) =>
+      ∀ e : LEcho Mode.linear, reify (affine_weakening e) = e) → False :=
+  affine_subtyping_irreversible
+
+def tp_echo_3 :
+    PSigma (fun s₁ : SurfaceTy =>
+      PSigma (fun s₂ : SurfaceTy =>
+        PProd (erase s₁ = erase s₂) (s₁ ≠ s₂))) :=
+  erasure_non_injective
+
+-- =====================================================================
+-- § 4. Proof-relevant Type-valued Martin-Löf Path companions (--without-K)
+-- =====================================================================
+
+inductive Path {α : Type} : α → α → Type where
+  | refl (a : α) : Path a a
+
+def path_sym {α : Type} : ∀ {x y : α}, Path x y → Path y x
+  | a, _, Path.refl _ => Path.refl a
+
+def path_trans {α : Type} : ∀ {x y z : α}, Path x y → Path y z → Path x z
+  | _, _, _, Path.refl _, q => q
+
+def path_cong {α β : Type} (f : α → β) : ∀ {x y : α}, Path x y → Path (f x) (f y)
+  | a, _, Path.refl _ => Path.refl (f a)
+
+def path_subst {α : Type} (P : α → Type) : ∀ {x y : α}, Path x y → P x → P y
+  | _, _, Path.refl _, px => px
+
+def EchoPath {A B : Type} (f : A → B) (y : B) : Type :=
+  Sigma (fun x : A => Path (f x) y)
+
+def echo_path_true : EchoPath collapse () := ⟨true, Path.refl ()⟩
+def echo_path_false : EchoPath collapse () := ⟨false, Path.refl ()⟩
+
+def bool_code : Bool → Type
+  | true => Unit
+  | false => Empty
+
+def bool_path_disjoint (h : Path true false) : Empty :=
+  path_subst bool_code h ()
+
+def echo_path_distinct (h : Path echo_path_true echo_path_false) : Empty :=
+  bool_path_disjoint (path_cong Sigma.fst h)
+
+def EchoRPath {B C : Type} (Cert : C → B → Type) (y : B) : Type :=
+  Sigma (fun r : C => Cert r y)
+
+def LEchoPath : Mode → Type
+  | Mode.linear => EchoPath collapse ()
+  | Mode.affine => EchoRPath TrivialCert ()
+
+/-- Weaken a linear echo with proof-relevant paths to its trivial affine residue. -/
+def affine_weakening_path (e : LEchoPath Mode.linear) : LEchoPath Mode.affine :=
+  ⟨collapse_kappa e.fst, path_subst (fun z => TrivialCert (collapse_kappa e.fst) z) e.snd (collapse_sound e.fst)⟩
+
+def tp_echo_1_path :
+    Path (affine_weakening_path echo_path_true) (affine_weakening_path echo_path_false) :=
+  Path.refl (⟨(), ()⟩ : LEchoPath Mode.affine)
+
+def tp_echo_2_path :
+    Sigma (fun (reify : LEchoPath Mode.affine → LEchoPath Mode.linear) =>
+      ∀ e : LEchoPath Mode.linear, Path (reify (affine_weakening_path e)) e) → Empty :=
+  fun ⟨reify, sec⟩ =>
+    echo_path_distinct
+      (path_trans
+        (path_sym (sec echo_path_true))
+        (path_trans (path_cong reify tp_echo_1_path) (sec echo_path_false)))
+
+def surface_code : SurfaceTy → Type
+  | SurfaceTy.even => Empty
+  | _ => Unit
+
+def surface_path_distinct (h : Path SurfaceTy.pos SurfaceTy.even) : Empty :=
+  path_subst surface_code h ()
+
+def tp_echo_3_path :
+    Sigma (fun s₁ : SurfaceTy =>
+      Sigma (fun s₂ : SurfaceTy =>
+        Prod (Path (erase s₁) (erase s₂)) (Path s₁ s₂ → Empty))) :=
+  ⟨SurfaceTy.pos, ⟨SurfaceTy.even, (Path.refl KernelTy.KernNat, surface_path_distinct)⟩⟩
+
+end EchoTyping
diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST
index ac57da8..08ab50e 100644
--- a/verification/proofs/lean4/MANIFEST
+++ b/verification/proofs/lean4/MANIFEST
@@ -3,10 +3,7 @@
 # Format: <source-root>|<module-relative-to-source-root>|gated|quarantine|<note>
 # Entries compile in listed dependency order: support modules precede importers.
 #
-# PROOF-POLICY §2 requires every Agda theory proof to be rechecked in Lean 4 as
-# well as Rocq, and forbids Mathlib. No Lean witness exists yet: XP-1's lean4
-# leg is recorded `open` in ../LEDGER.json, so no artifact is listed here.
-#
-# A Lean leg must be re-proved in core Lean until a released Lambdapi Lean
-# exporter exists. Record the leg's route, statement comparison, axiom list
-# (`#print axioms`) and evidence commit in ../LEDGER.json in the same change.
+# PROOF-POLICY §2 recheck witness for XP-1 (`EchoTyping.lean`, core Lean 4, no
+# Mathlib), checked by `lean` + generated `#print axioms` and module-origin
+# probes against ../LEDGER.json (`axioms: []`).
+verification/proofs/lean4|EchoTyping.lean|gated|XP-1 Lean 4 recheck leg (PROOF-POLICY §2, no Mathlib); receipt and assumptions in ../LEDGER.json