Linear witness-bound setup: proof internals

The concrete setup initializes the heads, records the input length in unary, and increments that counter. Its explicit time also gives a conservative all-prefix decision-space bound; no setup resource is treated as free.

theorem Complexity.WitnessBoundSetup.linearMachine_prepares_internal (x : List Bool) : linearMachine.HoareTime (fresh x) (ready x (x.length + 1)) (4 * x.length + 11)

The concrete linear setup has a canonical endpoint and explicit linear time.

theorem Complexity.WitnessBoundSetup.linearMachine_withinSpace_internal (x : List Bool) : linearMachine.HoareSafety (fresh x) fun (inp : Tape) (work : Fin 1 → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace x.length (4 * x.length + 11)

The setup's actual running time bounds every charged head on every prefix.