Retaining a charged prefix in counting computations

A tidy deterministic preparation restores the input head and blank work tapes after writing a prefix. Its singleton lift then runs the counting machine without changing any occurrence. Every preparation transition is included in the sum of the two native clocks.

Main results

• Turing.MultiTapeCTM.runList_prependOutput: unreadable output preserves all occurrences.
• Turing.MultiTapeCTM.runList_seq_prependOutput: retain a natively prepared prefix.
• Turing.MultiTapeCTM.haltsWithin_seq_prependOutput: charge preparation and computation.

References

The construction follows MultiTape.Probabilistic.OutputPrefix, adapted there from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8. The singleton lift here preserves exact multiplicity in addition to the output behavior.

theorem Turing.MultiTapeCTM.runList_prependOutput {k : ℕ} {Symbol State : Type} {input : List Symbol} (machine : MultiTapeCTM k Symbol State) (fuel : ℕ) (cfg : Cfg k Symbol State input) (pre : List Symbol) : machine.runList fuel (cfg.prependOutput pre) = List.map (fun (final : Cfg k Symbol State input) => final.prependOutput pre) (machine.runList fuel cfg)

Changing the unreadable output retains every subsequent configuration occurrence.

theorem Turing.MultiTapeCTM.HaltsWithin.prependOutput {k : ℕ} {Symbol State : Type} {input : List Symbol} {machine : MultiTapeCTM k Symbol State} (hnon : machine.Nonblocking) {fuel : ℕ} {cfg : Cfg k Symbol State input} (h : machine.HaltsWithin fuel cfg) (pre : List Symbol) : machine.HaltsWithin fuel (cfg.prependOutput pre)

A prefix changes no halting decision or clock, provided the transition table is nonblocking.

theorem Turing.MultiTapeCTM.runList_seq_prependOutput {k : ℕ} {Symbol State₀ State₁ : Type} (prepare : MultiTapeTM k Symbol State₀) (source : MultiTapeCTM k Symbol State₁) (hnon : source.Nonblocking) (input pre : List Symbol) (prepareTime runTime : ℕ) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) prepareTime = wordsCfg input none (fun (x : Fin k) => []) pre) (hsource : source.HaltsWithin runTime (MultiTapeMachine.initialConfig source input).tapes) : runList (MultiTapeMachine.seq (ofDeterministic prepare) source) (prepareTime + runTime) ((MultiTapeMachine.seq (ofDeterministic prepare) source).initialConfig input).tapes = List.map (fun (final : Cfg k Symbol State₁ input) => Cfg.mapState (Option.map Sum.inr) (final.prependOutput pre)) (source.runList runTime (MultiTapeMachine.initialConfig source input).tapes)

Workspace-restoring singleton preparation retains the prefix and every source occurrence.

theorem Turing.MultiTapeCTM.haltsWithin_seq_prependOutput {k : ℕ} {Symbol State₀ State₁ : Type} (prepare : MultiTapeTM k Symbol State₀) (source : MultiTapeCTM k Symbol State₁) (hnon : source.Nonblocking) (input pre : List Symbol) (prepareTime runTime : ℕ) (hprepare : MultiTapeTM.runFrom (prepare.initCfg input) prepareTime = wordsCfg input none (fun (x : Fin k) => []) pre) (hsource : source.HaltsWithin runTime (MultiTapeMachine.initialConfig source input).tapes) : HaltsWithin (MultiTapeMachine.seq (ofDeterministic prepare) source) (prepareTime + runTime) ((MultiTapeMachine.seq (ofDeterministic prepare) source).initialConfig input).tapes

The actual prepared-prefix machine halts within the sum of the two charged clocks.