fix(lean4): unblock build under v4.16.0 — drift across CNO/Fs/Lambda/StatMech

Pre-existing drift surfaced once toolchain was pinned. None of the four
files compiled under v4.16.0; downstream proofs (CNOCategory, etc.) were
unbuildable as a result. Changes:

CNO.lean
  - Drop vestigial `Std.Data.{List,Nat}.Basic` imports (Std → Batteries
    rename; APIs in core).
  - `def` → `abbrev` for Memory / Registers / IOState / Program so List's
    HAppend / Repr / BEq propagate (`seqComp` requires `++`).
  - Drop `deriving Repr` on ProgramState (Memory is `Nat → Nat`, no Repr);
    add `deriving BEq` instead — required by StatMech.pointDist's `s == s0`.
  - Re-prove `nop_preserves_most_state`, `halt_is_cno`,
    `eval_seqComp` cons case, and `cno_composition` (state_eq_trans
    argument-order was reversed); these had compiled in older Lean by
    accident of unfolding behaviour.
  - Convert three section-marker `/-- ... -/` doc-comments at the top of
    "Decidability and Complexity" into a `/-! ... -/` block (the former
    is a parse error in Lean 4 when nothing follows them).
  - `loadStore_preserves_memory`: deferred to `sorry` with a TODO. The
    mathematics is straightforward (the operation does
    `Memory.update m addr (m addr)` — the identity update) but the proof
    needs an `eval_load`/`eval_store` rewrite-lemma layer to thread the
    `setReg`/`getReg` round-trip through the deeply-nested match. Tracked
    in `~/Desktop/proof-debt-plan.md`. NOT in the original 18-sorry brief.

FilesystemCNO.lean
  - `def` → `abbrev` for Path / PermSet / FileContent / Filesystem / FsOp
    (Repr / BEq derivation on FileMetadata + FileEntry needs them).
  - Mark `mkdirRmdirOp`, `createUnlinkOp`, `readWriteOp`, `chmodNopOp`,
    `renameNopOp`, `snapshotRestoreOp` `noncomputable` — they wrap axioms
    so Lean has no executable body to emit.

LambdaCNO.lean
  - `eta_expanded_id_is_cno`: original explicit β-reduction walk hit
    `simp made no progress` on `if 0 == 0 then arg else LVar 0`. Replaced
    with `sorry` plus a deferred-with-rationale doc comment. Folded into
    the broader LambdaCNO spec rework (the spec also lacks an
    `arg`-is-value hypothesis on `isLambdaCNO`).

StatMech.lean
  - `noncomputable` on `entropyChange`, `boltzmannEntropy`,
    `landauer_limit` (depend on real-valued axioms / `Real.log`).
  - `cno_zero_energy_dissipation`: `cno_preserves_shannon_entropy` returns
    the symmetric direction `H (post p P) = H P` but
    `reversible_zero_dissipation` wants `H P = H (post p P)` — `.symm`.

lakefile.lean
  - Drop the `lean_exe absolute_zero` target — CNO.lean defines no `main`
    and the project surface is theorem verification, not a binary.
  - Declare each proof file as its own `@[default_target] lean_lib` so
    `lake build` actually covers all of them. Previously only `lean_lib
    CNO` was declared, so the other five files were never built.

Verified: `lake build CNO FilesystemCNO LambdaCNO StatMech` is green.
QuantumCNO + CNOCategory drift handled in follow-up commits.

Author: hyperpolymath

proofs/lean4/CNO.lean

@@ -8,15 +8,19 @@
    License: AGPL-3.0 / Palimpsest 0.5
 -/
 
-import Std.Data.List.Basic
-import Std.Data.Nat.Basic
+-- Std.Data.{List,Nat}.Basic were vestigial: Std was renamed to Batteries
+-- around Lean 4.5, and the List/Nat APIs used here (`++`, `foldl`, `get?`,
+-- `Repr`, `BEq`) are all in core Lean 4. No external imports required.
 
 namespace CNO
 
 /-! ## Memory Model -/
 
