proofs(lean4): promote ET-2 to main — L1 conversion is decidable

.github/workflows/estate-rules.yml

@@ -30,5 +30,3 @@ jobs:
         run: bash scripts/check-root-shape.sh .
       - name: AsciiDoc by default (no .md under docs/)
         run: bash scripts/check-no-md-in-docs.sh .
-      - name: No zig references
-        run: bash scripts/check-no-vlang.sh .

.github/workflows/proofs.yml

@@ -49,7 +49,7 @@ jobs:
           if [ ! -x "$HOME/.elan/bin/elan" ]; then
             ELAN_VERSION=4.2.3
             ELAN_SHA256=df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2
-            curl -sSfL -o /tmp/elan.tar.gz \
+            curl -sSfL --proto '=https' --tlsv1.2 -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
@@ -58,7 +58,20 @@ jobs:
           echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 
       - name: Install pinned Lean toolchain
-        run: elan toolchain install "$(cat verification/proofs/lean4/lean-toolchain)"
+        run: |
+          set -euo pipefail
+          tc="$(cat verification/proofs/lean4/lean-toolchain)"
+          # `elan toolchain install` exits 1 with "is already installed" when the
+          # runner image already ships the pinned toolchain, which fails the gate
+          # for a reason that has nothing to do with the proofs. Install only when
+          # absent, so a genuine install failure still fails the gate.
+          # match on the first field so an annotated listing (e.g. "... (default)") still matches
+          if elan toolchain list | awk '{print $1}' | grep -qx "$tc"; then
+            echo "toolchain $tc already present"
+          else
+            elan toolchain install "$tc"
+          fi
+          elan toolchain list
 
       - name: Proof gate (compile + coverage + axiom audit)
         run: ./scripts/check-proofs.sh lean4

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -79,14 +79,23 @@ enforcement-workflow = ".github/workflows/estate-rules.yml"
 #
 # Enforcement: `scripts/check-no-md-in-docs.sh` (fails if any *.md under docs/).
 
-# === Banned: ziguage ===
-# V (vlang.io) is banned estate-wide. Replaced by `zig-unified-api-adapter`
+# === Banned: the V language ===
+# V (vlang.io) is banned estate-wide. Replaced by `v-unified-api-adapter`
 # (16 endpoints + transaction-based firewall gating). Do not introduce
-# zig code, scaffolders, or references. Note that Coq theorem files use
+# V code, scaffolders, or references. Note that Coq theorem files use
 # the same `.v` extension and are unaffected — the rule looks at content
 # patterns, not the extension.
 #
-# Enforcement: `scripts/check-no-vlang.sh`.
+# Enforcement: WITHDRAWN 2026-07-27 (owner ruling). `scripts/check-no-vlang.sh`
+# and its `estate-rules` step are deleted. A rename sweep had rewritten "V" ->
+# "zig" throughout the script body AND this block, so the check was banning Zig
+# -- directly contradicting the estate's Zig-first ABI/FFI directive -- and
+# failing CI on dead template residue (.gitignore's .zig-cache/, commented-out
+# Justfile examples). The `.v`-extension caveat above is the tell: V uses `.v`,
+# Zig uses `.zig`. The V ban itself stands as policy; it is currently
+# UNENFORCED here. Re-enforcing needs a correctly-written checker -- the old one
+# cannot be salvaged by renaming, since its content patterns were corrupted too.
+# Closes the question raised in issue #19.
 
 # === Justfile structure ===
 # The root Justfile is self-contained. The template's build/just/ section
@@ -118,7 +127,6 @@ enforcement-workflow = ".github/workflows/estate-rules.yml"
 # === Reference scripts ===
 # scripts/check-root-shape.sh      Root allowlist validator
 # scripts/check-no-md-in-docs.sh   AsciiDoc-by-default validator
