Memory invariant of a timestamped query list

Main definitions

• PrunedQuery.ScanMemory: a distinct finite list and its timestamp membership directory.

Main results

• PrunedQuery.ScanMemory.insert_new: the two actual stores preserve the invariant on insertion.

The invariant describes memory contents only. Execution and instruction charges are proved separately for the native scan; no execution certificate is included here.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory (mem : ℕ → ℕ) (out stamps epoch capacity : ℕ) (S : Finset ℕ) : Prop

The occupied output prefix enumerates S once, and the timestamp table identifies exactly its members. Older timestamps may remain elsewhere in the directory.

• bounded (q : ℕ) : q ∈ S → q < capacity

  Each listed value is a valid directory index.

• stamp_le (q : ℕ) : q < capacity → mem (stamps + q) ≤ epoch

  Every timestamp is at most the current epoch.

• marked (q : ℕ) : q < capacity → (mem (stamps + q) = epoch ↔ q ∈ S)

  The current epoch is exactly the membership marker.

• listed : ∃ (v : Fin S.card → ℕ), Function.Injective v ∧ Set.range v = ↑S ∧ { base := out, length := S.card }.Realizes mem v

  The actual occupied prefix is an injective enumeration of the set.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.card_le {mem : ℕ → ℕ} {out stamps epoch capacity : ℕ} {S : Finset ℕ} (h : ScanMemory mem out stamps epoch capacity S) : S.card ≤ capacity

A realized distinct list cannot exceed its concrete directory capacity.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.congr {mem mem' : ℕ → ℕ} {out stamps epoch capacity : ℕ} {S : Finset ℕ} (h : ScanMemory mem out stamps epoch capacity S) (hlist : ∀ i < S.card, mem' (out + i) = mem (out + i)) (hstamp : ∀ q < capacity, mem' (stamps + q) = mem (stamps + q)) : ScanMemory mem' out stamps epoch capacity S

Agreement on the occupied list and timestamp directory preserves the scan invariant. Unoccupied list cells have no specified meaning and need not agree.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.image_read {mem : ℕ → ℕ} {out stamps epoch capacity : ℕ} {S : Finset ℕ} (h : ScanMemory mem out stamps epoch capacity S) : Finset.image (fun (i : ℕ) => mem (out + i)) (Finset.range S.card) = S

Reading the occupied native list gives exactly its represented finite set.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.injOn_read {mem : ℕ → ℕ} {out stamps epoch capacity : ℕ} {S : Finset ℕ} (h : ScanMemory mem out stamps epoch capacity S) : Set.InjOn (fun (i : ℕ) => mem (out + i)) {i : ℕ | i < S.card}

Occupied native list positions store different codes.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.card_lt_of_notMem {mem : ℕ → ℕ} {out stamps epoch capacity : ℕ} {S : Finset ℕ} (h : ScanMemory mem out stamps epoch capacity S) {q : ℕ} (hq : q < capacity) (hnew : q ∉ S) : S.card < capacity

An unseen valid code leaves a free output cell for its insertion.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.empty {mem : ℕ → ℕ} {out stamps epoch capacity : ℕ} (h : ∀ q < capacity, mem (stamps + q) < epoch) : ScanMemory mem out stamps epoch capacity ∅

A fresh epoch establishes the empty directory without clearing its cells.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.ScanMemory.insert_new {mem : ℕ → ℕ} {out stamps epoch capacity : ℕ} {S : Finset ℕ} (h : ScanMemory mem out stamps epoch capacity S) {q : ℕ} (hq : q < capacity) (hnew : q ∉ S) (hsep : out + capacity ≤ stamps ∨ stamps + capacity ≤ out) : ScanMemory (Function.update (Function.update mem (out + S.card) q) (stamps + q) epoch) out stamps epoch capacity (insert q S)

Append one previously unseen code, then mark its directory entry. Disjointness of the two concrete blocks ensures that neither store corrupts the other representation.