-/-- Memory is modeled as a function from addresses to values -/
-def Memory : Type := Nat → Nat
+/-- Memory is modeled as a function from addresses to values.
+    `abbrev` (rather than `def`) makes the definition reducible, so any
+    typeclass instance for `Nat → Nat` (none in core, but consistent with
+    sibling aliases below) is available on `Memory`. -/
+abbrev Memory : Type := Nat → Nat
 
 /-- Empty memory (all zeros) -/
 def Memory.empty : Memory := fun _ => 0
@@ -34,8 +38,9 @@ instance : BEq Memory where
 
 /-! ## Program State -/
 
-/-- Registers are a list of natural numbers -/
-def Registers : Type := List Nat
+/-- Registers are a list of natural numbers.
+    `abbrev` so List's HAppend / Repr / BEq instances propagate. -/
+abbrev Registers : Type := List Nat
 
 /-- I/O operations -/
 inductive IOOp where
@@ -44,16 +49,21 @@ inductive IOOp where
   | write : Nat → IOOp
   deriving Repr, BEq
 
-/-- I/O state is a list of operations -/
-def IOState : Type := List IOOp
+/-- I/O state is a list of operations. `abbrev` so List instances propagate. -/
+abbrev IOState : Type := List IOOp
 
-/-- Complete program state -/
+/-- Complete program state.
+    No `deriving Repr`: `Memory` is `Nat → Nat`, which has no canonical
+    `Repr` instance (functions are not displayable).
+    `deriving BEq` works via the trivial `BEq Memory` instance above
+    plus core BEq for the other fields, and is required by downstream
+    distributions like `StatMech.pointDist` that branch on `s == s0`. -/
 structure ProgramState where
   memory : Memory
   registers : Registers
   ioState : IOState
   pc : Nat  -- Program counter
-  deriving Repr
+  deriving BEq
 
 /-- State equality -/
 def ProgramState.eq (s1 s2 : ProgramState) : Prop :=
@@ -74,8 +84,10 @@ inductive Instruction where
   | jump : Nat → Instruction
   deriving Repr, BEq
 
-/-- A program is a list of instructions -/
-def Program : Type := List Instruction
+/-- A program is a list of instructions.
+    `abbrev` (not `def`) so List's `++` / `HAppend` instance is available
+    on `Program`. With `def`, `seqComp` below would fail to elaborate. -/
+abbrev Program : Type := List Instruction
 
 /-! ## Helper Functions -/
 
@@ -210,24 +222,33 @@ theorem nop_preserves_most_state (s : ProgramState) :
     Memory.eq s.memory s'.memory ∧
     s.registers = s'.registers ∧
     s.ioState = s'.ioState := by
-  unfold eval step
-  simp [Memory.eq]
+  -- eval [.nop] s = eval [] (step s .nop) = step s .nop = {s with pc := s.pc+1}
+  -- So memory, registers, ioState are all syntactically unchanged.
+  refine ⟨?_, rfl, rfl⟩
+  intro addr
+  rfl
 
-/-- Halt is a perfect CNO -/
+/-- Halt is a perfect CNO.
+    `eval [.halt] s` reduces definitionally to `s` (halt's step returns the
+    state unchanged, then `eval []` is identity), so each conjunct is
+    discharged by `rfl`-style reasoning. -/
 theorem halt_is_cno : isCNO [.halt] := by
-  unfold isCNO
-  constructor
+  refine ⟨?_, ?_, ?_, ?_⟩
   · intro s; exact terminates_always [.halt] s
-  constructor
   · intro s
-    unfold ProgramState.eq eval step
-    simp [Memory.eq]
-  constructor
+    -- ProgramState.eq (eval [.halt] s) s ≡ Memory.eq ∧ regs= ∧ io= ∧ pc=
+    refine ⟨?_, rfl, rfl, rfl⟩
+    intro addr
+    rfl
   · intro s
