proofs(lean4): mechanize the L1/L2 core (MECH-1 totality+stability, MECH-2 complete) with hard gates

.github/workflows/proofs.yml

@@ -0,0 +1,70 @@
+# SPDX-License-Identifier: MPL-2.0
+# Proof gate: the same scripts/check-proofs.sh a developer runs locally.
+# Hermetic by construction — elan comes from a version-pinned release tarball
+# with a checksum, the Lean toolchain from the committed lean-toolchain file,
+# and no floating setup action is involved. A missing prover FAILS (the gate
+# never skips), so this workflow existing is what makes green mean "proved".
+name: proofs
+
+on:
+  push:
+    branches: [main]
+    paths:
+      - "verification/proofs/**"
+      - "scripts/check-proofs.sh"
+      - "scripts/check-proof-status.sh"
+      - "scripts/scan-dangerous.sh"
+      - "docs/status/PROOF-STATUS.adoc"
+      - ".github/workflows/proofs.yml"
+  pull_request:
+    paths:
+      - "verification/proofs/**"
+      - "scripts/check-proofs.sh"
+      - "scripts/check-proof-status.sh"
+      - "scripts/scan-dangerous.sh"
+      - "docs/status/PROOF-STATUS.adoc"
+      - ".github/workflows/proofs.yml"
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+jobs:
+  lean4:
+    name: lean4 proof gate
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0
+
+      - name: Cache elan + toolchain (keyed on lean-toolchain pin)
+        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v4
+        with:
+          path: ~/.elan
+          key: elan-4.2.3-${{ runner.os }}-${{ hashFiles('verification/proofs/lean4/lean-toolchain') }}
+
+      - name: Install elan (pinned tarball, checksum-verified)
+        run: |
+          set -euo pipefail
+          if [ ! -x "$HOME/.elan/bin/elan" ]; then
+            ELAN_VERSION=4.2.3
+            ELAN_SHA256=df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2
+            curl -sSfL -o /tmp/elan.tar.gz \
+              "https://github.com/leanprover/elan/releases/download/v${ELAN_VERSION}/elan-x86_64-unknown-linux-gnu.tar.gz"
+            echo "${ELAN_SHA256}  /tmp/elan.tar.gz" | sha256sum -c -
+            tar -xzf /tmp/elan.tar.gz -C /tmp
+            /tmp/elan-init -y --default-toolchain none
+          fi
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Install pinned Lean toolchain
+        run: elan toolchain install "$(cat verification/proofs/lean4/lean-toolchain)"
+
+      - name: Proof gate (compile + coverage + axiom audit)
+        run: ./scripts/check-proofs.sh lean4
+
+      - name: Dangerous-construct scan
+        run: ./scripts/scan-dangerous.sh
+
+      - name: Status drift gate (PROOF-STATUS must match MANIFEST)
+        run: ./scripts/check-proof-status.sh

.gitignore

@@ -132,3 +132,6 @@ dist/
 
 # Coaptation re-anchor basis (occasional, generated on --reanchor when red; not a baseline)
 .machine_readable/coaptation/receipts/reanchor-basis.a2ml
+
+# Lean 4 / lake build artifacts (proofs are rebuilt by the gate, never committed)
+verification/proofs/lean4/.lake/

Justfile

@@ -544,6 +544,14 @@ help-me:
     @echo ""
     @echo "Include the output of 'just doctor' in your report."
 
+# ═══════════════════════════════════════════════════════════════════════════════
+# FORMAL VERIFICATION (PROOFS) — see build/just/proofs.just
+# proof-check-* delegate to scripts/check-proofs.sh: prover absent = FAIL,
+# MANIFEST-driven, coverage-enforced. Never reintroduce a skip-on-missing gate.
+# ═══════════════════════════════════════════════════════════════════════════════
+
+import? "build/just/proofs.just"
+
 # ═══════════════════════════════════════════════════════════════════════════════
 # SESSION MANAGEMENT (THIN BINDINGS TO CENTRAL STANDARDS)
 # ═══════════════════════════════════════════════════════════════════════════════

