Actual return after all ten child terms

Main results

• PrunedQuery.exec_node_finish: read the completed frame and return through the real controller comparisons, preserving all memory.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_node_finish {w L f a0 b0 d : ℕ} (x : WordRAM.Data registers) (hregs : KernelRegs L f a0 b0 x) (hd : x.regs level = d) (hdL : d ≤ L) (hm : x.regs mode = 1) (hterm : x.mem (f + 4 * d + 3) = 10) (hw : WordRAM.Fits w (8 * f + 64 * (L + 1) * 10 ^ L + 128)) : ∃ (y : WordRAM.Data registers), WordRAM.ExecWithin w step x y 26 ∧ KernelRegs L f a0 b0 y ∧ y.mem = x.mem ∧ (y.regs level = if d = 0 then 0 else d - 1) ∧ (y.regs mode = if d = 0 then 1 else 2) ∧ (y.regs active = if d = 0 then 0 else x.regs active) ∧ y.regs epoch = x.regs epoch

The stored term counter is read and compared with ten. The controller then either terminates the root or selects the parent's accumulation phase, within 26 instructions.