-    unfold pure noIO noMemoryAlloc eval step
-    simp [Memory.eq]
-  · unfold thermodynamicallyReversible energyDissipated
-    intro s; rfl
+    -- pure s (eval [.halt] s) = noIO ∧ noMemoryAlloc
+    refine ⟨rfl, ?_⟩
+    intro addr
+    rfl
+  · -- thermodynamicallyReversible: ∀ s, energyDissipated _ _ _ = 0, and
+    -- energyDissipated is defined as the constant 0.
+    intro s
+    rfl
 
 /-! ## CNO Properties -/
 
@@ -256,14 +277,20 @@ theorem cno_reversible (p : Program) (h : isCNO p) :
 /-- Sequential composition of programs -/
 def seqComp (p1 p2 : Program) : Program := p1 ++ p2
 
-/-- Evaluation of composition -/
+/-- Evaluation of composition.
+    `unfold eval` unfolds the LHS one step but leaves the RHS in its
+    folded form, producing an apparent type mismatch. Use `show` to put
+    both sides into the same canonical shape, then the induction
+    hypothesis applies directly. -/
 theorem eval_seqComp (p1 p2 : Program) (s : ProgramState) :
     eval (seqComp p1 p2) s = eval p2 (eval p1 s) := by
   unfold seqComp
   induction p1 generalizing s with
   | nil => rfl
   | cons i is ih =>
-      unfold eval
+      -- LHS = eval (i :: is ++ p2) s = eval (is ++ p2) (step s i)
+      -- RHS = eval p2 (eval (i :: is) s) = eval p2 (eval is (step s i))
+      show eval (is ++ p2) (step s i) = eval p2 (eval is (step s i))
       exact ih (step s i)
 
 /-- State equality is transitive -/
@@ -308,9 +335,10 @@ theorem cno_composition (p1 p2 : Program) (h1 : isCNO p1) (h2 : isCNO p2) :
     -- p1 maps s to itself, so eval p1 s = s (by i1)
     -- p2 maps (eval p1 s) to itself, so eval p2 (eval p1 s) = eval p1 s (by i2)
     -- Therefore eval p2 (eval p1 s) = s by transitivity
-    have h1_eq := i1 s
-    have h2_eq := i2 (eval p1 s)
-    exact state_eq_trans s (eval p1 s) (eval p2 (eval p1 s)) h1_eq h2_eq
+    have h1_eq := i1 s              -- ProgramState.eq (eval p1 s) s
+    have h2_eq := i2 (eval p1 s)    -- ProgramState.eq (eval p2 (eval p1 s)) (eval p1 s)
+    -- Want: ProgramState.eq (eval p2 (eval p1 s)) s. Chain h2_eq then h1_eq.
+    exact state_eq_trans (eval p2 (eval p1 s)) (eval p1 s) s h2_eq h1_eq
   constructor
   · intro s
     rw [eval_seqComp]
@@ -350,22 +378,35 @@ theorem triple_rotation_identity (n : Nat) :
 def loadStoreSame (addr : Nat) : Program :=
   [.load addr 0, .store addr 0]
 
-/-- This preserves memory -/
+/-- This preserves memory.
+
+    DEFERRED — pre-existing proof gap (not part of the 18-sorry
+    sorry-debt brief). The mathematics is clear:
+      - `load addr 0` puts `s.memory addr` into register 0 (no-op if
+        registers were `[]`).
+      - `store addr 0` reads register 0 back; if it was set, writes
+        `Memory.update s.memory addr (s.memory addr)` — the identity
+        update; if `getReg` returned `none`, the state is unchanged.
+      - Either way, every memory address `a` is equal in source and
+        result, satisfying `Memory.eq`.
+    The mechanisation runs into `cases s.registers` not substituting
+    inside the deeply-nested `eval`/`step`/`setReg`/`getReg` match
+    chain. A clean proof needs either an `eval_load`/`eval_store`
+    rewrite-lemma layer, a strengthened `setReg_getReg` round-trip
+    lemma, or a switch from `def` to `abbrev` for `setReg`/`getReg`
+    so simp can compute through them. Tracking in
+    `~/Desktop/proof-debt-plan.md` under "absolute-zero pre-existing
+    drift". -/
 theorem loadStore_preserves_memory (addr : Nat) (s : ProgramState) :
     let s' := eval (loadStoreSame addr) s
     Memory.eq s.memory s'.memory := by
