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

Promotes the **ET-2 closure** (decidability of L1 conversion) onto
`main`.

## Why this PR exists

ET-2 was proven and merged in **PR #24** — but into
`proofs/lean4-l1-l2`, **not `main`**. PR #17 had squash-merged that
branch to `main` *before* ET-2 existed, so `main` holds the L1/L2
mechanization content while the ET-2 work sits only on the branch. No
second PR to `main` was ever opened.

Measured before this PR: `main...proofs/lean4-l1-l2` was **diverged, 4
ahead / 14 behind**, and all four ET-2 proof files returned **404 on
`main`**. Anything reading `main` today correctly concludes ET-2 is
still open.

## What lands on `main`

| File | Contents |
|---|---|
| `Systemet/L1/SubstLemmas.lean` | substitution/weakening exchange
family, incl. `nf_substTy` — normalization commutes with hereditary
substitution (the whole content of the β case) |
| `Systemet/L1/Soundness.lean` | `soundness : DefEq t (embNf (nf t))` |
| `Systemet/L1/Completeness.lean` | `completeness : DefEq t u → nf t =
nf u`; `defEq_iff_nf : DefEq t u ↔ nf t = nf u` |
| `Systemet/L1/Decidable.lean` | `decEqNf` / `decEqSp` (hand-rolled
mutual `DecidableEq` — `deriving` does not work across the `Nf`/`Sp`
pair); `decDefEq : (t u : Ty Γ k) → Decidable (DefEq t u)` |

Plus the `PROOF-STATUS.adoc` truth pass (`gated` 11 → 15, ET-2 row
proven, MECH-1 row landed, the satisfied `ET-2 (finish)` OPEN row
removed) and append-only `MANIFEST` / `Systemet.lean` / `Audit.lean`
entries.

## Conflict resolution — read this bit

The pre-PR sync merge (`0104c9c`) hit five conflicts. **Four were
`add/add` artefacts of the squash in #17**, which makes git treat both
sides as independent additions. None were resolved by a blanket
`--ours`/`--theirs`:

- `MANIFEST`, `Systemet.lean`, `Audit.lean` — verified `main`'s content
is **byte-identical** to the branch's and the branch is a **strict
superset** (adds exactly the four ET-2 entries). Branch side taken.
- `PROOF-STATUS.adoc` — every difference is this branch's ET-2 update;
`main` carried no independent edits. Branch side taken.
- **`.github/workflows/proofs.yml` — a genuine two-sided merge.** The
sides differed in *opposite* directions: `main` had the newer
`actions/checkout@3d3c42e` (v7.0.1, from dependabot #26) while the
branch had `curl --proto '=https' --tlsv1.2` (the Sonar S6506 fix). Took
main's newer pin **and** re-applied the branch's https hardening, so
neither is regressed. Both confirmed present post-resolution.

## Evidence (measured on the merged tree, not inherited from #24)

- Cold rebuild after `rm -rf .lake/build` → **Build completed
successfully (16 jobs)**
- `scripts/check-proofs.sh lean4` → **PASS** (real exit 0); audit
reports **20/20 headline items within the trusted base**
- `scripts/scan-dangerous.sh` → **PASS** (real exit 0)
- `scripts/check-proof-status.sh` → **PASS** (real exit 0) — 15 gated,
document agrees
- Forbidden-token scan on the four new proof files → clean
- `#print axioms` on `soundness`, `completeness`, `defEq_iff_nf`,
`decDefEq`, `decEqNf`, `decEqSp`, `nf_substTy` → **`[propext,
Quot.sound]` only**; no `sorryAx`, no user axioms, not even
`Classical.choice`

Real exit codes were checked directly — piping a gate through `tail` and
reading `$?` reports *tail's* status, which is how a red gate can look
green.

## Scope — what this does *not* claim

`DefEq` here is **β + equivalence + congruence. η is not included** and
remains an OPEN row. **ET-3 is unaffected** — its η and model directions
stay open. `PROOF-STATUS.adoc` marks ET-2 proven *for the L1 core
calculus*, under the core-vs-full-theory caveat that file already
carries.

**ET-14 (TEA erasure) is untouched and remains the headline open
problem**, gated on the owner's ET-16 / L0-lowering ADR.

## Merge notes

Per the base ruleset, **squash is the only merge that works** here
(rebase merges cannot be signed by GitHub bots), and the phantom
required `Dependabot` context means this will need `--admin`. Not merged
by me — that call is yours.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

.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

flake.nix

@@ -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)

scripts/check-no-vlang.sh

@@ -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/MANIFEST

@@ -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