Count-preserving buffered machine composition

The shared compiler redirects each source output symbol to a work tape in the same transition. The singleton deterministic lift rewinds that buffer and marks its boundary in the word length plus four transitions. The consumer then reads the buffered word with separate blank work tapes. Source scratch and the real input head are retained; preparation introduces exactly one path.

The complete compiler is closed, with no oracle channels. Its native occurrence counts compose by List bind, and its all-branches clock is T₀ + (T₀ + 4 + T₁) from initialized tapes. The initial output is empty here; the general output-growth lemma retains its initial length.

Main definitions

• Turing.MultiTapeCTM.comp: feed one counting machine's output to another.

Main results

• Turing.MultiTapeCTM.runList_comp: the exact complete-configuration composition law.
• Turing.MultiTapeCTM.HaltsWithin.comp: the charged native all-branches clock.
• Turing.MultiTapeCTM.branchCount_comp: exact native counts through buffered composition.

References

The tape layout and native preparation are shared with MultiTape.Machine.Composition; that module records the original deterministic and probabilistic compiler sources.

theorem Turing.MultiTapeCTM.Nonblocking.outputToTape {k : ℕ} {Symbol State : Type} {machine : MultiTapeCTM k Symbol State} (h : machine.Nonblocking) : Nonblocking (MultiTapeMachine.outputToTape machine)

Output redirection does not introduce empty transition lists.

theorem Turing.MultiTapeCTM.Nonblocking.inputFromTape {k : ℕ} {Symbol State : Type} {machine : MultiTapeCTM k Symbol State} (h : machine.Nonblocking) : Nonblocking (MultiTapeMachine.inputFromTape machine)

Virtual input redirection does not introduce empty transition lists.

