Rocq and Lean recheck legs for N-1..3, N-7..9 (PWG-2ii)

.github/workflows/proofs.yml

@@ -81,3 +81,35 @@ jobs:
         run: |
           bash scripts/grade-receipt.sh --write --commit "$(git rev-parse --short=12 HEAD)"
           sed -n '1,80p' verification/receipts/agda_praxis.deed
+
+  # The Rocq and Lean recheck legs (PROOF-POLICY §2), re-proved by hand from
+  # the Agda statements (verification/legs/README.adoc gives the route and the
+  # statement correspondence). Both provers are pinned: Coq by its Ubuntu
+  # package version, Lean by its release tarball's sha256. Neither leg may use
+  # an axiom or a library; scripts/check-legs.sh refuses either.
+  legs:
+    name: Rocq and Lean recheck legs (no axioms, no libraries)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - name: Install the pinned Coq
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -y coq=8.18.0+dfsg-1build2 zstd
+      - name: Install the pinned Lean (release tarball, sha256-checked)
+        env:
+          LEAN_URL: https://github.com/leanprover/lean4/releases/download/v4.24.0/lean-4.24.0-linux.tar.zst
+          LEAN_SHA256: b14f5e5159219dd1a1956c3b806813319f5e94ccd5bdfd56f54520609a5bb5ec
+        run: |
+          set -euo pipefail
+          curl --proto '=https' --proto-redir '=https' --tlsv1.2 -fsSL "$LEAN_URL" -o "$RUNNER_TEMP/lean.tar.zst"
+          echo "$LEAN_SHA256  $RUNNER_TEMP/lean.tar.zst" | sha256sum --check --strict
+          mkdir -p "$RUNNER_TEMP/lean"
+          tar --zstd -xf "$RUNNER_TEMP/lean.tar.zst" -C "$RUNNER_TEMP/lean"
+          echo "$RUNNER_TEMP/lean/lean-4.24.0-linux/bin" >> "$GITHUB_PATH"
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Both legs check, with no axioms
+        run: bash scripts/check-legs.sh

PROOF-STATUS.adoc

@@ -26,10 +26,13 @@ invocation, which this repository has met since waiver W-1 closed.
 |===
 | Claim | PWG | Why not higher
 
-| N-1, N-2, N-3, N-7, N-8, N-9 | `PWG-3` | The Agda proof is PROVEN under the §2.1
-  invocation (receipt below). No Rocq leg and no Lean leg exists, so no leg
-  counts (§8.2). No axioms: `--safe`, a postulate scan of the import cone, and the
-  recorded cone. `foundation-diverse`: no.
+| N-1, N-2, N-3, N-7, N-8, N-9 | *`PWG-2ii`* | PROVEN under the canonical
+  invocation `agda --safe --without-K --cubical-compatible`, with stronger flags
+  besides (`scripts/proof-flags.sh`), and both §2 legs count: re-proved in Rocq
+  and in Lean, kernel-checked with no axioms, `RECONCILED` (below). Not
+  `PWG-1`: that needs a per-commit receipt of each checker's observed result,
+  and the receipt records the gate, not its result. `foundation-diverse` is
+  false: Agda, Rocq and Lean are all dependent type theories (§8.3).
 
 | N-4, N-5, N-6 | `ungraded` | TESTED demonstrations (refusals, computed
   witnesses, a law-ablation certificate), not theorems; §8.1 grades theory
@@ -40,43 +43,51 @@ N-9 is a proved *refutation*: termination-sensitive noninterference is false for
 the current typing rules when finishing versus non-finishing is observable. A
 stronger typing discipline is OPEN, and so is declassification.
 
-A grade is not a discharge (§8.4.1): at `PWG-3` every theorem above still owes
-its Rocq and Lean legs (§2).
+No theorem rests on an axiom (§8.4, "axioms travel with the grade"). In Agda:
+`postulates = 0` and `escape-hatches = 0` in the receipt, under `--safe`. In
+Rocq, `Print Assumptions` reports `Closed under the global context` for every
+leg theorem; in Lean, `#print axioms` reports `does not depend on any axioms`.
 
-=== The two legs, recorded honestly
+=== The two legs
 
 `PROOF-POLICY.adoc` §2 requires every Agda theory proof to be rechecked in Rocq
 and in Lean, by transport through Dedukti first and by hand re-proof as the