build/just/proofs.just

@@ -0,0 +1,61 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# FORMAL VERIFICATION (PROOFS)
+#
+# Imported by ../../Justfile via `import? "build/just/proofs.just"`.
+# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus
+# scan for dangerous/unsafe constructs and report status. Run via
+# `just proof-check-all` for the full sweep.
+
+# Check all formal proofs (Idris2 + Lean4 + Agda + Coq)
+proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous
+    @echo "=== All proof checks complete ==="
+
+# Each proof-check-<prover> delegates to scripts/check-proofs.sh, the single
+# source of truth. A missing toolchain is FATAL (never a skip); every module is
+# checked from its own source root; a proof file absent from the prover's
+# manifest (verification/proofs/<prover>/MANIFEST) is an error. See the script
+# header for the four "checks that could not fail" this replaces.
+
+# Check Idris2 proofs (per MANIFEST; fatal if idris2 absent)
+proof-check-idris2:
+    @bash scripts/check-proofs.sh idris2
+
+# Check Lean4 proofs (per MANIFEST; fatal if lean absent)
+proof-check-lean4:
+    @bash scripts/check-proofs.sh lean4
+
+# Check Agda proofs (per MANIFEST; fatal if agda absent)
+proof-check-agda:
+    @bash scripts/check-proofs.sh agda
+
+# Check Coq proofs (per MANIFEST; fatal if coqc absent)
+proof-check-coq:
+    @bash scripts/check-proofs.sh coq
+
+# Scan for dangerous constructs USED in proof code (believe_me, sorry, Admitted,
+# postulate, ...). Comments are ignored — a comment naming a banned construct
+# must not trip the gate. See scripts/scan-dangerous.sh.
+proof-scan-dangerous:
+    @bash scripts/scan-dangerous.sh
+
+# Show proof status summary
+proof-status:
+    #!/usr/bin/env bash
+    echo "=== Proof Status ==="
+    echo ""
+    echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files"
+    echo "Lean4:  $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files"
+    echo "Agda:   $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files"
+    echo "Coq:    $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files"
+    echo "TLA+:   $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files"
+    echo ""
+    # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23)
+    for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do
+        if [ -f "$candidate" ]; then
+            grep -E "^\| \*\*Total\*\*|^\| \*Total\*" "$candidate" 2>/dev/null || echo "(No summary row in $candidate)"
+            exit 0
+        fi
+    done
+    echo "(No PROOF-STATUS file found at root or docs/status/)"

docs/status/PROOF-STATUS.adoc

@@ -7,23 +7,64 @@
 The obligation *statements* live in `docs/theory/OBLIGATIONS.adoc` (the ET
 ledger); this file tracks *evidence*. A row is "Done" only when a prover
 actually ran (locally and in CI via `scripts/check-proofs.sh`) and the axiom
-audit is clean. The mechanization PR adds a CI drift gate that recomputes
-the summary from the per-prover MANIFESTs and fails if this table disagrees.
+audit is clean. `scripts/check-proof-status.sh` (run by CI) recomputes the
+summary from the per-prover MANIFESTs and fails if this file disagrees.
+
+// Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh.
+// Do not edit by hand without changing the MANIFEST accordingly.
+// gate:lean4 gated=11 quarantined=0
 
 == Summary
 
 [cols="3,1,1,1,1", options="header"]
 |===
 | Track | Total | Done | In progress | Open
 
-| ET obligations (DOM — the theory itself) | 15 | 0 | 0 | 15
-| MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | 0 | staged | —
-| MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 0 | staged | —
+| ET obligations (DOM — the theory itself) | 15 | 1 | 3 | 11
+| MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | —
+| MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | —
 |===
 
