Computed virtual width and register normalization

Setup reads the actual original headers and executes the existing ceiling-logarithm and natural-power programs. No logarithm, modulus, bounded initial scratch or source register certificate is supplied in the input.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.setup_fits {W b N Q : ℕ} (hfit : WordRAM.Fits W (b + 4 * windowSize N Q + 1024)) : sourceWidth N Q ≤ W ∧ N + Q + 3 ≤ windowSize N Q ∧ sourceWidth N Q < windowSize N Q

The explicit physical numerical margin covers setup and the smaller native source width.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.CallableProduct.exec_setup {W b N Q : ℕ} (x : WordRAM.Data 163) (hb : x.regs Reg.base = b) (hN : x.mem (b + 3) = N) (hQ : x.mem (b + 4) = Q) (hfit : WordRAM.Fits W (b + 4 * windowSize N Q + 1024)) : ∃ (y : WordRAM.Data 163), WordRAM.ExecWithin W setup x y (517 * Nat.clog 2 (N + Q + 3) + 184) ∧ y.mem = x.mem ∧ WordRAM.MemoryWindow.Matches (sourceWidth N Q) b (WordRAM.MemoryWindow.view (sourceWidth N Q) b y) y ∧ WordRAM.Data.Bounded (sourceWidth N Q) (WordRAM.MemoryWindow.view (sourceWidth N Q) b y)

Actual setup computes the modulus, normalizes the fixed source register bank and preserves every caller memory word. Its charge is logarithmic in original dimensions and query count.