Backward public-input copy -- proof internals

theorem Complexity.RAM.TMConfig.Sparse.marshalLoopOps_control_internal (n : ℕ) (store : Structured.Store) (hcursor : 0 < store stateReg) (hzero : store (zeroReg n) = 0) : have final := Structured.Basic.execList (marshalLoopOps n) store; final stateReg = store stateReg - 1 ∧ final (zeroReg n) = 0 ∧ final (oneReg n) = 1 ∧ final (tapeCountReg n) = n + 2 ∧ final (stateScratchReg n) = cellBase n ∧ 0 < final (cellReg n (inputTape n) (store stateReg))

The backward-copy body always decrements its cursor and restores all four loop constants, even when the cursor itself visits one of their registers.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoopOps_exec_internal (n : ℕ) (store : Structured.Store) : ∃ (cost : ℕ) (space : ℕ), Structured.Exec (Structured.Cmd.basics (marshalLoopOps n)) store (Structured.Basic.execList (marshalLoopOps n) store) (marshalLoopOps n).length cost space

One backward-copy body has an exact structured execution.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoopOps_data_internal (n : ℕ) (store : Structured.Store) (reg : ℕ) (hcursor : 0 < store stateReg) (hzero : store (zeroReg n) = 0) (hfree : store stateReg ∉ captureRegs n) (hdata : cellBase n ≤ reg) : Structured.Basic.execList (marshalLoopOps n) store reg = Function.update (Function.update store (store stateReg) 0) (cellReg n (inputTape n) (store stateReg)) (store (store stateReg) + 1) reg

Away from the six captured scratch positions, one loop body clears the raw source cell and writes its Boolean value, shifted to the sparse symbol code, to the corresponding input cell. This is the relocation induction step.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoopOps_of_ne_internal (n : ℕ) (store : Structured.Store) (reg : ℕ) (hcursor : 0 < store stateReg) (hzero : store (zeroReg n) = 0) (hstate : reg ≠ stateReg) (hfree : reg ∉ captureRegs n) (hsource : reg ≠ store stateReg) (hdestination : reg ≠ cellReg n (inputTape n) (store stateReg)) : Structured.Basic.execList (marshalLoopOps n) store reg = store reg

Apart from the raw source, sparse destination, state, and six scratch registers, a loop body preserves every register. This form does not assume that the cursor avoids scratch, so it carries both future raw sources and previously relocated cells across captured iterations.

theorem Complexity.RAM.TMConfig.Sparse.marshalLoop_exec_internal (n cursor : ℕ) (store : Structured.Store) (hcursor : store stateReg = cursor) (hzero : store (zeroReg n) = 0) (hone : store (oneReg n) = 1) (hcount : store (tapeCountReg n) = n + 2) (hbase : store (stateScratchReg n) = cellBase n) : ∃ (final : Structured.Store) (cost : ℕ) (space : ℕ), Structured.Exec (marshalLoop n) store final (marshalLoopSteps n cursor) cost space ∧ final stateReg = 0 ∧ final (zeroReg n) = 0 ∧ final (oneReg n) = 1 ∧ final (tapeCountReg n) = n + 2 ∧ final (stateScratchReg n) = cellBase n

The backward-copy loop executes exactly once per raw input cell and exits with cursor zero and all constants restored.