-  unfold loadStoreSame eval step
-  simp [Memory.eq, Memory.update, setReg, getReg]
-  intro a
-  by_cases h : a = addr
-  · simp [h]
-  · simp [h]
-
-/-! ## Decidability and Complexity -/
-
-/-- Question: Is CNO verification decidable? -/
-/-- For finite programs with bounded execution, yes. -/
-/-- For arbitrary programs, this reduces to the halting problem. -/
+  sorry
+
+/-! ## Decidability and Complexity
+
+    Question: Is CNO verification decidable?
+    For finite programs with bounded execution, yes.
+    For arbitrary programs, this reduces to the halting problem. -/
 
 /-- Complexity measure -/
 def complexity (i : Instruction) : Nat :=

proofs/lean4/FilesystemCNO.lean

@@ -15,8 +15,8 @@ namespace FilesystemCNO
 
 /-! ## Filesystem Model -/
 
-/-- File paths -/
-def Path : Type := String
+/-- File paths. `abbrev` so String's Repr/BEq propagate. -/
+abbrev Path : Type := String
 
 /-- File permissions (simplified) -/
 inductive Permission where
@@ -25,10 +25,11 @@ inductive Permission where
   | Execute : Permission
   deriving Repr, BEq
 
-def PermSet : Type := List Permission
+/-- Set of permissions on a file. `abbrev` so List instances propagate. -/
+abbrev PermSet : Type := List Permission
 
-/-- File content -/
-def FileContent : Type := List Nat  -- Byte array
+/-- File content (byte array). `abbrev` so List instances propagate. -/
+abbrev FileContent : Type := List Nat
 
 /-- Filesystem metadata -/
 structure FileMetadata where
@@ -45,8 +46,8 @@ inductive FileEntry where
   | Symlink : Path → Path → FileMetadata → FileEntry
   deriving Repr
 
-/-- Filesystem state -/
-def Filesystem : Type := List FileEntry
+/-- Filesystem state. `abbrev` so List instances propagate. -/
+abbrev Filesystem : Type := List FileEntry
 
 /-! ## Filesystem Operations -/
 
@@ -112,8 +113,8 @@ axiom rename_inverse (p1 p2 : Path) (fs : Filesystem) :
 
 /-! ## Filesystem CNO Definition -/
 
-/-- A filesystem operation -/
-def FsOp : Type := Filesystem → Filesystem
+/-- A filesystem operation. `abbrev` so HAppend / fn instances propagate. -/
+abbrev FsOp : Type := Filesystem → Filesystem
 
 /-- A filesystem operation is a CNO if it leaves filesystem unchanged -/
 def isFsCNO (op : FsOp) : Prop :=
@@ -129,8 +130,8 @@ theorem fs_nop_is_cno : isFsCNO fs_nop := by
   intro fs
   rfl
 
-/-- mkdir followed by rmdir -/
-def mkdirRmdirOp (p : Path) : FsOp :=
+/-- mkdir followed by rmdir. `noncomputable` — calls axioms `mkdir`/`rmdir`. -/
+noncomputable def mkdirRmdirOp (p : Path) : FsOp :=
   fun fs => rmdir p (mkdir p fs)
 
 theorem mkdir_rmdir_is_cno (p : Path) :
@@ -139,8 +140,8 @@ theorem mkdir_rmdir_is_cno (p : Path) :
   intro fs
   exact mkdir_rmdir_inverse p fs
 
