Original callee header stores

The native stores place the payload length, computed tensor level and recovered inner depth, outer dimension and actual occurrence count above the producer's heap. No encoded matrix or query table is supplied by this header.

theorem Cslib.Algorithms.WordRAM.ExactTriangle.RecordProduct.exec_writeHeader {W b m n A Q : ℕ} (x : WordRAM.Data 320) (hb : x.regs Reg.base = b) (hm : x.regs Reg.destination = 2 * m) (hA : x.regs Reg.twiceArea = 2 * A) (hQ : x.regs Reg.count = Q) (hn : x.regs Reg.size = n) (h1 : x.regs Reg.one = 1) (h2 : x.regs Reg.two = 2) (h19 : x.regs Reg.nineteen = 19) (h4 : x.regs Reg.four = 4) (hfit : WordRAM.Fits W (b + 19 * m + 2 * A + 2 * Q + 64)) : ∃ (y : WordRAM.Data 320), WordRAM.ExecWithin W writeHeader x y 15 ∧ { base := b, length := 5 }.Realizes y.mem ![4 + 2 * A + 2 * Q, 19 * m, m, n, Q] ∧ (∀ (a : ℕ), a < b ∨ b + 5 ≤ a → y.mem a = x.mem a) ∧ ∀ (i : Fin 320), ↑i < 78 → y.regs i = x.regs i

Fifteen actual arithmetic/copy/store instructions write the five original header words. All metadata below register 78, including the complete producer bank, is preserved.