fix(lean4/cno): finish loadStore_preserves_memory cons-case build (#23)

Two root causes of the soundness-repair-in-flight build failure:

1. `private lemma` keyword was used in 3 places (L399 `setReg_cons_zero`,
   L404 `getReg_cons_zero`, L410 `Memory.update_same_pointwise`). The
   `lemma` alias is provided by Mathlib (`Mathlib.Tactic`), but this file
   declares no imports (`namespace CNO` at L15, no `import` lines per
   intentional design — L11–13 comment "No external imports required").
   Lean 4 core parser only accepts `theorem`. Fixed by changing all 3
   `private lemma` → `private theorem`. The L498 `setReg_cons_zero`
   unknown-identifier error was a downstream consequence and resolved
   too.

2. The nil-case `simp only []` at L482 failed with "simp made no
   progress" — Lean 4.16's `simp only` is strict about needing at least
   one lemma. After `unfold setReg getReg`, the goal reduces to
   `Memory.eq s.memory s.memory` by definitional equality alone
   (`[].get?` reduces via core `List.get?`'s `Option.none` clause, and
   the resulting `match none with ... | none => s` is an ι-reduction
   handled by the kernel). Dropping the redundant `simp only []` lets
   `intro a; rfl` close the goal directly.

The cons-case branch (`rw [setReg_cons_zero, getReg_cons_zero]; simp
only []; intro a; exact ...`) was correct once the helper lemmas above
parsed.

Build verified: `lake build` exits 0 across all 6 lean libraries (CNO,
CNOCategory, FilesystemCNO, LambdaCNO, QuantumCNO, StatMech). Only
linter warnings remain (pre-existing unused-variable noise at L37, L181;
not addressed in this PR).

Refs hyperpolymath/standards#133. Lean half of "[P2] absolute-zero:
finish Lean CNO cons-case + Coq tier-0 rebuild". Coq tier-0 rebuild is
the other half, filed separately.

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

proofs/lean4/CNO.lean

@@ -384,7 +384,7 @@ def loadStoreSame (addr : Nat) : Program :=
 
 /- ── Helper lemmas for loadStore_preserves_memory ──────────────────────────
 
-   These three private lemmas establish the round-trip property of
+   These three private theorems establish the round-trip property of
    `setReg`/`getReg` for register index 0 and the no-op character of
    `Memory.update m addr (m addr)`.  They are the rewrite-lemma layer
    mentioned in the DEFERRED comment below.
@@ -396,18 +396,18 @@ def loadStoreSame (addr : Nat) : Program :=
    `Memory.update_same_pointwise` is the key identity-update fact: writing
    the value already stored at an address is a no-op, point-wise. -/
 
-private lemma setReg_cons_zero (r val : Nat) (rs : List Nat) :
+private theorem setReg_cons_zero (r val : Nat) (rs : List Nat) :
     setReg (r :: rs) 0 val = val :: rs := by
   unfold setReg
   rfl
 
-private lemma getReg_cons_zero (val : Nat) (rs : List Nat) :
+private theorem getReg_cons_zero (val : Nat) (rs : List Nat) :
     getReg (val :: rs) 0 = some val := by
   unfold getReg
   rfl
 
 /-- Writing the value already at `addr` back to `addr` is a pointwise no-op. -/
-private lemma Memory.update_same_pointwise (m : Memory) (addr a : Nat) :
+private theorem Memory.update_same_pointwise (m : Memory) (addr a : Nat) :
     Memory.update m addr (m addr) a = m a := by
   unfold Memory.update
   -- The branch condition is `a == addr : Bool`.  We case-split on whether
@@ -475,12 +475,10 @@ theorem loadStore_preserves_memory (addr : Nat) (s : ProgramState) :
     -- ⟹ the store instruction takes the `none` error branch → leaves
     --    memory and registers unchanged.
     -- `unfold setReg getReg` expands both defs by their match clauses.
-    -- `simp only []` then applies ι-reductions: `[].get? 0 ↝ none`,
-    -- `match none with ... | none => X ↝ X`, and `.memory` projection;
-    -- the goal collapses to `Memory.eq s.memory s.memory`.
+    -- ι-reductions then collapse the goal: `[].get? 0 ↝ none`,
+    -- `match none with ... | none => X ↝ X`, and `.memory` projection
+    -- happen by definitional equality, so `rfl` closes after `intro a`.
     unfold setReg getReg
-    simp only []
-    -- Goal: Memory.eq s.memory s.memory
     intro a
     rfl
   | cons r rs =>