One charged native tile-count update

Main results

• Wanted.exec_countStep: load the actual pair, compute its tile and increment exactly that bucket while preserving original query memory and all other counts.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tileKey (L m N : ℕ) (q : ℕ × ℕ) : ℕ

A row-major tile key, computed from the two original coordinate words.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.tileKey_lt {L m N : ℕ} (hm : m ≤ L) (q : ℕ × ℕ) (hr : q.1 < N) (hc : q.2 < N) : tileKey L m N q < MatrixMultiplication.Schonhage.numBands L m N ^ 2

Admitted original positions always name one of the actual tiles.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Wanted.exec_countStep {w L m N Q n : ℕ} (hm : m ≤ L) (pairs : ℕ → ℕ × ℕ) (hn : n < Q) (hpair : (pairs n).1 < N ∧ (pairs n).2 < N) (x : WordRAM.Data 96) (hx : Parameters L m N Q x) (hi : x.regs index = n) (hinput : x.mem (5 + 2 * n) = (pairs n).1 ∧ x.mem (5 + 2 * n + 1) = (pairs n).2) (hcounts : ∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2, x.mem (countAddress L Q + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k = t) n) (hfit : WordRAM.Fits w (wordBudget L m N Q)) : ∃ (y : WordRAM.Data 96), WordRAM.ExecWithin w countStep x y 14 ∧ Parameters L m N Q y ∧ y.regs index = n + 1 ∧ (∀ t < MatrixMultiplication.Schonhage.numBands L m N ^ 2, y.mem (countAddress L Q + t) = Nat.count (fun (k : ℕ) => (tileKey L m N ∘ pairs) k = t) (n + 1)) ∧ ∀ (a : ℕ), a < countAddress L Q ∨ countAddress L Q + MatrixMultiplication.Schonhage.numBands L m N ^ 2 ≤ a → y.mem a = x.mem a

The full native count update, including loading both original coordinates. Its count bound comes from the original prefix length, rather than a supplied intermediate-state fit.