Skipping a computed empty child

Main results

• PrunedQuery.exec_progress_empty: native scanning and its computed zero count advance the partial-sum invariant without a recursive call or a value store.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_progress_empty {w L f a0 b0 n d p E : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr (n + 1))) (a b : MatrixMultiplication.Schonhage.Leaf (n + 1) → ℤ) (x y : WordRAM.Data registers) (hx : NodeReady L f a0 b0 (n + 1) d p E S x) (k : Fin 10) (hy : NodeProgress L f a0 b0 n d p E S a b x (↑k) y) (hempty : MatrixMultiplication.Schonhage.childSet S (Encoding.termDigits k) = ∅) (hfit : WordRAM.Fits w (nodeBudget L f a0 b0 E (n + 1))) : ∃ (z : WordRAM.Data registers), WordRAM.ExecWithin w step y z (20 * S.card + 33) ∧ NodeProgress L f a0 b0 n d p E S a b x (↑k + 1) z

The proof selects the empty mathematical case, and the actual native scan proves that the machine takes its zero-count branch. Every directory update and loop test is charged.