Run simulation for the Tseitin streaming controller #
This module iterates the one-token controller simulation over a successful
Streaming.run. The input is framed by an already-consumed token prefix and
the remaining token list. Every iteration advances that prefix by one token,
preserves the pure-state tape invariant, and consumes at most one
controllerTokenBudget.
The hypothesis st.maxValue + toks.length ≤ cap supplies one common register
cap for the whole suffix. Streaming.maxValue_step_le_internal reestablishes
the hypothesis after the head token. The endpoint remains in first-bit read
mode on the trailing blank; taking the final halt step is intentionally left
to the next layer.
Main result #
theorem
Complexity.SAT.ThreeSAT.Machine.validEmitterTM_streaming_run_internal
{Q : Type}
{st st' : Streaming.State}
(pre toks : List EncToken)
(cap : ℕ)
(c : Cfg workTapeCount Q)
(hrun : Streaming.run st toks = some st')
(hinput : c.input = framedTokenInput pre toks)
(hpre : StreamingStatePred c.input st c.input c.work c.output)
(hcap : st.maxValue + toks.length ≤ cap)
:
∃ (c' : Cfg workTapeCount validEmitterTM.Q),
∃ t ≤ toks.length * controllerTokenBudget cap,
validEmitterTM.reachesIn t (controllerReadCfg (StreamMode.ofState st) c) c' ∧ ControllerReadPred (StreamMode.ofState st') (StreamingStatePred (framedTokenInput (pre ++ toks) []) st') c'
Simulate a successful pure streaming run over a framed token suffix.