hyperpolymath · hyperpolymath · Jul 22, 2026 · Jul 22, 2026
@@ -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

@@ -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)
@@ -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
@@ -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
@@ -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
@@ -0,0 +1,88 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.Completeness
+/-!
+# L1 decidability of conversion (ET-2)
+
+Hand-rolled decidable equality for the mutual pair `Nf`/`Sp` — `deriving
+DecidableEq` cannot handle the mutual inductives, and `.ne`/`.cons` hide a
+head/argument kind that must be compared first (with `Kind`'s decidable
+equality) before the pieces can be compared componentwise. With
+`defEq_iff_nf` this closes ET-2: `decDefEq` decides conversion by
+normalize-then-compare.
+-/
+
+namespace Systemet.L1
+
+mutual
+  /-- Decidable equality on normal forms. -/
+  def decEqNf : {Γ : Ctx} → {k : Kind} → (m n : Nf Γ k) → Decidable (m = n)
+    | _, _, .lam b₁, .lam b₂ =>
+      match decEqNf b₁ b₂ with
+      | .isTrue h => .isTrue (by rw [h])
+      | .isFalse h => .isFalse fun e => h (by injection e)
+    | _, _, .lam _, .ne _ _ => .isFalse fun e => by injection e
+    | _, _, .ne _ _, .lam _ => .isFalse fun e => by injection e
+    | _, _, .base n₁, .base n₂ =>
+      match Nat.decEq n₁ n₂ with
+      | .isTrue h => .isTrue (by rw [h])
+      | .isFalse h => .isFalse fun e => h (by injection e)
+    | _, _, .base _, .arrow _ _ => .isFalse fun e => by injection e
+    | _, _, .base _, .ne _ _ => .isFalse fun e => by injection e
+    | _, _, .arrow _ _, .base _ => .isFalse fun e => by injection e
+    | _, _, .arrow a₁ b₁, .arrow a₂ b₂ =>
+      match decEqNf a₁ a₂ with
+      | .isFalse h₁ => .isFalse fun e => h₁ (by injection e)
+      | .isTrue h₁ =>
+        match decEqNf b₁ b₂ with
+        | .isTrue h₂ => .isTrue (by rw [h₁, h₂])
+        | .isFalse h₂ => .isFalse fun e => h₂ (by injection e)
+    | _, _, .arrow _ _, .ne _ _ => .isFalse fun e => by injection e
+    | _, _, .ne _ _, .base _ => .isFalse fun e => by injection e
+    | _, _, .ne _ _, .arrow _ _ => .isFalse fun e => by injection e
+    | _, _, .ne (k := c₁) y₁ sp₁, .ne (k := c₂) y₂ sp₂ =>
+      if hc : c₁ = c₂ then by
+        subst hc
+        exact
+          if hy : y₁ = y₂ then
+            match decEqSp sp₁ sp₂ with
+            | .isTrue hs => .isTrue (by rw [hy, hs])
+            | .isFalse hs => .isFalse fun e => hs (by injection e)
+          else .isFalse fun e => hy (by injection e)
+      else .isFalse fun e => hc (by injection e)
+  termination_by _ _ m _ => nfSize m
+  decreasing_by all_goals (simp only [nfSize]; omega)
+
+  /-- Decidable equality on spines. -/
+  def decEqSp : {Γ : Ctx} → {a j : Kind} → (s t : Sp Γ a j) → Decidable (s = t)
+    | _, _, _, .nil, .nil => .isTrue rfl
+    | _, _, _, .nil, .cons _ _ => .isFalse fun e => by injection e
+    | _, _, _, .cons _ _, .nil => .isFalse fun e => by injection e
+    | _, _, _, .cons (b := b₁) sp₁ v₁, .cons (b := b₂) sp₂ v₂ =>
+      if hb : b₁ = b₂ then by
+        subst hb
+        exact
+          match decEqSp sp₁ sp₂ with
+          | .isFalse h₁ => .isFalse fun e => h₁ (by injection e)
+          | .isTrue h₁ =>
+            match decEqNf v₁ v₂ with
+            | .isTrue h₂ => .isTrue (by rw [h₁, h₂])
+            | .isFalse h₂ => .isFalse fun e => h₂ (by injection e)
+      else .isFalse fun e => hb (by injection e)
+  termination_by _ _ _ s _ => spSize s
+  decreasing_by all_goals (simp only [spSize]; omega)
+end
+
+instance : DecidableEq (Nf Γ k) := decEqNf
+
+instance : DecidableEq (Sp Γ a j) := decEqSp
+
+/-- **ET-2, closure**: conversion is decidable — normalize and compare. -/
+def decDefEq (t u : Ty Γ k) : Decidable (DefEq t u) :=
+  match decEqNf (nf t) (nf u) with
+  | .isTrue h => .isTrue (defEq_iff_nf.mpr h)
+  | .isFalse h => .isFalse fun d => h (defEq_iff_nf.mp d)
+
+instance : Decidable (DefEq t u) := decDefEq t u
+
+end Systemet.L1
@@ -0,0 +1,133 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+import Systemet.L1.SubstLemmas
+/-!
+# L1 soundness: `DefEq t (embNf (nf t))` (ET-2, milestone 2 of MECH-1)
+
+The substitution-commutation family at the `DefEq` level — the lemma named
+in Conversion.lean's docstring,
+`DefEq (substTy (embNf t) x (embNf u)) (embNf (substNf t x u))` — proved by
+the same `(kindSize, tag, size)` lexicographic induction as `substNf`
+itself. `DefEq`'s β-rule absorbs all the β-work `appSp` performs, so this
+direction needs no equational commutation of substitutions. Soundness of
+the normalizer follows by structural induction.
+-/
+
+namespace Systemet.L1
+
+mutual
+  /-- Substitution commutes with embedding, up to conversion: the
+      Keller–Altenkirch commutation lemma at the `DefEq` level. -/
+  theorem defEq_substTy_embNf : {Γ : Ctx} → {j k : Kind} → (t : Nf Γ j) →
+      (x : Var Γ k) → (u : Nf (rem x) k) →
+      DefEq (substTy (embNf t) x (embNf u)) (embNf (substNf t x u))
+    | _, _, _, .lam (k₁ := k₁) b, x, u => by
+      have ih := defEq_substTy_embNf b (Var.vs (k' := k₁) x) (wkNf .vz u)
+      rw [embNf_wkNf] at ih
+      simp only [embNf, substNf, substTy]
+      exact ih.lamCong
+    | _, _, _, .base n, _, _ => by
+      simp only [embNf, substNf, substTy]
+      exact .refl
+    | _, _, _, .arrow a b, x, u => by
+      simp only [embNf, substNf, substTy]
+      exact (defEq_substTy_embNf a x u).arrowCong (defEq_substTy_embNf b x u)
+    | _, _, _, .ne (k := c) z sp, x, u =>
+      match c, z, sp, eqv x z with
+      | _, _, sp, .same => by
+        simp only [embNf, substNf_ne_self]
+        exact (defEq_substTy_embSp sp x u (.var x) (embNf u)
+          (by simp only [substTy, eqv_refl]; exact .refl)).trans
+          (defEq_embSp_appSp u (substSp sp x u))
+      | _, _, sp, .diff _ z' => by
+        simp only [embNf, substNf_ne_wkv]
+        exact defEq_substTy_embSp sp x u (.var (wkv x z')) (.var z')
+          (by simp only [substTy, eqv_wkv]; exact .refl)
+  termination_by _ _ k t _ _ => (kindSize k, 1, nfSize t)
+  decreasing_by
+    all_goals simp only [nfSize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+      | (apply Prod.Lex.right; apply Prod.Lex.left; omega)
+
+  /-- Spine form of `defEq_substTy_embNf`, threading a converted head. -/
+  theorem defEq_substTy_embSp : {Γ : Ctx} → {a j k : Kind} → (sp : Sp Γ a j) →
+      (x : Var Γ k) → (u : Nf (rem x) k) → (h : Ty Γ a) → (h' : Ty (rem x) a) →
+      DefEq (substTy h x (embNf u)) h' →
+      DefEq (substTy (embSp h sp) x (embNf u)) (embSp h' (substSp sp x u))
+    | _, _, _, _, .nil, _, _, _, _, hh => by
+      simp only [embSp, substSp]
+      exact hh
+    | _, _, _, _, .cons sp v, x, u, h, h', hh => by
+      simp only [embSp, substSp, substTy]
+      exact (defEq_substTy_embSp sp x u h h' hh).appCong
+        (defEq_substTy_embNf v x u)
+  termination_by _ _ _ k sp _ _ _ _ _ => (kindSize k, 1, spSize sp)
+  decreasing_by
+    all_goals simp only [spSize]
+    all_goals (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+
+  /-- Folding a normal form through a spine, embedded: `appSp` is
+      conversion-compatible. -/
+  theorem defEq_embSp_appSp : {Γ : Ctx} → {a j : Kind} → (F : Nf Γ a) →
+      (SP : Sp Γ a j) → DefEq (embSp (embNf F) SP) (embNf (appSp F SP))
+    | _, _, _, F, .nil => by
+      simp only [embSp, appSp]
+      exact .refl
+    | _, _, _, F, .cons SP v => by
+      rw [appSp_cons]
+      have s1 := (defEq_embSp_appSp F SP).appCong (DefEq.refl (t := embNf v))
+      cases hG : appSp F SP with
+      | lam T =>
+        rw [hG] at s1
+        simp only [embSp, embNf, napp] at s1 ⊢
+        exact s1.trans ((DefEq.beta (embNf T) (embNf v)).trans
+          (defEq_substTy_embNf T .vz v))
+      | ne y sp' =>
+        rw [hG] at s1
+        simp only [embSp, embNf, napp] at s1 ⊢
+        exact s1
+  termination_by _ a _ _ SP => (kindSize a, 0, spSize SP)
+  decreasing_by
+    all_goals simp only [spSize]
+    all_goals first
+      | (apply Prod.Lex.right; apply Prod.Lex.right; omega)
+      | (apply Prod.Lex.left
+         have h := spKindLe SP
+         simp only [kindSize] at h ⊢
+         omega)
+end
+
+/-- One-step β-application, embedded: `napp` is conversion-compatible. -/
+theorem defEq_embNf_napp : {Γ : Ctx} → {a b : Kind} → (F : Nf Γ (.arr a b)) →
+    (A : Nf Γ a) → DefEq (.app (embNf F) (embNf A)) (embNf (napp F A))
+  | _, _, _, .lam T, A => by
+    simp only [embNf, napp]
+    exact (DefEq.beta (embNf T) (embNf A)).trans (defEq_substTy_embNf T .vz A)
+  | _, _, _, .ne y sp, A => by
+    simp only [embNf, napp, embSp]
+    exact .refl
+
+/-- **Soundness**: every type-level term converts to its normal form.
+    With stability (`nf_emb`) this makes `nf` a normalizer for `DefEq`. -/
+theorem soundness : {Γ : Ctx} → {k : Kind} → (t : Ty Γ k) → DefEq t (embNf (nf t))
+  | _, _, .var x => by
+    simp only [nf, embNf, embSp]
+    exact .refl
+  | _, _, .base n => by
+    simp only [nf, embNf]
+    exact .refl
+  | _, _, .arrow a b => by
+    simp only [nf, embNf]
+    exact (soundness a).arrowCong (soundness b)
+  | _, _, .lam b => by
+    simp only [nf, embNf]
+    exact (soundness b).lamCong
+  | _, _, .app f a => by
+    simp only [nf]
+    exact ((soundness f).appCong (soundness a)).trans
+      (defEq_embNf_napp (nf f) (nf a))
+termination_by _ _ t => tySize t
+decreasing_by all_goals (simp only [tySize]; first | exact Nat.lt_succ_self _ | omega)
+
+end Systemet.L1