Frames for the recursive controller proof

Main results

• PrunedQuery.nodeWrites_child_subset: a recursive child's writes stay in its parent's frame.
• PrunedQuery.notMem_nodeWrites_list: a node's request list remains read-only.
• PrunedQuery.notMem_nodeWrites_ancestor_values: a child preserves its parent's accumulators.

The footprints are the concrete intervals used by the native program. These facts impose no execution or fit hypotheses; they provide the spatial part of the node induction.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.mem_nodeWrites_iff {L f d c : ℕ} (hd : d ≤ L) : c ∈ nodeWrites L f d ↔ ((f + 4 * d ≤ c ∧ c < f + 4 * (L + 1) ∨ f + 4 * (L + 1) + (d + 1) * 10 ^ L ≤ c ∧ c < f + 4 * (L + 1) + (L + 1) * 10 ^ L) ∨ f + 4 * (L + 1) + (L + 1) * 10 ^ L + d * 10 ^ L ≤ c ∧ c < f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L) ∨ f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L ≤ c ∧ c < f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + 10 ^ L

Normalize every row interval to its fixed workspace endpoint.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.nodeWrites_child_subset {L f d : ℕ} (hd : d < L) : nodeWrites L f (d + 1) ⊆ nodeWrites L f d

The recursive child's full writable frame is contained in the parent's frame.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.childWrites_subset_nodeWrites {L f d : ℕ} (hd : d < L) : childWrites L f d ⊆ nodeWrites L f d

The scan-and-push transition changes only cells in the current node's frame.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.emptyChildWrites_subset_nodeWrites {L f d : ℕ} (hd : d < L) : emptyChildWrites L f d ⊆ nodeWrites L f d

The scan-and-skip transition also stays inside the current node's frame.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.notMem_nodeWrites_before {L f d c : ℕ} (hd : d ≤ L) (hc : c < f) : c ∉ nodeWrites L f d

No node changes the original input or any other cell below the workspace.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.notMem_nodeWrites_list {L f d q : ℕ} (hd : d ≤ L) (hq : q < 10 ^ L) : f + 4 * (L + 1) + d * 10 ^ L + q ∉ nodeWrites L f d

A node preserves every occupied or unoccupied cell of its own request row.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.notMem_nodeWrites_ancestor_frame {L f d e j : ℕ} (hd : d ≤ L) (he : e < d) (hj : j < 4) : f + 4 * e + j ∉ nodeWrites L f d

Returning from a child preserves all four words of every ancestor frame.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.notMem_nodeWrites_ancestor_values {L f d e q : ℕ} (hd : d ≤ L) (he : e < d) (hq : q < 10 ^ L) : f + 4 * (L + 1) + (L + 1) * 10 ^ L + e * 10 ^ L + q ∉ nodeWrites L f d

Returning from a child preserves every value-directory cell in an ancestor's row.