One-token simulation for the Tseitin streaming controller

This module composes the two concrete input-reading steps with the scheduled register child, when any, and relates the result to one successful Streaming.step. The endpoint is again a first-bit read configuration, its input is advanced by exactly two cells, and its tapes represent the new pure streaming state. Every successful token transition fits the common controllerTokenBudget under a bound on the six register values.

The theorem is framed over an arbitrary tape-carrying configuration so that a later induction over Streaming.run can instantiate it directly.

Main result

• validEmitterTM_streaming_step_internal

theorem Complexity.SAT.ThreeSAT.Machine.parked_move_right_internal {input : Tape} (h : TM.Parked input) : TM.Parked (input.move Dir3.right)

Moving a parked input tape right preserves parkedness.

theorem Complexity.SAT.ThreeSAT.Machine.validEmitterTM_streaming_step_internal {Q : Type} {st st' : Streaming.State} (tok : EncToken) (cap : ℕ) (c : Cfg workTapeCount Q) (hstep : Streaming.step st tok = some st') (hpre : StreamingStatePred c.input st c.input c.work c.output) (hinput : InputTokenAt c.input tok) (hinp : TM.Parked c.input) (hbound : (BufferValues.ofStreaming st).BoundedBy cap) : ∃ (c' : Cfg workTapeCount validEmitterTM.Q), ∃ t ≤ controllerTokenBudget cap, validEmitterTM.reachesIn t (controllerReadCfg (StreamMode.ofState st) c) c' ∧ ControllerReadPred (StreamMode.ofState st') (StreamingStatePred ((c.input.move Dir3.right).move Dir3.right) st') c'

Simulate one successful pure token transition. The final StreamingStatePred fixes the input to the original input moved right twice, so it also records exact input-head and input-cell framing.