fix: Blitter6502OISC — inline let binders in execSUBLEQ, remove Repr (ℕ→ℕ)

execSUBLEQ now uses direct field syntax instead of let binders,
fixing the 'rw can't find pattern' errors on branch/fall-through
theorems. Removed deriving Repr from M6502State (functions aren't
Repr-able).

Build: 3299 jobs, 0 errors

formal/SilverSight/Blitter6502OISC.lean

@@ -59,20 +59,18 @@ structure SUBLEQ where
 structure M6502State where
   mem : ℕ → ℕ             -- memory as function (0 = uninitialized)
   pc  : ℕ                  -- program counter
-  deriving Repr
 
 /-- Execute one SUBLEQ instruction.
 
     M[b] := M[b] - M[a]
     if M[b] ≤ 0 then PC := c else PC := PC + 3 (3 operands) -/
 def execSUBLEQ (s : M6502State) (inst : SUBLEQ) : M6502State :=
-  let aVal := s.mem inst.srcA.addr
-  let bVal := s.mem inst.dstB.addr
-  let result := bVal - aVal
-  let newPC := if result ≤ 0 then inst.branch.addr else s.pc + 3
-  let newMem := fun addr =>
-    if addr == inst.dstB.addr then result else s.mem addr
-  { mem := newMem, pc := newPC }
+  { mem := fun addr => if addr == inst.dstB.addr
+      then s.mem inst.dstB.addr - s.mem inst.srcA.addr
+      else s.mem addr
+  , pc := if s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0
+      then inst.branch.addr
+      else s.pc + 3 }
 
 /-- Blitter: copy N bytes from src to dst using a SUBLEQ loop.
 
@@ -125,21 +123,22 @@ def predictedThroughput (baseRate : ℕ) (prog : BlitterProgram) : ℕ :=
 /-- SUBLEQ execution: result = M[b] - M[a]. -/
 theorem subleq_subtracts (s : M6502State) (inst : SUBLEQ) :
     (execSUBLEQ s inst).mem inst.dstB.addr = s.mem inst.dstB.addr - s.mem inst.srcA.addr := by
-  simp [execSUBLEQ]
+  unfold execSUBLEQ
+  simp
 
 /-- SUBLEQ branches when result ≤ 0. -/
 theorem subleq_branches_on_le_zero (s : M6502State) (inst : SUBLEQ)
     (h : s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0) :
     (execSUBLEQ s inst).pc = inst.branch.addr := by
-  simp [execSUBLEQ]
-  rw [if_pos h]
+  unfold execSUBLEQ
+  simp [h]
 
 /-- SUBLEQ falls through when result > 0. -/
 theorem subleq_falls_through (s : M6502State) (inst : SUBLEQ)
     (h : s.mem inst.dstB.addr - s.mem inst.srcA.addr > 0) :
     (execSUBLEQ s inst).pc = s.pc + 3 := by
-  simp [execSUBLEQ]
-  rw [if_neg (by omega : ¬(s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0))]
+  unfold execSUBLEQ
+  simp [h]
 
 /-- Blitter step count: 3 SUBLEQ instructions per byte. -/
 theorem blitter_step_count (prog : BlitterProgram) :
@@ -153,19 +152,32 @@ theorem blitter_uses_subleq_throughput (baseRate : ℕ) (prog : BlitterProgram)
     predictedThroughput baseRate prog =
       HCMR.throughput baseRate .subleqWord * blitterInstrCount prog := rfl
 
-/-- Ring dispatch is at least as fast as SUBLEQ for the blitter.
+/-- Ring dispatch would be at least as fast as SUBLEQ for the blitter.
 
-    If the blitter used ring dispatch (zero contention) instead of SUBLEQ
-    (82.3% contention), throughput would be at least as high. This is the
-    HCMR ordering theorem applied to the blitter. Stated with `≥` because
-    Q16_16 truncation makes the two sides equal when `byteCount = 0`
-    (both products vanish), and `omega` cannot discharge the nonlinear
-    `a * c > b * c` goal that the strict version would need. -/
+    If the blitter used ring dispatch (zero contention) instead of
+    SUBLEQ (82.3% contention), throughput would be `baseRate × 1.0`
+    instead of `baseRate × 0.177` per instruction. This is the HCMR
+    ordering theorem applied to the blitter.
+
+    NOTE: stated with `≥` rather than `>` because when `byteCount = 0`,
+    both throughputs are 0 and the strict ordering is vacuously false.
+    The non-strict ordering holds for all `baseRate > 0`. -/
 theorem ring_faster_than_subleq_blitter (baseRate : ℕ) (prog : BlitterProgram)
     (hbase : baseRate > 0) :
     HCMR.throughput baseRate .ringDispatch * blitterInstrCount prog ≥
     predictedThroughput baseRate prog := by
-  simp only [predictedThroughput]
-  exact Nat.mul_le_mul_right _ (HCMR.ring_fastest_subleq_avx baseRate hbase).1
+  simp only [predictedThroughput, HCMR.throughput, HCMR.selfLoopProb, blitterInstrCount]
+  have hpos : (0 : ℕ) < 65536 := by norm_num
+  have h_left : baseRate * 65536 / 65536 = baseRate := by
+    rw [Nat.mul_comm]; exact Nat.mul_div_cancel_left baseRate hpos
+  have h_right_le : baseRate * 11628 / 65536 ≤ baseRate := by
+    have h_step : baseRate * 11628 / 65536 ≤ baseRate * 65536 / 65536 :=
+      Nat.div_le_div_right (Nat.mul_le_mul_left baseRate (by norm_num : (11628:ℕ) ≤ 65536))
+    have h_cancel : baseRate * 65536 / 65536 = baseRate := by
+      rw [Nat.mul_comm]; exact Nat.mul_div_cancel_left baseRate hpos
+    rw [h_cancel] at h_step
+    exact h_step
+  rw [h_left]
+  exact Nat.mul_le_mul_right _ h_right_le
 
 end SilverSight.Blitter6502OISC