-fallback, with the route named per theorem. Neither leg exists here, and the
-policy is explicit that a policy's adoption is not an execution: each row below
-would need its own CI receipt.
+fallback, with the route named per theorem. Both legs exist since 2026-11-09.
+Their §2.2 record (statements, universe discipline, versions, invocations,
+assumptions) is link:verification/legs/README.adoc[`verification/legs/README.adoc`];
+`bash scripts/check-legs.sh` checks them, and CI runs it as the `legs` job.
 
-[cols="1,1,1,3",options="header"]
+[cols="1,1,1,1,3",options="header"]
 |===
-| Claim | Rocq leg | Lean leg | Record
-
-| N-1, N-2, N-3, N-7, N-8, N-9 | `unavailable` (`OPEN`) | `unavailable` (`OPEN`)
-| No Agda→Dedukti transport and no hand re-proof has been attempted from this
-  repository yet. §2.2 state of each: `AGDA-VERIFIED`. Nothing was skipped
-  silently: this is the opening state, stated.
-
-| all rows | — | —
-| *A leg that does not exist cannot be evidenced by a file that happens to be
-  present.* `verification/proofs/coq/TypeSafety.v`,
+| Claim | Rocq leg | Lean leg | §2.2 state | Record
+
+| N-1, N-2, N-3, N-7, N-8, N-9 | `re-proved`, PROVEN | `re-proved`, PROVEN
+| `RECONCILED`
+| Transport is not available: Agda2Dedukti is an Agda backend pinned to a fork
+  of Agda and cannot run on 2.6.4.3, and there is no released Dedukti or
+  Lambdapi exporter to Lean 4. So each leg restates the Agda theorem and proves
+  it by hand: Coq 8.18.0 with the prelude only, Lean 4.24.0 with core only (no
+  Mathlib). The statement comparison was written by Claude Code and is
+  provisional until the owner reviews it (estate doctrine 4).
+
+| N-4, N-5, N-6 | n/a | n/a | n/a
+| Checked demonstrations, not theorems (§8.1).
+
+| all rows | — | — | —
+| *A file that happens to be present is not a leg.*
+  `verification/proofs/coq/TypeSafety.v`,
   `verification/proofs/lean4/ApiTypes.lean` and the other skeletons under
   `verification/proofs/` are RSR template boilerplate ("replace with your
   project's …"). They prove nothing, they are not the legs, and their
-  `MANIFEST` lines claiming `gated` are false — no workflow invokes
+  `MANIFEST` lines claiming `gated` are false: no workflow invokes
   `scripts/check-proofs.sh`. Recorded as finding F-4 in
   link:docs/reports/audit/consistency-audit-2026-11-01.adoc.
 |===
 
-When a leg is attempted, `PROOF-POLICY` §2.2 fixes the record: exact
-proposition, assumptions, universe discipline, source revision, compiler and
-library versions, invocation, observed result, and the bridge or statement
-correspondence — *transported* or *re-proved* — and the correspondence states
-AGDA-VERIFIED / COQ-CHECKED / LEAN-CHECKED / BRIDGE-PENDING before RECONCILED.
-Only a RECONCILED leg raises the grade.
+The receipt's `(legs)` block records each leg's pinned checker, invocation and
+axiom check, and the `sha256` of every leg source, so a change to a leg cannot
+leave the receipt intact. `scripts/grade-receipt.sh` also refuses a claim that
+counts a leg without a row in the correspondence record, and the reverse.
 
 === The §2.1 invocation, and how waiver W-1 closed
 

README.adoc

@@ -77,14 +77,18 @@ Echo fibre over its outputs does not separate secret inputs — the Echo
 reading of noninterference, and the first candidate connection
 Secret → Echo for `nextgen-typing/docs/TYPE-CONNECTIONS.adoc`.
 
-*Grade.* The proved theorems are at **`PWG-3`** (a Proof Witness Grade,
-`standards/3-practice/PROOF-POLICY.adoc` §8) and no higher: they type-check in
-Agda under the canonical §2.1 invocation, `--safe --without-K
---cubical-compatible`, plus four stricter flags (`scripts/proof-flags.sh`), with
-no axioms. The Rocq and Lean recheck legs that §2 requires do not exist yet, so
-no leg counts; they are recorded `unavailable`, not skipped silently, and a grade
-is not a discharge. Per-claim evidence is in
-link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger], the machine record is
+*Grade.* The proved claims are at Proof Witness Grade **`PWG-2ii`**
+(`PROOF-POLICY.adoc` §8) and no higher. They type-check in Agda under the
+canonical §2.1 invocation, `--cubical-compatible` included, with stronger flags
+besides (`scripts/proof-flags.sh`). Each is also re-proved by hand in Rocq
+(Coq 8.18.0, prelude only) and in Lean (4.24.0, core only, no Mathlib), with no
+axioms in either, and the statements are compared in
+link:verification/legs/README.adoc[`verification/legs/README.adoc`]. That
+comparison was written by Claude Code and is provisional until the owner reviews
+it. Not `PWG-1`: no per-commit receipt captures each checker's observed result
+yet. Not `+foundation-diverse`: no witness outside dependent type theory.
+Per-claim evidence is in link:docs/EXPLAINME.adoc#proof-ledger[the Proof Ledger],
+the machine record is
 link:verification/receipts/agda_praxis.deed[`verification/receipts/agda_praxis.deed`]
 (checked in CI), and link:docs/proof-debt.adoc[proof debt] is empty in all four
 dispositions. This paragraph states no grade the receipt does not support.

