Function composition: first-phase boundary

This module runs the first function machine with its output redirected to the raw-output work tape, places that run in the composite layout, and exposes the exact tape facts required by the normalization tail.

theorem Complexity.TM.compositionFirstTM_boundary_internal {nf : ℕ} (tmF : TM nf) (ng : ℕ) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : tmF.ComputesInTime f T) (x : List Bool) : ∃ (C : Cfg (compositionTapeCount nf ng) (tmF.compositionFirstTM ng).Q), ∃ t ≤ T x.length, (tmF.compositionFirstTM ng).reachesIn t ((tmF.compositionFirstTM ng).initCfg x) C ∧ (tmF.compositionFirstTM ng).halted C ∧ (transitionTape (C.work (compositionRawOutputIdx nf ng))).HasOutput (f x) ∧ (transitionTape (C.work (compositionRawOutputIdx nf ng))).head ≤ t + 1 ∧ transitionTape (C.work (compositionVirtualInputIdx nf ng)) = (Tape.init []).move Dir3.right ∧ (∀ (j : Fin ng), transitionTape (C.work (compositionSecondWorkIdx nf ng j)) = (Tape.init []).move Dir3.right) ∧ (transitionInput C.input).StartInvariant ∧ 1 ≤ (transitionInput C.input).head ∧ (∀ (i : Fin (compositionTapeCount nf ng)), (transitionTape (C.work i)).StartInvariant ∧ 1 ≤ (transitionTape (C.work i)).head) ∧ transitionTape C.output = (Tape.init []).move Dir3.right

The first computation reaches a halted composite-layout boundary within its original time bound. The raw output remains readable, the destination for the canonical virtual input is still fresh, and every seam tape is parked in a start-invariant state.