Memory invariants for the saved routing arrays

Main definitions

• QueriedProduct.SavedGroups: protected words agree with an earlier actual router state.

Main results

• QueriedProduct.SavedGroups.reframe: kernel and producer frames retain the saved arrays.
• QueriedProduct.router_code_lt: executed stable scatter gives a valid query code at every grouped position, including duplicate requests.
• QueriedProduct.SavedGroups.span_bounds: actual saved offsets form admitted kernel spans.

The earlier memory is a proof reference to an executed state, not program input. The native copy theorem establishes these equalities before any low-memory reuse occurs.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.SavedGroups (L m N Q : ℕ) (old μ : ℕ → ℕ) : Prop

Values copied from the actual router state into protected caller-owned arrays.

• offsets (t : ℕ) : t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2 → μ (offsetBase L m N Q + t) = old (Wanted.offsetAddress L m N Q + t)

  All actual offsets, including the terminal offset.

• codes (j : ℕ) : j < Q → μ (codeBase L m N Q + j) = old (Wanted.codeAddress L m N Q + j)

  All actual grouped codes.

• originals (j : ℕ) : j < Q → μ (originalBase L m N Q + j) = old (Wanted.originalAddress L m N Q + j)

  All actual original-position words.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.SavedGroups.reframe {L m N Q : ℕ} {old μ ν : ℕ → ℕ} (h : SavedGroups L m N Q old μ) (hf : ∀ (a : ℕ), offsetBase L m N Q ≤ a → a < groupedBase L m N Q → ν a = μ a) : SavedGroups L m N Q old ν

Preserving the protected readonly interval preserves the saved routing arrays.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.router_code_lt {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) (old : ℕ → ℕ) (hvalues : ∀ (i : Fin qs.length), old (Wanted.codeAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = ↑(PrunedQuery.queryIndex (MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) ↑(qs.get i).1 ↑(qs.get i).2))) (j : ℕ) (hj : j < qs.length) : old (Wanted.codeAddress L m N qs.length + j) < 10 ^ L

Stable scatter covers every grouped cell, so every stored code is a valid query index. The proof uses the existing permutation theorem rather than a supplied inverse table.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.SavedGroups.span_bounds {L m N Q : ℕ} {old μ : ℕ → ℕ} (h : SavedGroups L m N Q old μ) (key : ℕ → ℕ) (hoffsets : ∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2, old (Wanted.offsetAddress L m N Q + t) = Nat.count (fun (k : ℕ) => key k < t) Q) {t : ℕ} (ht : t < MatrixMultiplication.Schonhage.numBands L m N ^ 2) : μ (offsetBase L m N Q + t) ≤ μ (offsetBase L m N Q + t + 1) ∧ μ (offsetBase L m N Q + t + 1) ≤ Q

The actual protected offset words satisfy the kernel's monotone span and count bounds. These inequalities follow from the executed prefix-count meanings, not input certificates.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.QueriedProduct.SavedGroups.span_queries {L m N : ℕ} (hm : m ≤ L) (qs : List (Fin N × Fin N)) {old μ : ℕ → ℕ} (h : SavedGroups L m N qs.length old μ) (hvalues : ∀ (i : Fin qs.length), old (Wanted.codeAddress L m N qs.length + CountingSort.position (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) qs.length ↑i) = ↑(PrunedQuery.queryIndex (MatrixMultiplication.Schonhage.outStrOfPos (MatrixMultiplication.Schonhage.MaskTable.layout hm) ↑(qs.get i).1 ↑(qs.get i).2))) (hoffsets : ∀ t ≤ MatrixMultiplication.Schonhage.numBands L m N ^ 2, old (Wanted.offsetAddress L m N qs.length + t) = Nat.count (fun (k : ℕ) => (Wanted.tileKey L m N ∘ Wanted.inputPairs qs) k < t) qs.length) (T : ℕ × ℕ) (hT : T ∈ MatrixMultiplication.Schonhage.tiles L m N) (a b : ℕ) (ha : μ (offsetBase L m N qs.length + (T.1 * MatrixMultiplication.Schonhage.numBands L m N + T.2)) = a) (hb : μ (offsetBase L m N qs.length + (T.1 * MatrixMultiplication.Schonhage.numBands L m N + T.2 + 1)) = b) (queries : Fin (b - a) → MatrixMultiplication.Schonhage.OutStr L) (hinput : ∀ (i : Fin (b - a)), μ (codeBase L m N qs.length + (a + ↑i)) = ↑(PrunedQuery.queryIndex (queries i))) : Finset.image queries Finset.univ = MatrixMultiplication.Schonhage.wantedStrings (MatrixMultiplication.Schonhage.MaskTable.layout hm) qs.toFinset T.1 T.2

A typed view of the actual saved code span requests exactly the original finite tile set. This uses the existing router's span theorem; the native caller constructs the view by decoding its real words, rather than receiving a query-set or routing certificate.