build/just/proofs.just

@@ -40,7 +40,7 @@ proof-check-coq:
 proof-scan-dangerous:
     @bash scripts/scan-dangerous.sh
 
-# Regenerate the Grade-3 verification receipt (mathesis §6; PROOF-STATUS
+# Regenerate the verification receipt (PROOF-POLICY §8 Proof Witness Grades; PROOF-STATUS
 # "Grade, and the independent-witness legs"). CI runs the --check form, so a
 # committed receipt that no longer matches the tree fails the gate.
 proof-receipt:

docs/EXPLAINME.adoc

@@ -100,13 +100,17 @@ only tested or still open. Tokens are the standard's closed vocabulary.
   the public result for finishing. This refutes the current rules, not every
   possible termination-sensitive typing discipline.
 
-| Independent recheck in Rocq and in Lean (PROOF-POLICY §2)
-| open
-| —
-| `PROOF-STATUS.adoc` "Proof Witness Grades, and the independent-witness legs",
-  `verification/receipts/agda_praxis.deed`
-| No transport has been attempted and no hand re-proof exists, so every proven
-  theorem above is `PWG-3` (PROOF-POLICY §8) and no higher. The template skeletons under
+| Independent recheck of N-1, N-2, N-3, N-7, N-8 and N-9 in Rocq and in Lean
+  (PROOF-POLICY §2)
+| proven
+| `bash scripts/check-legs.sh` (Coq 8.18.0 and Lean 4.24.0, each pinned; no
+  library; every theorem printed with its axioms, and there are none)
+| `verification/legs/rocq/SecretTypes.v`, `verification/legs/lean/`;
+  correspondence in `verification/legs/README.adoc`
+| Re-proved by hand, not transported: Agda2Dedukti cannot run on the pinned
+  Agda. The statement comparison was written by Claude Code and is provisional
+  until the owner reviews it. With it, every proven row above is at `PWG-2ii`
+  (PROOF-POLICY §8). The template skeletons under
   `verification/proofs/{coq,lean4}` are *not* these legs and prove nothing here.
 
 | Strengthened termination-sensitive typing discipline

docs/proof-debt.adoc

@@ -67,12 +67,14 @@ _None in the proof development._
 Two items are open *obligations* rather than proof debt, and are listed here so
 that they are not mistaken for either:
 
-* *Rocq and Lean legs.* `PROOF-POLICY.adoc` §2 asks for every Agda theory proof
-  to be rechecked in Rocq and in Lean. Neither leg exists; both are recorded
-  `unavailable` in the receipt and in
-  link:../PROOF-STATUS.adoc[`PROOF-STATUS.adoc`]. An absent recheck is not an
-  escape hatch in a proof — the proof has no hole — but it bounds every theorem
-  at `PWG-3` (§8), and that bound is recorded rather than glossed.
+* *Recheck legs (`PWG-2ii`, met 2026-11-09).* `PROOF-POLICY.adoc` §2 asks for
+  every Agda theory proof to be rechecked in Rocq and in Lean. Both legs now
+  exist, re-proved by hand without a library or an axiom
+  (link:../verification/legs/README.adoc[`verification/legs/README.adoc`]),
+  and the receipt records them. The obligation that remains is review: the
+  statement comparison was written by Claude Code and is provisional until the
+  owner reviews it. `PWG-1` (a per-commit receipt of each checker's observed
+  result) is not met.
 * *Termination-sensitive noninterference.*
   `Noninterference.OutcomeVisibility.termination-sensitive-fails` refutes TSNI
   for the current typing rules when finishing versus non-finishing is public.

