Input-derived bounds for native pruned evaluation

Main definitions

• PrunedQuery.nodeBudget: a scalar address/counter budget, including remaining epochs.
• PrunedQuery.magnitudeBound: covers both operands and every partial sum.

Main results

• PrunedQuery.nodeBudget_input_le: the concrete input-derived bound covers the root budget.
• PrunedQuery.fits_partialValue: the original magnitude bound derives partial accumulator fits.

The only fit assumptions are numerical inequalities on original parameters. No state-by-state fit assertion or execution/time certificate is supplied.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nodeBudget (L f a b E n : ℕ) : ℕ

A node budget for ordinary pointers, powers, counters and all remaining fresh epochs.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.evaluationBudget (L f a b q o Q E : ℕ) : ℕ

Root deduplication and reporting additionally use the original query/output pointers and the full supplied query count, which may exceed the distinct-set capacity.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.kernelBudget (L f a b q o Q E : ℕ) : ℕ

The callable kernel also computes its own powers and workspace pointers. Its numeric admission includes those setup bounds and permits arbitrary separated input/output addresses.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.evaluationBudget_input_le (L Q : ℕ) : evaluationBudget L (scratchBase L Q) 3 (3 + 10 ^ L) (3 + 2 * 10 ^ L) (outputBase L Q) Q 0 ≤ addressBound L Q

The ordinary initialized layout covers evaluation, including repeated supplied queries.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nodeBudget_input_le (L Q : ℕ) : nodeBudget L (scratchBase L Q) 3 (3 + 10 ^ L) 1 L ≤ addressBound L Q

The larger concrete standalone bound covers initialization and every root parameter.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nodeBudget_child_le {L f a b E E' n : ℕ} (hE : E' + epochAllowance n ≤ E + epochAllowance (n + 1)) : nodeBudget L f a b E' n ≤ nodeBudget L f a b E (n + 1)

Epoch allocation to a child is paid for by the remaining parent allowance.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.magnitudeBound (L A B : ℕ) : ℕ

A single original-parameter envelope covers the two inputs and all tensor partial sums.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.magnitudeBound_fits {w L A B : ℕ} (hw : 0 < w) (hfit : magnitudeBound L A B < 2 ^ (w - 1)) : GenericRAM.Signed.Fits w ↑(magnitudeBound L A B)

The positive-endpoint inequality makes the nonnegative envelope a signed fitting value.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.fits_left {w L A B : ℕ} {z : ℤ} (hfit : GenericRAM.Signed.Fits w ↑(magnitudeBound L A B)) (hz : |z| ≤ ↑A) : GenericRAM.Signed.Fits w z

The original bound on one input entry derives its signed fit through the common envelope.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.fits_right {w L A B : ℕ} {z : ℤ} (hfit : GenericRAM.Signed.Fits w ↑(magnitudeBound L A B)) (hz : |z| ≤ ↑B) : GenericRAM.Signed.Fits w z

The right operand uses the same envelope, including the zero-input boundary.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.fits_product {w L A B : ℕ} {a b : ℤ} (hfit : GenericRAM.Signed.Fits w ↑(magnitudeBound L A B)) (ha : |a| ≤ ↑A) (hb : |b| ≤ ↑B) : GenericRAM.Signed.Fits w (a * b)

The leaf product fits the same envelope, including when either input bound is zero.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.fits_partialValue {w L n A B : ℕ} (hn : n + 1 ≤ L) (hfit : GenericRAM.Signed.Fits w ↑(magnitudeBound L A B)) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (ha : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |a v| ≤ ↑A) (hb : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |b v| ≤ ↑B) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (q : MatrixMultiplication.Schonhage.OutStr (n + 1)) (k : ℕ) : GenericRAM.Signed.Fits w (partialValue a b S q k)

A partial sum at any remaining depth fits by the original global magnitude inequality.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.fits_childResult {w L n A B : ℕ} (hn : n ≤ L) (hfit : GenericRAM.Signed.Fits w ↑(magnitudeBound L A B)) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (ha : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |a v| ≤ ↑A) (hb : ∀ (v : MatrixMultiplication.Schonhage.Leaf (n + 1)), |b v| ≤ ↑B) (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (lam : MatrixMultiplication.Schonhage.Term) (q : MatrixMultiplication.Schonhage.OutStr n) : GenericRAM.Signed.Fits w (MatrixMultiplication.Schonhage.Pruned.childResult a b S lam q)

Every returned child result fits, including an unselected or skipped zero value.