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

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