-*Overall: 0% proven.* No completed systemet proof exists at this date. The
-generic template stubs previously counted here (5 ABI + 2 TP) were template
-properties, not systemet obligations; they were removed with the ABI seam.
+The Done/In-progress claims above are scoped to the *mechanized core
+calculus* (type-level STLC with base constants and the object arrow;
+grade algebras as ordered semirings). They are evidence toward the ET
+obligations, not proofs of the full-theory statements.
+
+== Current evidence (verified by `./scripts/check-proofs.sh lean4`)
+
+All items below compile under Lean 4.32.0 (hermetic, zero dependencies, no
+mathlib), pass the MANIFEST coverage check, and pass the axiom audit —
+every theorem depends on nothing outside Lean's three-axiom trusted base
+(`propext`, `Classical.choice`, `Quot.sound`); no `sorryAx`, no user axioms.
+
+[cols="1,3,2", options="header"]
+|===
+| Covers | Artefact (Lean identifier) | Status
+
+| ET-1 (Totality Gate, L1 calculus)
+| `Systemet.L1.substNf` / `appSp` / `nf` — hereditary substitution and the
+  normalizer, total by a `(kindSize, tag, size)` lexicographic measure
+| *Proven* (totality is by construction; the measure is the proof)
+
+| ET-2 (equality is conversion) — partial
+| `Systemet.L1.DefEq` (β + equivalence + congruence) stated;
+  `Systemet.L1.nf_emb : nf (embNf n) = n` — normal forms are fixed points
+  of the normalizer (stability)
+| *Stability proven*; soundness/completeness OPEN (below)
+
+| ET-4 (grade algebras: the law set)
+| `Systemet.L2.GradeAlgebra` — ordered-semiring law set (16 laws) as a
+  class whose fields *are* the proof obligations
+| *Proven* for every instance below
+
+| ET-5 (same rules, different algebra)
+| `Systemet.L2.Affine.grade` ({0,1,ω}), `Systemet.L2.Cost.grade`
+  (tropical min/+), `Systemet.L2.BoundedDistLattice.grade` (generic
+  theorem: every bounded distributive lattice is a grade algebra,
+  instantiated at `Level` = Low≤High), `Systemet.L2.prodGrade` (R×S
+  componentwise — composite disciplines are composition of algebras)
+| *Proven* (4 algebras + 1 generic construction)
+|===
 
 == Mechanization slots
 
@@ -32,15 +73,18 @@ properties, not systemet obligations; they were removed with the ABI seam.
 | Slot | Headline artefact | Covers | File target
 
 | MECH-1
-| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment;
-  normalizer total by construction)
-| ET-1, ET-2, syntactic core of ET-3
+| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment).
+  Landed so far: totality core + stability. Remaining: soundness
+  (`DefEq t (embNf (nf t))`), completeness (`DefEq t u → nf t = nf u`),
+  decidable equality of `Nf` — all rest on the substitution-commutation
+  lemma; statements recorded in `Systemet/L1/Conversion.lean`.
+| ET-1 ✓, ET-2 (partial), syntactic core of ET-3
 | `verification/proofs/lean4/Systemet/L1/`
 
 | MECH-2
 | `GradeAlgebra` class (the ET-4 law set) + instances Affine, Tropical
-  (Cost), Lattice (generic + Low≤High), Product (R×S)
-| ET-4, ET-5
+  (Cost), Lattice (generic + Low≤High), Product (R×S) — *complete*.
+| ET-4 ✓, ET-5 ✓ (for the mechanized law set)
 | `verification/proofs/lean4/Systemet/L2/`
 |===
 
@@ -51,6 +95,7 @@ properties, not systemet obligations; they were removed with the ABI seam.
 | ID | Target
 
 | ET-14 | *TEA erasure — the headline open problem. Never cite as proven.*
+| ET-2 (finish) | soundness + completeness + `defEq_iff_nf` + `decDefEq` (MECH-1 milestone 2)
 | ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1
 | ET-1..3 (NAT) | type-level ℕ + recursor via NbE (stretch; research-adjacent)
 | ET-6, ET-7 | Structural Gate soundness + refusal characterization
@@ -61,19 +106,18 @@ properties, not systemet obligations; they were removed with the ABI seam.
 
 == Verification commands
 
