is_Recursive_byTape from a computable decider

This file builds, from a total computable decider f : List T → Bool for a language L, an always-halting TM0 over Option (T ⊕ Γ) that leaves a designated acceptSym under the head exactly on the words of L, i.e. is_Recursive_byTape L.

The construction threads the Mathlib Code → TM2 → TM1 → TM0 translation chain, but unlike the .Dom-only bridge code_implies_isTM_direct, it tracks the final tape (not just halting), because acceptance is read off the head symbol.

SPIKE: Computable f → ToPartrec.Code with characterized output

Given f : List T → Bool computable, we produce a ToPartrec.Code bitCode with bitCode.eval [Encodable.encode w] = some [if f w then 1 else 0].

noncomputable def ByTapeFromComputable.bitFn {T : Type} [Primcodable T] (f : List T → Bool) : ℕ → ℕ

The unary ℕ → ℕ function: decode the input as a word and return the bit.

Equations

• ByTapeFromComputable.bitFn f n = if (Option.map f (Encodable.decode n)).getD false = true then 1 else 0

theorem ByTapeFromComputable.bitFn_encode {T : Type} [Primcodable T] (f : List T → Bool) (w : List T) : bitFn f (Encodable.encode w) = if f w = true then 1 else 0

theorem ByTapeFromComputable.computable_bitFn {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) : Computable (bitFn f)

theorem ByTapeFromComputable.partrec_bitFn {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) : Nat.Partrec' fun (v : List.Vector ℕ 1) => ↑(bitFn f) v.head

noncomputable def ByTapeFromComputable.bitCode₀ {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) : Turing.ToPartrec.Code

A ToPartrec.Code computing bitFn f (as a singleton output).

Equations

• ByTapeFromComputable.bitCode₀ f hf = ⋯.choose

theorem ByTapeFromComputable.bitCode₀_eval {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) (n : ℕ) : (bitCode₀ f hf).eval [n] = Part.some [bitFn f n]

Output shaping: bit → [] / [0]

Code.case Code.zero Code.nil maps [0] ↦ [0] (reject) and [1] ↦ [] (accept). Composed with bitCode₀, the full code outputs [] exactly when f w = true.

noncomputable def ByTapeFromComputable.deciderCode {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) : Turing.ToPartrec.Code

The full decider code on the encoded input. Outputs [] iff f w = true.

Equations

• ByTapeFromComputable.deciderCode f hf = (Turing.ToPartrec.Code.zero.case Turing.ToPartrec.Code.nil).comp (ByTapeFromComputable.bitCode₀ f hf)

theorem ByTapeFromComputable.deciderCode_eval {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) (w : List T) : (deciderCode f hf).eval [Encodable.encode w] = Part.some (if f w = true then [] else [0])

theorem ByTapeFromComputable.deciderCode_eval_dom {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) (w : List T) : ((deciderCode f hf).eval [Encodable.encode w]).Dom

TM2 final configuration

By PartrecToTM2.tr_eval, the TM2 machine reaches halt v where v is the output of the code.

noncomputable def ByTapeFromComputable.outWord {T : Type} (f : List T → Bool) (w : List T) : List ℕ

The output word of the decider code on w.

Equations

• ByTapeFromComputable.outWord f w = if f w = true then [] else [0]

theorem ByTapeFromComputable.composedCode_outWord {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) (w : List T) : (Langlib.TMCodeListEncode.composedCode (deciderCode f hf)).eval (Langlib.TMCodeListEncode.shiftedEncoding w) = Part.some (outWord f w)

The composed code (with list-encoding prefix) on shiftedEncoding w evaluates to outWord f w.

theorem ByTapeFromComputable.tm2_eval_halt_composed {T : Type} [Primcodable T] (f : List T → Bool) (hf : Computable f) (w : List T) : Turing.PartrecToTM2.halt (outWord f w) ∈ Turing.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init (Langlib.TMCodeListEncode.composedCode (deciderCode f hf)) (Langlib.TMCodeListEncode.shiftedEncoding w))

Generic chain tape descent (TM2 halt v → TM0 tape)

For any code c and input v such that the TM2 reaches halt v, the chain TM0 ChainTM0 reaches a configuration whose tape head is the embedded final-tape head. We track the full configuration via the Mathlib Respects relations.

@[reducible, inline]

abbrev ByTapeFromComputable.chainTM1Init (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')

The chain TM1 initial config (matches partrec_init_trCfg).

Equations

• One or more equations did not get rendered due to their size.

theorem ByTapeFromComputable.tm1_descent (c : Turing.ToPartrec.Code) (vIn vOut : List ℕ) (hhalt : Turing.PartrecToTM2.halt vOut ∈ Turing.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c vIn)) : ∃ (cfg₁ : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')), Turing.TM2to1.TrCfg (Turing.PartrecToTM2.halt vOut) cfg₁ ∧ cfg₁ ∈ Turing.eval (Turing.TM1.step ChainTM1) (chainTM1Init c vIn)

TM1 descent: the chain TM1 reaches some config with TrCfg (halt vOut) cfg₁, where vIn is the input and vOut the reached output.

theorem ByTapeFromComputable.tm0_descent (c : Turing.ToPartrec.Code) (v : List ℕ) (cfg₁ : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')) (hmem : cfg₁ ∈ Turing.eval (Turing.TM1.step ChainTM1) (chainTM1Init c v)) : Turing.TM1to0.trCfg ChainTM1 cfg₁ ∈ Turing.eval (Turing.TM0.step ChainTM0) (Turing.TM1to0.trCfg ChainTM1 (chainTM1Init c v))

TM0 descent: the chain TM0 reaches a config whose tape is the TM1 final tape, starting from TM1to0.trCfg ChainTM1 (chainTM1Init c v).

Tape-tracking eval lemmas for reroot / restrict / alphabet-lift

Each underlying Respects relation preserves the tape, so Turing.tr_eval transports a final config of known tape.

theorem ByTapeFromComputable.reroot_eval_tape {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (q₀ : Λ) (l : List Γ) (cf : Turing.TM0.Cfg Γ Λ) (hmem : cf ∈ Turing.eval (Turing.TM0.step M) { q := q₀, Tape := Turing.Tape.mk₁ l }) : ∃ (cf' : Turing.TM0.Cfg Γ (ParrecToTM0.Rooted Λ q₀)), cf'.Tape = cf.Tape ∧ cf' ∈ Turing.eval (Turing.TM0.step (ParrecToTM0.tm0Reroot M q₀)) (Turing.TM0.init l)

Re-rooted TM0: a final config with tape T is reached, given the original reaches a final config with tape T from ⟨q₀, Tape.mk₁ l⟩.

theorem ByTapeFromComputable.restrict_eval_tape {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hS : Turing.TM0.Supports M ↑S) (l : List Γ) (cf : Turing.TM0.Cfg Γ Λ) (hmem : cf ∈ Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)) : ∃ (cf' : Turing.TM0.Cfg Γ { q : Λ // q ∈ S }), cf'.Tape = cf.Tape ∧ cf' ∈ Turing.eval (Turing.TM0.step (Turing.TM0.restrict M S hS)) (Turing.TM0.init l)

Restricted TM0: tape-tracking version of restrict_eval_dom_iff.

theorem ByTapeFromComputable.restrictReroot_eval_tape {Γ : Type} [Inhabited Γ] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hS : Turing.TM0.Supports M ↑S) (q₀ : Λ) (hq₀ : q₀ ∈ S) (l : List Γ) (cf : Turing.TM0.Cfg Γ Λ) (hmem : cf ∈ Turing.eval (Turing.TM0.step M) { q := q₀, Tape := Turing.Tape.mk₁ l }) : ∃ (cf' : Turing.TM0.Cfg Γ { q : ParrecToTM0.Rooted Λ q₀ // q ∈ Finset.map ParrecToTM0.rootedEmbFn S }), cf'.Tape = cf.Tape ∧ cf' ∈ Turing.eval (Turing.TM0.step (ParrecToTM0.tm0RestrictReroot M S hS q₀ hq₀)) (Turing.TM0.init l)

Restrict+reroot TM0: tape-tracking version of tm0RestrictReroot_eval_dom.

theorem ByTapeFromComputable.lift_eval_tape {Γ Γ₂ : Type} [Inhabited Γ] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (emb : Γ → Γ₂) (inv : Γ₂ → Γ) (hemb : ∀ (a : Γ), inv (emb a) = a) (hemb_default : emb default = default) (l : List Γ) (cf : Turing.TM0.Cfg Γ Λ) (hmem : cf ∈ Turing.eval (Turing.TM0.step M) (Turing.TM0.init l)) : ∃ (cf' : Turing.TM0.Cfg Γ₂ Λ), cf'.Tape = Turing.Tape.map (TM0AlphabetSim.embPM emb hemb_default) cf.Tape ∧ cf' ∈ Turing.eval (Turing.TM0.step (TM0AlphabetSim.liftMachine M emb inv)) (Turing.TM0.init (List.map emb l))

Alphabet-lifted TM0: tape-tracking version of lift_eval_dom.

The final TM1 tape head for a halt v config

From TrCfg (halt v) cfg₁, the TM1 tape head is (true, L.head) where each stack component is the head of the reversed encoded stack.

theorem ByTapeFromComputable.trCfg_halt_head (v : List ℕ) (cfg₁ : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')) (htr : Turing.TM2to1.TrCfg (Turing.PartrecToTM2.halt v) cfg₁) : cfg₁.Tape.head = (true, fun (k : Turing.PartrecToTM2.K') => (List.map some (Turing.PartrecToTM2.K'.elim (Turing.PartrecToTM2.trList v) [] [] [] k)).reverse.headI)

theorem ByTapeFromComputable.trCfg_halt_head_accept (cfg₁ : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')) (htr : Turing.TM2to1.TrCfg (Turing.PartrecToTM2.halt []) cfg₁) : cfg₁.Tape.head = (true, fun (x : Turing.PartrecToTM2.K') => none)

The TM1 final tape head for the accepting output [].

theorem ByTapeFromComputable.trCfg_halt_head_reject (cfg₁ : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')) (htr : Turing.TM2to1.TrCfg (Turing.PartrecToTM2.halt [0]) cfg₁) : cfg₁.Tape.head.2 Turing.PartrecToTM2.K'.main = some Turing.PartrecToTM2.Γ'.cons

The TM1 final tape head for the rejecting output [0].

theorem ByTapeFromComputable.directBlankEmb_injective {T : Type} : Function.Injective directBlankEmb

directBlankEmb is injective (it has the left inverse directBlankInv).

noncomputable def ByTapeFromComputable.acceptSym {T : Type} : Option (T ⊕ ChainΓ)

The accepting symbol: the embedding of the accept TM1 head.

Equations

• ByTapeFromComputable.acceptSym = directBlankEmb (true, fun (x : Turing.PartrecToTM2.K') => none)

theorem ByTapeFromComputable.reject_head_ne_acceptSym {T : Type} (h : ChainΓ) (hh : h.2 Turing.PartrecToTM2.K'.main = some Turing.PartrecToTM2.Γ'.cons) : directBlankEmb h ≠ acceptSym

A reject head (whose main component is some cons) embeds to something different from acceptSym.

Chain TM0 with Fintype states and final tape

The analogue of code_to_tm0_fintype_general, but additionally producing the final tape (the embedded addBottom L head).

theorem ByTapeFromComputable.code_to_tm0_tape (c : Turing.ToPartrec.Code) : ∃ (ΛTy : Type) (x : Inhabited ΛTy) (x_1 : Fintype ΛTy) (M : Turing.TM0.Machine ChainΓ ΛTy), ∀ (vIn vOut : List ℕ), Turing.PartrecToTM2.halt vOut ∈ Turing.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c vIn) → ∃ cf ∈ Turing.eval (Turing.TM0.step M) (Turing.TM0.init (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList vIn))), ∀ (cfg₁ : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')), Turing.TM2to1.TrCfg (Turing.PartrecToTM2.halt vOut) cfg₁ → cfg₁ ∈ Turing.eval (Turing.TM1.step ChainTM1) (chainTM1Init c vIn) → cf.Tape = cfg₁.Tape

Final assembly

noncomputable def ByTapeFromComputable.chainInput {T : Type} [Primcodable T] (w : List T) : List ChainΓ

The chain input tape (over ChainΓ) for word w.

Equations

• ByTapeFromComputable.chainInput w = Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList (Langlib.TMCodeListEncode.shiftedEncoding w))

theorem ByTapeFromComputable.is_Recursive_byTape_of_computable_decide {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] (L : Language T) (f : List T → Bool) (hf : Computable f) (hL : ∀ (w : List T), w ∈ L ↔ f w = true) : is_Recursive_byTape L

is_Recursive_byTape from a computable decider.

The assembled TM0 over Option (T ⊕ ChainΓ) is compose M_conv (directEmbedTM0 M), where M_conv writes the chain input from w, M is the chain decider, and the alphabet is lifted via directBlankEmb. It always halts and its final head is acceptSym exactly on words of L.

theorem is_Recursive_byTape_of_computable_decide {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] (L : Language T) (f : List T → Bool) (hf : Computable f) (hL : ∀ (w : List T), w ∈ L ↔ f w = true) : is_Recursive_byTape L

is_Recursive_byTape from a computable decider (top-level form).

theorem is_Recursive_of_computable_decide {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] (L : Language T) (f : List T → Bool) (hf : Computable f) (hL : ∀ (w : List T), w ∈ L ↔ f w = true) : is_Recursive L

A total computable Boolean decision procedure yields a recursive language. Combining the tape-output decider construction with the tape-vs-state acceptance equivalence is_Recursive_of_byTape.