Finite-set invariant of the native deduplicating scan

Main definitions

• PrunedQuery.scanSet: the selected, shortened codes among a processed input prefix.

Main results

• PrunedQuery.scanSet_succ: the exact insertion made by one scan step.
• PrunedQuery.scanSet_child: agreement of the child scan with childCodes.

These describe the native loop's mathematical invariant; they do not assume its execution.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.selected (child : Bool) (term code : ℕ) : Prop

Root scans retain every query; child scans retain exactly contributing first digits.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.instDecidableSelected (child : Bool) (term code : ℕ) : Decidable (selected child term code)

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.shortened (child : Bool) (code : ℕ) : ℕ

Child requests discard one digit; root requests keep the supplied complete code.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSet (child : Bool) (term : ℕ) (input : ℕ → ℕ) (k : ℕ) : Finset ℕ

The deduplicated codes selected from the first k actual input entries.

@[simp]

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSet_zero (child : Bool) (term : ℕ) (input : ℕ → ℕ) : scanSet child term input 0 = ∅

No input positions have been visited initially.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSet_succ (child : Bool) (term : ℕ) (input : ℕ → ℕ) (k : ℕ) : scanSet child term input (k + 1) = if selected child term (input k) then insert (shortened child (input k)) (scanSet child term input k) else scanSet child term input k

A scan step inserts one selected suffix, leaving any previous occurrence deduplicated.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.card_scanSet_le (child : Bool) (term : ℕ) (input : ℕ → ℕ) (k : ℕ) : (scanSet child term input k).card ≤ k

At most one new distinct code is emitted for each processed input word.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSet_root (term : ℕ) (input : ℕ → ℕ) (k : ℕ) : scanSet false term input k = Finset.image input (Finset.range k)

Root deduplication computes exactly the image of the input prefix.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSet_child (term : ℕ) (input : ℕ → ℕ) (k : ℕ) : scanSet true term input k = childCodes (Finset.image input (Finset.range k)) term

A child scan uses the same selected quotient image as the finite pruning specification.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.scanSet_bounded {child : Bool} {term k capacity : ℕ} {input : ℕ → ℕ} (h : ∀ i < k, selected child term (input i) → shortened child (input i) < capacity) (q : ℕ) : q ∈ scanSet child term input k → q < capacity

Every stored code lies in the concrete destination capacity when each selected source does.