Capturing raw-input scratch bits in finite control -- proof internals

theorem Complexity.RAM.TMConfig.Sparse.initRegs_bool_of_pos_internal (x : List Bool) {reg : ℕ} (hpos : 0 < reg) : initRegs x reg = 0 ∨ initRegs x reg = 1

theorem Complexity.RAM.TMConfig.Sparse.captureRegs_positive_internal (n : ℕ) {reg : ℕ} (hmem : reg ∈ captureRegs n) : 0 < reg

theorem Complexity.RAM.TMConfig.Sparse.captureInput_exec_of_leaf_internal {n : ℕ} (tm : TM n) (store : Structured.Store) (regs : List ℕ) (captured : List (ℕ × ℕ)) {final : Structured.Store} (hbits : ∀ reg ∈ regs, store reg = 0 ∨ store reg = 1) (hleaf : ∃ (steps : ℕ) (cost : ℕ) (space : ℕ), Structured.Exec (marshalLeaf tm (captureValues store regs captured)) store final steps cost space) : ∃ (steps : ℕ) (cost : ℕ) (space : ℕ), Structured.Exec (captureInput tm regs captured) store final steps cost space

If the selected leaf executes, the generated capture tree executes that same leaf without changing the store. Branch costs are left existential here; the later resource layer assigns their common envelope.

theorem Complexity.RAM.TMConfig.Sparse.marshalInput_exec_of_leaf_internal {n : ℕ} (tm : TM n) (x : List Bool) {final : Structured.Store} (hleaf : ∃ (steps : ℕ) (cost : ℕ) (space : ℕ), Structured.Exec (marshalLeaf tm (captureValues (initRegs x) (captureRegs n) [])) (initRegs x) final steps cost space) : ∃ (steps : ℕ) (cost : ℕ) (space : ℕ), Structured.Exec (marshalInput tm) (initRegs x) final steps cost space

Specialization of finite capture to the public RAM input store.