-# scripts/check-no-vlang.sh        zig ban validator
 # scripts/validate-template.sh     Aggregate RSR compliance (workflows, SPDX, etc.)
 
 # === Reference memory entries (for AI agents) ===

.machine_readable/6a2/STATE.a2ml

@@ -43,7 +43,6 @@ milestones = [
 [blockers-and-issues]
 issues = [
   { id = 18, title = "descriptiles/6a2 migration (blocked: contractiles.mjs needs Node, estate-denied here)" },
-  { id = 19, title = "wire check-no-vlang.sh into lint after clearing template zig residue (owner: confirm the script's premise vs Zig-first directive)" },
 ]
 # Downstream tracking: anytype issues #13-#19 (ET-obligation audit, 2026-07-21) +
 # anytype PR #20 echoing them; anytype #13 = refresh its systemet pin past the ET ledger.

docs/status/PROOF-STATUS.adoc

@@ -12,15 +12,15 @@ 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
+// gate:lean4 gated=15 quarantined=0
 
 == Summary
 
 [cols="3,1,1,1,1", options="header"]
 |===
 | Track | Total | Done | In progress | Open
 
-| ET obligations (DOM — the theory itself) | 15 | 1 | 3 | 11
+| ET obligations (DOM — the theory itself) | 15 | 2 | 2 | 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 | — | —
 |===
@@ -46,11 +46,15 @@ every theorem depends on nothing outside Lean's three-axiom trusted base
   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-2 (equality is conversion; decidability)
+| `Systemet.L1.nf_emb` (stability), `nf_substTy` (normalization commutes
+  with substitution — the beta case), `soundness : DefEq t (embNf (nf t))`,
+  `completeness : DefEq t u → nf t = nf u`,
+  `defEq_iff_nf : DefEq t u ↔ nf t = nf u`, `decEqNf` / `decEqSp`
+  (hand-rolled mutual decidable equality on normal forms), and
+  `decDefEq : (t u : Ty Γ k) → Decidable (DefEq t u)`
+| *Proven* for the L1 core calculus — `DefEq` here is β + equivalence +
+  congruence; η is **not** included (tracked as an OPEN row below)
 
 | ET-4 (grade algebras: the law set)
 | `Systemet.L2.GradeAlgebra` — ordered-semiring law set (16 laws) as a
@@ -73,12 +77,12 @@ every theorem depends on nothing outside Lean's three-axiom trusted base
 | Slot | Headline artefact | Covers | File target
 
 | MECH-1
-| `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
+| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment) —
+  *landed*. Totality core, stability, the substitution-commutation family
+  (`SubstLemmas.lean`), soundness, completeness, and decidable `Nf`
+  equality all compile and pass the axiom audit. Remaining for this slot:
+  the η extension and the model direction of ET-3.
+| ET-1 ✓, ET-2 ✓ (β-fragment), syntactic core of ET-3
 | `verification/proofs/lean4/Systemet/L1/`
 
 | MECH-2
@@ -95,7 +99,6 @@ every theorem depends on nothing outside Lean's three-axiom trusted base
 | 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

verification/proofs/lean4/MANIFEST

@@ -12,3 +12,7 @@ verification/proofs/lean4|Systemet/L2/Instances/Tropical.lean|gated|MECH-2: Cost
 verification/proofs/lean4|Systemet/L2/Instances/Lattice.lean|gated|MECH-2: bounded distributive lattice => grade algebra; Level
 verification/proofs/lean4|Systemet/L2/Instances/Product.lean|gated|MECH-2: componentwise product algebra (ET-5)
 verification/proofs/lean4|Systemet/Audit.lean|gated|axiom audit (#print axioms per headline)
+verification/proofs/lean4|Systemet/L1/SubstLemmas.lean|gated|MECH-1: ET-2 commutation toolkit (exchange laws, nf_substTy)
+verification/proofs/lean4|Systemet/L1/Soundness.lean|gated|MECH-1: ET-2 soundness (DefEq t (embNf (nf t)))
+verification/proofs/lean4|Systemet/L1/Completeness.lean|gated|MECH-1: ET-2 completeness + defEq_iff_nf
+verification/proofs/lean4|Systemet/L1/Decidable.lean|gated|MECH-1: ET-2 decEqNf/decDefEq (decidability of conversion)

verification/proofs/lean4/Systemet.lean

@@ -7,3 +7,7 @@ import Systemet.L2.Instances.Affine
 import Systemet.L2.Instances.Tropical
 import Systemet.L2.Instances.Lattice
 import Systemet.L2.Instances.Product
+import Systemet.L1.SubstLemmas
+import Systemet.L1.Soundness
+import Systemet.L1.Completeness
+import Systemet.L1.Decidable

verification/proofs/lean4/Systemet/Audit.lean

@@ -7,7 +7,7 @@ import Systemet
 `scripts/check-proofs.sh lean4` runs this file and requires one
 "does not depend on any axioms" line per `#print axioms` command below
 (and no `sorryAx` anywhere in the output). A theorem that elaborates but
-smuggles in an axiom or a `sorry` through an import fails the gate here,
+smuggles in a user axiom or a `sorryAx` through an import fails the gate here,
 not in a status document. Update the PROOF-STATUS ledger when adding lines.
 -/
 
@@ -26,3 +26,13 @@ not in a status document. Update the PROOF-STATUS ledger when adding lines.
 #print axioms Systemet.L2.BoundedDistLattice.grade
 #print axioms Systemet.L2.Level.lattice
 #print axioms Systemet.L2.prodGrade
+
+-- MECH-1 (L1) milestone 2: ET-2 — conversion is decidable
+#print axioms Systemet.L1.nf_substTy
+#print axioms Systemet.L1.substNf_substNf
+#print axioms Systemet.L1.defEq_substTy_embNf
+#print axioms Systemet.L1.soundness
+#print axioms Systemet.L1.completeness
+#print axioms Systemet.L1.defEq_iff_nf
+#print axioms Systemet.L1.decEqNf
+#print axioms Systemet.L1.decDefEq

verification/proofs/lean4/Systemet/L1/Completeness.lean

@@ -0,0 +1,45 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.Soundness
+/-!
+# L1 completeness and `defEq_iff_nf` (ET-2)
+
+Completeness — convertible terms have equal normal forms — by induction on
+the conversion derivation; the β-case is exactly the commutation equation
+`nf_substTy`. Together with soundness this gives the ET-2 headline
+`defEq_iff_nf : DefEq t u ↔ nf t = nf u`.
+-/
+
+namespace Systemet.L1
+
+/-- **Completeness**: `nf` respects conversion. -/
+theorem completeness : {Γ : Ctx} → {k : Kind} → {t u : Ty Γ k} →
+    DefEq t u → nf t = nf u := by
+  intro Γ k t u h
+  induction h with
+  | refl => rfl
+  | symm _ ih => exact ih.symm
+  | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂
+  | beta b u =>
+    show nf (.app (.lam b) u) = nf (subst0 b u)
+    simp only [nf, napp]
+    exact (nf_substTy b .vz u).symm
+  | arrowCong _ _ ih₁ ih₂ =>
+    simp only [nf]
+    rw [ih₁, ih₂]
+  | lamCong _ ih =>
+    simp only [nf]
+    rw [ih]
+  | appCong _ _ ih₁ ih₂ =>
+    simp only [nf]
+    rw [ih₁, ih₂]
+
+/-- **ET-2, headline**: conversion is normalize-then-compare. -/
+theorem defEq_iff_nf {Γ : Ctx} {k : Kind} {t u : Ty Γ k} :
+    DefEq t u ↔ nf t = nf u :=
+  ⟨completeness, fun h =>
+    (soundness t).trans (by
+      rw [congrArg embNf h]
+      exact (soundness u).symm)⟩
+
+end Systemet.L1