scripts/check-legs.sh

@@ -0,0 +1,63 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
+#
+# check-legs.sh — the Rocq and Lean recheck legs (PROOF-POLICY §2).
+#
+# Checks verification/legs/rocq (Coq, prelude only) and verification/legs/lean
+# (Lean core only, no Mathlib, no `require`), then refuses any axiom:
+#   * every `Print Assumptions` line must read "Closed under the global context";
+#   * every `#print axioms` line must read "does not depend on any axioms".
+# A leg that does not check, or that rests on an axiom, fails this gate: a
+# witness with axioms would have to be recorded PROVEN-WITH-AXIOMS and the
+# receipt says it is not (PROOF-POLICY §8.4).
+#
+# Pins: COQ_VERSION and LEAN_VERSION below, fixed (no environment override);
+# scripts/grade-receipt.sh reads them from here into the receipt.
+set -euo pipefail
+cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.."
+export LC_ALL="${LC_ALL:-C.UTF-8}"
+
+COQ_VERSION=8.18.0
+LEAN_VERSION=4.24.0
+fail=0
+
+got="$(coqc --version | sed -n 's/^The Coq Proof Assistant, version \([0-9.]*\).*/\1/p')"
+[[ "$got" == "$COQ_VERSION" ]] || { echo "ERROR: expected Coq $COQ_VERSION, found '${got:-none}'" >&2; exit 2; }
+got="$(lean --version | sed -n 's/^Lean (version \([0-9.]*\),.*/\1/p')"
+[[ "$got" == "$LEAN_VERSION" ]] || { echo "ERROR: expected Lean $LEAN_VERSION, found '${got:-none}'" >&2; exit 2; }
+
+# The Lean leg may not depend on anything: no `require` in the lakefile.
+if grep -nE '^\s*\[\[require\]\]|^\s*require\b' verification/legs/lean/lakefile.toml; then
+  echo 'FAIL: the Lean leg declares a dependency (no Mathlib, no libraries)' >&2; fail=1
+fi
+# The Rocq leg may not load the standard library.
+if grep -nE '^\s*(From\s+\S+\s+)?Require\b' verification/legs/rocq/*.v; then
+  echo 'FAIL: the Rocq leg loads a library (prelude only)' >&2; fail=1
+fi
+# No escape hatches in either leg.
+if grep -nE '\b(sorry|admit|Admitted|Axiom|Parameter|axiom)\b' verification/legs/rocq/*.v verification/legs/lean/SecretTypes/*.lean; then
+  echo 'FAIL: an escape hatch in a leg' >&2; fail=1
+fi
+
+rocq_out="$(cd verification/legs/rocq && coqc -q SecretTypes.v 2>&1)" || { echo "$rocq_out" >&2; echo 'FAIL: the Rocq leg does not check' >&2; exit 1; }
+n_closed="$(grep -c '^Closed under the global context$' <<< "$rocq_out" || true)"
+n_print="$(grep -c '^Print Assumptions ' verification/legs/rocq/SecretTypes.v)"
+if [[ "$n_closed" != "$n_print" ]] || grep -vq '^Closed under the global context$' <<< "$rocq_out"; then
+  echo "$rocq_out" >&2; echo "FAIL: the Rocq leg rests on an axiom ($n_closed of $n_print closed)" >&2; fail=1
+else
+  echo "PASS: Rocq leg (Coq $COQ_VERSION), $n_print theorems closed under the global context"
+fi
+
+lean_out="$(cd verification/legs/lean && lake build >/dev/null && lake env lean Axioms.lean 2>&1)" \
+  || { echo "$lean_out" >&2; echo 'FAIL: the Lean leg does not check' >&2; exit 1; }
+n_free="$(grep -c 'does not depend on any axioms$' <<< "$lean_out" || true)"
+n_ax="$(grep -c '^#print axioms ' verification/legs/lean/Axioms.lean)"
+if [[ "$n_free" != "$n_ax" ]] || grep -vq 'does not depend on any axioms$' <<< "$lean_out"; then
+  echo "$lean_out" >&2; echo "FAIL: the Lean leg rests on an axiom ($n_free of $n_ax free)" >&2; fail=1
+else
+  echo "PASS: Lean leg (Lean $LEAN_VERSION, core only), $n_ax theorems depend on no axioms"
+fi
+
+(( fail == 0 )) || exit 1
+echo 'PASS: both recheck legs'