-Available after the mechanization PR lands:
-
 [source,bash]
 ----
-just proof-check-all        # every prover with a MANIFEST; absent prover = FAIL
-just proof-check-lean4
-just proof-scan-dangerous   # comment-aware banned-construct scan
+just proof-check-all          # every prover with a MANIFEST; absent prover = FAIL
+just proof-check-lean4        # compile + coverage + lake build + axiom audit
+just proof-scan-dangerous     # comment-aware banned-construct scan
 ./scripts/check-proofs.sh lean4
+./scripts/check-proof-status.sh   # this file vs MANIFEST ground truth
 ----
 
-Until then there is deliberately *no* proof-check recipe: a recipe that
-green-exits with no prover is the estate's known fake-gate pattern and is
-not reproduced here.
+The gate has been *watched to fail* on all four failure modes (broken
+proof; smuggled `axiom` that compiles green; absent prover; proof file on
+disk but missing from the MANIFEST) before its green was trusted.
 
 == Escape-hatch registry echo (ET-15)
 

scripts/check-proof-status.sh

@@ -0,0 +1,60 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# check-proof-status.sh — the status-drift gate.
+#
+# docs/status/PROOF-STATUS.adoc claims numbers; the per-prover MANIFESTs are
+# the ground truth check-proofs.sh actually enforces. This script recomputes
+# the counts from every MANIFEST and fails if the document disagrees, so the
+# status file cannot drift into fiction (the estate's recurring failure mode:
+# status docs saying "proved" while nothing was checked).
+#
+# Contract: for each verification/proofs/<prover>/MANIFEST the document must
+# contain the exact line
+#
+#   // gate:<prover> gated=<N> quarantined=<M>
+#
+# and must not contain such a line for a prover with no MANIFEST.
+
+set -euo pipefail
+cd "$(dirname "${BASH_SOURCE[0]}")/.."
+DOC="docs/status/PROOF-STATUS.adoc"
+[ -f "$DOC" ] || { echo "FAIL: $DOC missing" >&2; exit 1; }
+
+fails=0
+found_any=0
+
+for mf in verification/proofs/*/MANIFEST; do
+  [ -f "$mf" ] || continue
+  found_any=1
+  prover="$(basename "$(dirname "$mf")")"
+  gated="$(awk -F'|' '$0 !~ /^[[:space:]]*(#|$)/ && $3 == "gated"' "$mf" | wc -l)"
+  quar="$(awk -F'|' '$0 !~ /^[[:space:]]*(#|$)/ && $3 == "quarantine"' "$mf" | wc -l)"
+  want="// gate:$prover gated=$gated quarantined=$quar"
+  if grep -qxF "$want" "$DOC"; then
+    echo "OK: $prover — $gated gated, $quar quarantined (document agrees)"
+  else
+    echo "FAIL: $DOC does not contain the line:"
+    echo "        $want"
+    echo "      ($mf ground truth: $gated gated, $quar quarantined)"
+    fails=$((fails + 1))
+  fi
+done
+
+# A marker for a prover with no MANIFEST is a stale claim.
+while IFS= read -r line; do
+  p="$(sed -E 's|^// gate:([A-Za-z0-9_-]+) .*|\1|' <<<"$line")"
+  if [ ! -f "verification/proofs/$p/MANIFEST" ]; then
+    echo "FAIL: stale marker in $DOC for prover '$p' (no MANIFEST on disk)"
+    fails=$((fails + 1))
+  fi
+done < <(grep -E '^// gate:' "$DOC" || true)
+
+[ "$found_any" -eq 1 ] || echo "note: no MANIFESTs found — only staleness was checked"
+
+if [ "$fails" -gt 0 ]; then
+  echo "RESULT: FAIL ($fails drift(s) between PROOF-STATUS.adoc and MANIFEST ground truth)"
+  exit 1
+fi
+echo "RESULT: PASS — PROOF-STATUS.adoc matches MANIFEST ground truth"