Regularly padded deterministic unrolling families -- proof internals

The padding proof separates three facts: the direct tableau fits its closed cubic budget, constant gates remain topological at every later frontier, and the terminal copy reads the original acceptance wire through the dead padding.

theorem Complexity.TM.directUnrollingRawCircuit_length_le_gateBound_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : List.length (tm.directUnrollingRawCircuit f n) ≤ tm.directUnrollingGateBound f n

theorem Complexity.TM.paddedDirectUnrollingRawCircuit_length_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : List.length (tm.paddedDirectUnrollingRawCircuit f n) = tm.directUnrollingGateBound f n + 1

theorem Complexity.TM.paddedDirectUnrollingRawCircuit_wellFormed_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : CircuitCode.RawCircuit.WellFormed n (tm.paddedDirectUnrollingRawCircuit f n)

theorem Complexity.TM.paddedDirectUnrollingRawCircuit_eval?_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] (x : BitString n) : (tm.paddedDirectUnrollingRawCircuit f n).eval? x.toList = some (CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f n) x fun (x : Fin (f n)) => false)