noncomputable def Turing.MultiTapeCTM.Composition.continuation {k₁ : ℕ} {Symbol State₁ : Type} (machine : MultiTapeCTM k₁ Symbol State₁) (k₀ : ℕ) (mark : Symbol) : MultiTapeCTM (k₁ + k₀ + 2) Symbol ((MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁)

Rewind and mark the buffered word with exactly one path, then start the consumer.

theorem Turing.MultiTapeCTM.Composition.runList_source {k₀ : ℕ} {Symbol State₀ : Type} (machine : MultiTapeCTM k₀ Symbol State₀) (k₁ fuel : ℕ) (input : List Symbol) : runList (MultiTapeMachine.Composition.source machine k₁) fuel ((MultiTapeMachine.Composition.source machine k₁).initialConfig input).tapes = List.map (fun (cfg : Cfg k₀ Symbol State₀ input) => (MultiTapeMachine.Composition.buffer k₁ (MultiTapeMachine.Config.emptyOracleEquiv.symm cfg)).tapes) (machine.runList fuel (MultiTapeMachine.initialConfig machine input).tapes)

Source buffering preserves every configuration occurrence.

theorem Turing.MultiTapeCTM.Composition.runList_consumer {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapeCTM k₁ Symbol State₁) (mark : Symbol) (cfg₀ : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (cfg₁ : MultiTapeMachine.Config k₁ Symbol State₁ Empty cfg₀.tapes.output) (fuel : ℕ) : runList (MultiTapeMachine.Composition.consumer machine k₀) fuel (MultiTapeMachine.Composition.consumerConfig mark cfg₀ cfg₁).tapes = List.map (fun (cfg : Cfg k₁ Symbol State₁ cfg₀.tapes.output) => (MultiTapeMachine.Composition.consumerConfig mark cfg₀ (MultiTapeMachine.Config.emptyOracleEquiv.symm cfg)).tapes) (machine.runList fuel cfg₁.tapes)

The consumer keeps every source scratch cell and every continuation occurrence.

theorem Turing.MultiTapeCTM.Composition.nonblocking_source {k₀ : ℕ} {Symbol State₀ : Type} {machine : MultiTapeCTM k₀ Symbol State₀} (h : machine.Nonblocking) (k₁ : ℕ) : Nonblocking (MultiTapeMachine.Composition.source machine k₁)

Buffering the source preserves the explicit no-stuck table condition.

theorem Turing.MultiTapeCTM.Composition.nonblocking_consumer {k₁ : ℕ} {Symbol State₁ : Type} {machine : MultiTapeCTM k₁ Symbol State₁} (h : machine.Nonblocking) (k₀ : ℕ) : Nonblocking (MultiTapeMachine.Composition.consumer machine k₀)

The virtual-input consumer preserves the explicit no-stuck table condition.

theorem Turing.MultiTapeCTM.Composition.nonblocking_continuation {k₁ : ℕ} {Symbol State₁ : Type} {machine : MultiTapeCTM k₁ Symbol State₁} (h : machine.Nonblocking) (k₀ : ℕ) (mark : Symbol) : (continuation machine k₀ mark).Nonblocking

Singleton preparation and a nonblocking consumer have no stuck local views.

theorem Turing.MultiTapeCTM.Composition.haltsWithin_consumer {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} {machine : MultiTapeCTM k₁ Symbol State₁} (hnon : machine.Nonblocking) (mark : Symbol) (cfg₀ : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (cfg₁ : MultiTapeMachine.Config k₁ Symbol State₁ Empty cfg₀.tapes.output) (fuel : ℕ) (h : machine.HaltsWithin fuel cfg₁.tapes) : HaltsWithin (MultiTapeMachine.Composition.consumer machine k₀) fuel (MultiTapeMachine.Composition.consumerConfig mark cfg₀ cfg₁).tapes

A native consumer clock survives the exact tape embedding.

theorem Turing.MultiTapeCTM.Composition.runList_continuation {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapeCTM k₁ Symbol State₁) (hnon : machine.Nonblocking) (mark : Symbol) (cfg : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (prepareTime runTime : ℕ) (hprepare : cfg.tapes.output.length + 4 ≤ prepareTime) (hrun : machine.HaltsWithin runTime (MultiTapeMachine.initialConfig machine cfg.tapes.output).tapes) : (continuation machine k₀ mark).runList (prepareTime + runTime) (MultiTapeMachine.Sequential.start (continuation machine k₀ mark) (MultiTapeMachine.Composition.buffer k₁ cfg)).tapes = List.map (fun (final : Cfg k₁ Symbol State₁ cfg.tapes.output) => (MultiTapeMachine.Sequential.right (MultiTapeMachine.Composition.consumerConfig mark cfg (MultiTapeMachine.Config.emptyOracleEquiv.symm final))).tapes) (machine.runList runTime (MultiTapeMachine.initialConfig machine cfg.tapes.output).tapes)

The charged handoff has one path and then preserves the consumer's complete configuration.

theorem Turing.MultiTapeCTM.Composition.haltsWithin_continuation {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {input : List Symbol} (machine : MultiTapeCTM k₁ Symbol State₁) (hnon : machine.Nonblocking) (mark : Symbol) (cfg : MultiTapeMachine.Config k₀ Symbol State₀ Empty input) (prepareTime runTime : ℕ) (hprepare : cfg.tapes.output.length + 4 ≤ prepareTime) (hrun : machine.HaltsWithin runTime (MultiTapeMachine.initialConfig machine cfg.tapes.output).tapes) : (continuation machine k₀ mark).HaltsWithin (prepareTime + runTime) (MultiTapeMachine.Sequential.start (continuation machine k₀ mark) (MultiTapeMachine.Composition.buffer k₁ cfg)).tapes

The singleton handoff and consumer halt natively within the charged combined bound.

noncomputable def Turing.MultiTapeCTM.comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (second : MultiTapeCTM k₁ Symbol State₁) (first : MultiTapeCTM k₀ Symbol State₀) (mark : Symbol) : MultiTapeCTM (k₁ + k₀ + 2) Symbol (State₀ ⊕ (MultiTapeTM.MarkWorkState ⊕ MultiTapeTM.RewindWorkState) ⊕ State₁)

Feed first's output to second, with distinct work tapes and a singleton charged handoff.

theorem Turing.MultiTapeCTM.Nonblocking.comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} {first : MultiTapeCTM k₀ Symbol State₀} {second : MultiTapeCTM k₁ Symbol State₁} (hfirst : first.Nonblocking) (hsecond : second.Nonblocking) (mark : Symbol) : (second.comp first mark).Nonblocking

Buffered composition has no stuck views when both component tables are nonblocking.

theorem Turing.MultiTapeCTM.runList_comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeCTM k₀ Symbol State₀) (second : MultiTapeCTM k₁ Symbol State₁) (hnonfirst : first.Nonblocking) (hnonsecond : second.Nonblocking) (mark : Symbol) (input : List Symbol) (firstTime secondTime : ℕ) (hfirst : first.HaltsWithin firstTime (MultiTapeMachine.initialConfig first input).tapes) (hsecond : ∀ result ∈ first.runList firstTime (MultiTapeMachine.initialConfig first input).tapes, second.HaltsWithin secondTime (MultiTapeMachine.initialConfig second result.output).tapes) : (second.comp first mark).runList (firstTime + (firstTime + 4 + secondTime)) (MultiTapeMachine.initialConfig (second.comp first mark) input).tapes = List.flatMap (fun (result : Cfg k₀ Symbol State₀ input) => List.map (fun (final : Cfg k₁ Symbol State₁ (MultiTapeMachine.Config.emptyOracleEquiv.symm result).tapes.output) => (MultiTapeMachine.Composition.finalConfig mark (MultiTapeMachine.Config.emptyOracleEquiv.symm result) (MultiTapeMachine.Config.emptyOracleEquiv.symm final)).tapes) (second.runList secondTime (MultiTapeMachine.initialConfig second result.output).tapes)) (first.runList firstTime (MultiTapeMachine.initialConfig first input).tapes)

Exact full-configuration composition, including scratch and input-head preservation. Both machines start with empty output. Each source instruction emits at most one symbol, so preparation takes at most firstTime + 4; it is not a free conversion between machine models.

theorem Turing.MultiTapeCTM.HaltsWithin.comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeCTM k₀ Symbol State₀) (second : MultiTapeCTM k₁ Symbol State₁) (hnonfirst : first.Nonblocking) (hnonsecond : second.Nonblocking) (mark : Symbol) (input : List Symbol) (firstTime secondTime : ℕ) (hfirst : first.HaltsWithin firstTime (MultiTapeMachine.initialConfig first input).tapes) (hsecond : ∀ result ∈ first.runList firstTime (MultiTapeMachine.initialConfig first input).tapes, second.HaltsWithin secondTime (MultiTapeMachine.initialConfig second result.output).tapes) : (second.comp first mark).HaltsWithin (firstTime + (firstTime + 4 + secondTime)) (MultiTapeMachine.initialConfig (second.comp first mark) input).tapes

The compiled machine halts on every native branch within the charged combined clock.

theorem Turing.MultiTapeCTM.branchCount_comp {k₀ k₁ : ℕ} {Symbol State₀ State₁ : Type} (first : MultiTapeCTM k₀ Symbol State₀) (second : MultiTapeCTM k₁ Symbol State₁) (hnonfirst : first.Nonblocking) (hnonsecond : second.Nonblocking) (mark : Symbol) (input : List Symbol) (firstTime secondTime : ℕ) (hfirst : first.HaltsWithin firstTime (MultiTapeMachine.initialConfig first input).tapes) (hsecond : ∀ result ∈ first.runList firstTime (MultiTapeMachine.initialConfig first input).tapes, second.HaltsWithin secondTime (MultiTapeMachine.initialConfig second result.output).tapes) (verdict : List Symbol → Bool) : (second.comp first mark).branchCount verdict (firstTime + (firstTime + 4 + secondTime)) (MultiTapeMachine.initialConfig (second.comp first mark) input).tapes = (List.map (fun (result : Cfg k₀ Symbol State₀ input) => second.branchCount verdict secondTime (MultiTapeMachine.initialConfig second result.output).tapes) (first.runList firstTime (MultiTapeMachine.initialConfig first input).tapes)).sum

Native terminal counts compose by summing the consumer count once per source occurrence. The sum is over a List, so duplicate source configurations retain their exact multiplicity.