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

[hyperpolymath]

Summary

Lean half of standards#133. Repair two root-cause defects that prevented lake build from completing on proofs/lean4/CNO.lean:

1. private lemma keyword used in 3 helper lemmas (setReg_cons_zero, getReg_cons_zero, Memory.update_same_pointwise). lemma is a Mathlib alias, but this file ships with zero imports by intentional design (L11–13 comment). Lean 4 core parser only accepts theorem. Switched all 3 to private theorem. The downstream "unknown identifier setReg_cons_zero" error at L498 was a cascading consequence and resolved too.
2. Redundant simp only [] at L482 in the nil-branch of loadStore_preserves_memory. 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 (kernel ι-reductions on [].get? and the match none with ... | none => s arm). Dropping simp only [] lets intro a; rfl close.

Test plan

• lake build CNO exits 0
• lake build (full project, 6 libraries) exits 0
• Only linter warnings remain (unused variable at L37/L181/QuantumCNO; pre-existing, not in scope)
• No sorry or axiom introduced in CNO.lean (verified: CNO.lean is axiom-free; the existing axioms in LambdaCNO.lean/StatMech.lean/FilesystemCNO.lean are out of scope for this issue)

Refs

`Refs hyperpolymath/standards#133` — Lean half of "[P2] absolute-zero: finish Lean CNO cons-case + Coq tier-0 rebuild". The Coq tier-0 rebuild (4 axioms in `proofs/coq/common/CNO.v`: `eval_deterministic`, `cno_decidable`, `eval_respects_state_eq_{left,right}`) is the other half and will be filed separately.

🤖 Generated with Claude Code

[github-actions]

🔍 Hypatia Security Scan

Findings: 68 issues detected

Severity	Count
🔴 Critical	10
🟠 High	11
🟡 Medium	47

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Stray AI.a2ml in root -- use 0-AI-MANIFEST.a2ml only",
    "type": "banned",
    "file": "AI.a2ml",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "Superseded by 0-AI-MANIFEST.a2ml",
    "type": "banned",
    "file": "AI.djot",
    "action": "delete",
    "rule_module": "root_hygiene",
    "severity": "high"
  },
  {
    "reason": "No test directory or test files found",
    "type": "no_tests",
    "file": "/home/runner/work/absolute-zero/absolute-zero",
    "action": "flag",
    "rule_module": "honest_completion",
    "severity": "high",
    "deduction": 20
  },
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action actions/checkout@v6.0.2 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/configure-pages@v6 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/jekyll-build-pages@v1 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action actions/upload-pages-artifact@v5 needs attention",
    "type": "unpinned_action",
    "file": "jekyll-gh-pages.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "medium"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence