Direct work-symbol branch combinator #
This module exposes exact framed execution for a one-step branch on an arbitrary work-tape symbol. It is the direct controller primitive used to branch on the readable sparse-entry equality flag.
theorem
Complexity.TM.branchWorkSymbolTM_reachesIn_equal_frame
{n : ℕ}
(idx : Fin n)
(symbol : Γ)
(onEqual onDifferent : TM n)
(inp : Tape)
(work : Fin n → Tape)
(out : Tape)
{t : ℕ}
{c' : Cfg n onEqual.Q}
(hequal : (work idx).read = symbol)
(hinp : inp.read ≠ Γ.start)
(hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start)
(hout : out.read ≠ Γ.start)
(hreach : onEqual.reachesIn t { state := onEqual.qstart, input := inp, work := work, output := out } c')
(hhalt : onEqual.halted c')
:
∃ (C : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q),
(branchWorkSymbolTM idx symbol onEqual onDifferent).reachesIn (t + 1)
{ state := (branchWorkSymbolTM idx symbol onEqual onDifferent).qstart, input := inp, work := work, output := out }
C ∧ (branchWorkSymbolTM idx symbol onEqual onDifferent).halted C ∧ C.input = c'.input ∧ C.work = c'.work ∧ C.output = c'.output
Exact framed execution through the symbol-equal branch.
theorem
Complexity.TM.branchWorkSymbolTM_reachesIn_different_frame
{n : ℕ}
(idx : Fin n)
(symbol : Γ)
(onEqual onDifferent : TM n)
(inp : Tape)
(work : Fin n → Tape)
(out : Tape)
{t : ℕ}
{c' : Cfg n onDifferent.Q}
(hdifferent : (work idx).read ≠ symbol)
(hinp : inp.read ≠ Γ.start)
(hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start)
(hout : out.read ≠ Γ.start)
(hreach : onDifferent.reachesIn t { state := onDifferent.qstart, input := inp, work := work, output := out } c')
(hhalt : onDifferent.halted c')
:
∃ (C : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q),
(branchWorkSymbolTM idx symbol onEqual onDifferent).reachesIn (t + 1)
{ state := (branchWorkSymbolTM idx symbol onEqual onDifferent).qstart, input := inp, work := work, output := out }
C ∧ (branchWorkSymbolTM idx symbol onEqual onDifferent).halted C ∧ C.input = c'.input ∧ C.work = c'.work ∧ C.output = c'.output
Exact framed execution through the symbol-different branch.
theorem
Complexity.TM.IsTransducer.branchWorkSymbolTM
{n : ℕ}
{idx : Fin n}
{symbol : Γ}
{onEqual onDifferent : TM n}
(hequal : onEqual.IsTransducer)
(hdifferent : onDifferent.IsTransducer)
:
(TM.branchWorkSymbolTM idx symbol onEqual onDifferent).IsTransducer
A direct work-symbol branch is a transducer when both selected branches are transducers.
theorem
Complexity.TM.branchWorkSymbolTM_prefix_withinAuxSpace
{n : ℕ}
(idx : Fin n)
(symbol : Γ)
(onEqual onDifferent : TM n)
(branchTime inputLength initialSpace time : ℕ)
(start current : Cfg n (branchWorkSymbolTM idx symbol onEqual onDifferent).Q)
(hinitial : start.WithinAuxSpace inputLength initialSpace)
(hreach : (branchWorkSymbolTM idx symbol onEqual onDifferent).reachesIn time start current)
(htime : time ≤ branchTime + 1)
:
current.WithinAuxSpace inputLength (initialSpace + branchTime + 1)
Coarse all-prefix auxiliary-space envelope for a direct work-symbol branch.