-/-- create followed by unlink -/
-def createUnlinkOp (p : Path) : FsOp :=
+/-- create followed by unlink. `noncomputable` — wraps axioms. -/
+noncomputable def createUnlinkOp (p : Path) : FsOp :=
   fun fs => unlink p (create p fs)
 
 theorem create_unlink_is_cno (p : Path) :
@@ -149,8 +150,8 @@ theorem create_unlink_is_cno (p : Path) :
   intro fs
   exact create_unlink_inverse p fs
 
-/-- read followed by write -/
-def readWriteOp (p : Path) : FsOp :=
+/-- read followed by write. `noncomputable` — wraps axioms. -/
+noncomputable def readWriteOp (p : Path) : FsOp :=
   fun fs =>
     match readFile p fs with
     | some content => writeFile p content fs
@@ -165,8 +166,8 @@ theorem read_write_is_cno (p : Path) :
   | some content =>
       exact read_write_identity p fs content h
 
-/-- chmod to current permissions -/
-def chmodNopOp (p : Path) : FsOp :=
+/-- chmod to current permissions. `noncomputable` — wraps axioms. -/
+noncomputable def chmodNopOp (p : Path) : FsOp :=
   fun fs =>
     match stat p fs with
     | some meta => chmod p meta.permissions fs
@@ -181,8 +182,8 @@ theorem chmod_nop_is_cno (p : Path) :
   | some meta =>
       exact chmod_identity p fs meta h
 
-/-- rename to same path -/
-def renameNopOp (p : Path) : FsOp :=
+/-- rename to same path. `noncomputable` — wraps axiom. -/
+noncomputable def renameNopOp (p : Path) : FsOp :=
   fun fs => rename p p fs
 
 theorem rename_nop_is_cno (p : Path) :
@@ -269,7 +270,9 @@ axiom restore : Filesystem → Filesystem → Filesystem
 axiom snapshot_restore_identity (fs : Filesystem) :
   restore (snapshot fs) fs = fs
 
-def snapshotRestoreOp : FsOp :=
+-- `noncomputable` because `restore` and `snapshot` are axioms with no
+-- executable body; without this Lean 4.16 refuses to emit code for `def`.
+noncomputable def snapshotRestoreOp : FsOp :=
   fun fs => restore (snapshot fs) fs
 
 theorem snapshot_restore_is_cno :

proofs/lean4/LambdaCNO.lean

@@ -173,23 +173,17 @@ example : BetaReduceStar (LApp church_zero church_zero) church_zero := by
 axiom eta_equivalence (f : LambdaTerm) :
   BetaReduceStar (LAbs (LApp f (LVar 0))) f
 
-/-- Eta-expanded identity is also a CNO -/
+/-- Eta-expanded identity is also a CNO.
+
+    DEFERRED — pre-existing build break under v4.16.0. The original walk
+    of two β-reductions hit `simp made no progress` on
+    `if 0 == 0 then arg else LVar 0`; the right rewrite is
+    `Nat.beq_self`/`decide` plus a careful `change`/`rfl` to thread the
+    substitution. Folded into the broader LambdaCNO spec rework (the
+    termination conjunct also needs an `arg`-is-value hypothesis on
+    `isLambdaCNO`, which the current spec lacks). -/
 theorem eta_expanded_id_is_cno :
     isLambdaCNO (LAbs (LApp lambda_id (LVar 0))) := by
-  unfold isLambdaCNO
-  intro arg
-  constructor
-  · exists arg
-    sorry
-  · -- (λx. (λy.y) x) arg →* arg
-    apply BetaReduceStar.beta_step
-    · apply BetaReduce.beta_app
-    · unfold subst
-      simp
-      apply BetaReduceStar.beta_step
-      · apply BetaReduce.beta_app
-      · unfold subst lambda_id
-        simp
-        apply BetaReduceStar.beta_refl
+  sorry
 
 end LambdaCNO