Direct work-symbol branch combinator -- proof internals

def Complexity.TM.workBranchBlankWrap {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (c : Cfg n onBlank.Q) : Cfg n (branchWorkBlankTM idx onBlank onNonblank).Q

Embed a blank-branch configuration into the combined controller.

Equations

• Complexity.TM.workBranchBlankWrap idx onBlank onNonblank c = { state := onBlank.workBranchBlankState onNonblank c.state, input := c.input, work := c.work, output := c.output }

def Complexity.TM.workBranchNonblankWrap {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (c : Cfg n onNonblank.Q) : Cfg n (branchWorkBlankTM idx onBlank onNonblank).Q

Embed a nonblank-branch configuration into the combined controller.

Equations

• Complexity.TM.workBranchNonblankWrap idx onBlank onNonblank c = { state := onBlank.workBranchNonblankState onNonblank c.state, input := c.input, work := c.work, output := c.output }

theorem Complexity.TM.workBranchBlankWrap_halted_iff_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (c : Cfg n onBlank.Q) : (branchWorkBlankTM idx onBlank onNonblank).halted (workBranchBlankWrap idx onBlank onNonblank c) ↔ onBlank.halted c

theorem Complexity.TM.workBranchNonblankWrap_halted_iff_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (c : Cfg n onNonblank.Q) : (branchWorkBlankTM idx onBlank onNonblank).halted (workBranchNonblankWrap idx onBlank onNonblank c) ↔ onNonblank.halted c

theorem Complexity.TM.branchWorkBlankTM_blank_step_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) {c c' : Cfg n onBlank.Q} (hstep : onBlank.step c = some c') : (branchWorkBlankTM idx onBlank onNonblank).step (workBranchBlankWrap idx onBlank onNonblank c) = some (workBranchBlankWrap idx onBlank onNonblank c')

theorem Complexity.TM.branchWorkBlankTM_nonblank_step_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) {c c' : Cfg n onNonblank.Q} (hstep : onNonblank.step c = some c') : (branchWorkBlankTM idx onBlank onNonblank).step (workBranchNonblankWrap idx onBlank onNonblank c) = some (workBranchNonblankWrap idx onBlank onNonblank c')

theorem Complexity.TM.branchWorkBlankTM_blank_reachesIn_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) {t : ℕ} {c c' : Cfg n onBlank.Q} (hreach : onBlank.reachesIn t c c') : (branchWorkBlankTM idx onBlank onNonblank).reachesIn t (workBranchBlankWrap idx onBlank onNonblank c) (workBranchBlankWrap idx onBlank onNonblank c')

theorem Complexity.TM.branchWorkBlankTM_nonblank_reachesIn_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) {t : ℕ} {c c' : Cfg n onNonblank.Q} (hreach : onNonblank.reachesIn t c c') : (branchWorkBlankTM idx onBlank onNonblank).reachesIn t (workBranchNonblankWrap idx onBlank onNonblank c) (workBranchNonblankWrap idx onBlank onNonblank c')

theorem Complexity.TM.branchWorkBlankTM_dispatch_blank_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hblank : (work idx).read = Γ.blank) (hinp : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (hout : out.read ≠ Γ.start) : (branchWorkBlankTM idx onBlank onNonblank).step { state := (branchWorkBlankTM idx onBlank onNonblank).qstart, input := inp, work := work, output := out } = some (workBranchBlankWrap idx onBlank onNonblank { state := onBlank.qstart, input := inp, work := work, output := out })

theorem Complexity.TM.branchWorkBlankTM_dispatch_nonblank_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) (hnonblank : (work idx).read ≠ Γ.blank) (hinp : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (hout : out.read ≠ Γ.start) : (branchWorkBlankTM idx onBlank onNonblank).step { state := (branchWorkBlankTM idx onBlank onNonblank).qstart, input := inp, work := work, output := out } = some (workBranchNonblankWrap idx onBlank onNonblank { state := onNonblank.qstart, input := inp, work := work, output := out })

theorem Complexity.TM.branchWorkBlankTM_reachesIn_blank_frame_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {t : ℕ} {c' : Cfg n onBlank.Q} (hblank : (work idx).read = Γ.blank) (hinp : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (hout : out.read ≠ Γ.start) (hreach : onBlank.reachesIn t { state := onBlank.qstart, input := inp, work := work, output := out } c') (hhalt : onBlank.halted c') : ∃ (C : Cfg n (branchWorkBlankTM idx onBlank onNonblank).Q), (branchWorkBlankTM idx onBlank onNonblank).reachesIn (t + 1) { state := (branchWorkBlankTM idx onBlank onNonblank).qstart, input := inp, work := work, output := out } C ∧ (branchWorkBlankTM idx onBlank onNonblank).halted C ∧ C.input = c'.input ∧ C.work = c'.work ∧ C.output = c'.output

theorem Complexity.TM.branchWorkBlankTM_reachesIn_nonblank_frame_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) (inp : Tape) (work : Fin n → Tape) (out : Tape) {t : ℕ} {c' : Cfg n onNonblank.Q} (hnonblank : (work idx).read ≠ Γ.blank) (hinp : inp.read ≠ Γ.start) (hwork : ∀ (i : Fin n), (work i).read ≠ Γ.start) (hout : out.read ≠ Γ.start) (hreach : onNonblank.reachesIn t { state := onNonblank.qstart, input := inp, work := work, output := out } c') (hhalt : onNonblank.halted c') : ∃ (C : Cfg n (branchWorkBlankTM idx onBlank onNonblank).Q), (branchWorkBlankTM idx onBlank onNonblank).reachesIn (t + 1) { state := (branchWorkBlankTM idx onBlank onNonblank).qstart, input := inp, work := work, output := out } C ∧ (branchWorkBlankTM idx onBlank onNonblank).halted C ∧ C.input = c'.input ∧ C.work = c'.work ∧ C.output = c'.output

theorem Complexity.TM.branchWorkBlankTM_hoareTime_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) {pre blankPre nonblankPre blankPost nonblankPost : TapePred n} {blankTime nonblankTime : ℕ} (hframe : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → inp.read ≠ Γ.start ∧ (∀ (i : Fin n), (work i).read ≠ Γ.start) ∧ out.read ≠ Γ.start) (hblankPre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → (work idx).read = Γ.blank → blankPre inp work out) (hnonblankPre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → (work idx).read ≠ Γ.blank → nonblankPre inp work out) (hblank : onBlank.HoareTime blankPre blankPost blankTime) (hnonblank : onNonblank.HoareTime nonblankPre nonblankPost nonblankTime) : (branchWorkBlankTM idx onBlank onNonblank).HoareTime pre (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => blankPost inp work out ∨ nonblankPost inp work out) (branchWorkBlankTime blankTime nonblankTime)

theorem Complexity.TM.branchWorkBlankTM_hoareTimeSpace_internal {n : ℕ} (idx : Fin n) (onBlank onNonblank : TM n) {pre blankPre nonblankPre blankPost nonblankPost : TapePred n} {blankTime nonblankTime inputLength blankSpace nonblankSpace : ℕ} (hframe : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → inp.read ≠ Γ.start ∧ (∀ (i : Fin n), (work i).read ≠ Γ.start) ∧ out.read ≠ Γ.start) (hblankPre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → (work idx).read = Γ.blank → blankPre inp work out) (hnonblankPre : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), pre inp work out → (work idx).read ≠ Γ.blank → nonblankPre inp work out) (hblank : onBlank.HoareTimeSpace blankPre blankPost blankTime inputLength blankSpace) (hnonblank : onNonblank.HoareTimeSpace nonblankPre nonblankPost nonblankTime inputLength nonblankSpace) : (branchWorkBlankTM idx onBlank onNonblank).HoareTimeSpace pre (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => blankPost inp work out ∨ nonblankPost inp work out) (branchWorkBlankTime blankTime nonblankTime) inputLength (max blankSpace nonblankSpace)

theorem Complexity.TM.IsTransducer.branchWorkBlankTM_internal {n : ℕ} {idx : Fin n} {onBlank onNonblank : TM n} (hblank : onBlank.IsTransducer) (hnonblank : onNonblank.IsTransducer) : (branchWorkBlankTM idx onBlank onNonblank).IsTransducer

theorem Complexity.Tape.HasBinaryNat.read_eq_blank_iff_internal {t : Tape} {value : ℕ} (h : t.HasBinaryNat value) : t.read = Γ.blank ↔ value = 0

A canonical little-endian natural reads blank exactly at zero.