Finite composition of proof-carrying binary routines

Fixed machine-dependent state, symbol, tape, and transition-case phases can be unrolled into ordinary lists. This module proves their composition sound once, leaving only genuinely input-dependent ranges to the binary loop adapter.

theorem Complexity.BinaryRoutine.seqList_sound {n : ℕ} (routines : List (BinaryRoutine n)) (hsound : ∀ routine ∈ routines, routine.Sound) : (seqList routines).Sound

A fixed list of sound routines composes to a sound routine.

theorem Complexity.BinaryRoutine.repeatRoutine_sound {n : ℕ} (count : ℕ) (routine : BinaryRoutine n) (hsound : routine.Sound) : (repeatRoutine count routine).Sound

Fixed finite repetition preserves routine soundness.

theorem Complexity.BinaryRoutine.seqList_append_effect {n : ℕ} (first second : List (BinaryRoutine n)) (values : BinaryValues n) : (seqList (first ++ second)).effect values = (seqList second).effect ((seqList first).effect values)

Sequential-list effects distribute over list append.

theorem Complexity.BinaryRoutine.seqList_ofFn_effect_eq_trajectory {n : ℕ} (count : ℕ) (routineAt : Fin count → BinaryRoutine n) (initial : BinaryValues n) (trajectory : ℕ → BinaryValues n) (hzero : trajectory 0 = initial) (hstep : ∀ (index : Fin count), (routineAt index).effect (trajectory ↑index) = trajectory (↑index + 1)) : (seqList (List.ofFn routineAt)).effect initial = trajectory count

The effect of a finite routine family follows any supplied one-step trajectory from its stated initial value to the family endpoint.