Direct ToPartrec.Code → TM Recognition

This file proves the direct bridge from a semideciding ToPartrec.Code to is_TM. It composes the user code with listEncodeCode, so the Partrec chain runs on a variable-length List ℕ input representing the encoded word. The tape-level part realizes the finite per-symbol conversion from the input alphabet to the shifted chain fragments used by shiftedEncoding.

Key results

• shifted_converter_exists: realizes the finite per-symbol conversion.
• directEmbedTM0_eval_dom: alphabet lifting preserves the embedded TM0's halting domain.
• code_implies_isTM_direct: a ToPartrec.Code recognizing a language gives is_TM for that language.

Blank-preserving embedding

noncomputable def directBlankEmb {T Γ₀ : Type} [DecidableEq Γ₀] [Inhabited Γ₀] (γ : Γ₀) : Option (T ⊕ Γ₀)

Equations

• directBlankEmb γ = if γ = default then none else some (Sum.inr γ)

noncomputable def directBlankInv {T Γ₀ : Type} [Inhabited Γ₀] (a : Option (T ⊕ Γ₀)) : Γ₀

Equations

• directBlankInv (some (Sum.inr γ)) = γ
• directBlankInv a = default

theorem directBlankEmb_default {T Γ₀ : Type} [DecidableEq Γ₀] [Inhabited Γ₀] : directBlankEmb default = default

theorem directBlankInv_emb {T Γ₀ : Type} [DecidableEq Γ₀] [Inhabited Γ₀] (γ : Γ₀) : directBlankInv (directBlankEmb γ) = γ

theorem directBlankEmb_ne_default {T Γ₀ : Type} [DecidableEq Γ₀] [Inhabited Γ₀] (γ : Γ₀) (hγ : γ ≠ default) : directBlankEmb γ = some (Sum.inr γ)

Direct shifted tape construction

noncomputable def directChainCons : ChainΓ

Equations

• directChainCons = γ'ToChainΓ Turing.PartrecToTM2.Γ'.cons

noncomputable def shiftedNatBlock (n : ℕ) : List ChainΓ

Equations

• shiftedNatBlock n = directChainCons :: (chainBinaryRepr n).reverse

noncomputable def shiftedSymbolBlock {T : Type} [Primcodable T] (t : T) : List ChainΓ

Equations

• shiftedSymbolBlock t = shiftedNatBlock (Encodable.encode t + 1)

noncomputable def shiftedPayload {T : Type} [Primcodable T] : List T → List ChainΓ

Equations

• shiftedPayload = List.foldr (fun (t : T) (acc : List ChainΓ) => shiftedSymbolBlock t ++ acc) []

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

Equations

• shiftedChainTape w = chainConsBottom :: shiftedPayload w ++ [directChainCons]

theorem directChainCons_ne_default : directChainCons ≠ default

theorem shiftedNatBlock_ne_default (n : ℕ) (g : ChainΓ) : g ∈ shiftedNatBlock n → g ≠ default

theorem shiftedSymbolBlock_ne_default {T : Type} [Primcodable T] (t : T) (g : ChainΓ) : g ∈ shiftedSymbolBlock t → g ≠ default

theorem shiftedPayload_ne_default {T : Type} [Primcodable T] (w : List T) (g : ChainΓ) : g ∈ shiftedPayload w → g ≠ default

theorem shiftedChainTape_ne_default {T : Type} [Primcodable T] (w : List T) (g : ChainΓ) : g ∈ shiftedChainTape w → g ≠ default

theorem trList_eq_flatMap (ns : List ℕ) : Turing.PartrecToTM2.trList ns = List.flatMap (fun (n : ℕ) => Turing.PartrecToTM2.trNat n ++ [Turing.PartrecToTM2.Γ'.cons]) ns

theorem trInit_trList_append_zero (ns : List ℕ) : Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList (ns ++ [0])) = chainConsBottom :: List.flatMap shiftedNatBlock ns.reverse

theorem flatMap_shiftedNatBlock_map_encode {T : Type} [Primcodable T] (w : List T) : List.flatMap shiftedNatBlock (List.map ((fun (x : ℕ) => x + 1) ∘ Encodable.encode) w) = shiftedPayload w

theorem trInit_trList_shiftedEncoding_eq {T : Type} [Primcodable T] (w : List T) : Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList (Langlib.TMCodeListEncode.shiftedEncoding w)) = shiftedChainTape w

noncomputable def shiftedFoldAccStep {T : Type} [Primcodable T] (t : T) (acc : List ChainΓ) : List ChainΓ

Equations

• shiftedFoldAccStep t acc = shiftedSymbolBlock t ++ acc

noncomputable def shiftedFoldTapeStep (T : Type) [DecidableEq T] [Fintype T] [Primcodable T] (t : T) : List (Option (T ⊕ ChainΓ)) → List (Option (T ⊕ ChainΓ))

Equations

• shiftedFoldTapeStep T t = hetFoldAdapt shiftedFoldAccStep t

theorem shiftedFoldTapeStep_hetMix (T : Type) [DecidableEq T] [Fintype T] [Primcodable T] (t : T) (ts : List T) (acc : List ChainΓ) : shiftedFoldTapeStep T t (hetMix ts acc) = hetMix ts (shiftedFoldAccStep t acc)

theorem shiftedFoldAccStep_ne_default {T : Type} [Primcodable T] (t : T) (acc : List ChainΓ) (hacc : ∀ g ∈ acc, g ≠ default) (g : ChainΓ) : g ∈ shiftedFoldAccStep t acc → g ≠ default

theorem shiftedFoldTapeStep_ne_default (T : Type) [DecidableEq T] [Fintype T] [Primcodable T] (t : T) (block : List (Option (T ⊕ ChainΓ))) (hblock : ∀ g ∈ block, g ≠ default) (g : Option (T ⊕ ChainΓ)) : g ∈ shiftedFoldTapeStep T t block → g ≠ default

theorem shiftedFoldBody (T : Type) [DecidableEq T] [Fintype T] [Primcodable T] : TM0RealizesHetFoldBody (shiftedFoldTapeStep T)

theorem shiftedFoldRealizes {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ∃ (Λ : Type) (x : Inhabited Λ) (x_1 : Fintype Λ) (M : Turing.TM0.Machine (Option (T ⊕ ChainΓ)) Λ), ∀ (w : List T), (TM0Seq.evalCfg M (List.map (some ∘ Sum.inl) w)).Dom ∧ ∀ (h : (TM0Seq.evalCfg M (List.map (some ∘ Sum.inl) w)).Dom), ((TM0Seq.evalCfg M (List.map (some ∘ Sum.inl) w)).get h).Tape = Turing.Tape.mk₁ (List.map (some ∘ Sum.inr) (shiftedPayload w))

noncomputable def shiftedFinishBlock {T : Type} (block : List (Option (T ⊕ ChainΓ))) : List (Option (T ⊕ ChainΓ))

Equations

• shiftedFinishBlock block = some (Sum.inr chainConsBottom) :: block ++ [some (Sum.inr directChainCons)]

theorem shiftedFinishBlock_realizes (T : Type) [DecidableEq T] [Fintype T] : TM0RealizesBlock (Option (T ⊕ ChainΓ)) shiftedFinishBlock

theorem shiftedFinishBlock_on_payload {T : Type} [Primcodable T] (w : List T) : shiftedFinishBlock (List.map (some ∘ Sum.inr) (shiftedPayload w)) = List.map directBlankEmb (shiftedChainTape w)

Remaining direct-converter obligation

def ShiftedEncodingConverter (T : Type) [DecidableEq T] [Fintype T] [Primcodable T] : Prop

The reduced converter obligation for the direct bridge.

It maps identity-encoded input w to the embedded Partrec-chain tape for shiftedEncoding w. Since T is finite, this is implemented by the finite per-symbol substitution fold above rather than binary arithmetic on the tape.

Equations

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

theorem shifted_converter_exists {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] : ShiftedEncodingConverter T

Local alphabet embedding

noncomputable def directEmbedTM0 {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine ChainΓ Λ) : Turing.TM0.Machine (Option (T ⊕ ChainΓ)) Λ

Embed a ChainΓ TM0 into Option (T ⊕ ChainΓ), preserving blanks.

Equations

• directEmbedTM0 M = TM0AlphabetSim.liftMachine M directBlankEmb directBlankInv

theorem directEmbedTM0_eval_dom {T Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine ChainΓ Λ) (l : List ChainΓ) : (Turing.TM0.eval M l).Dom ↔ (Turing.TM0.eval (directEmbedTM0 M) (List.map directBlankEmb l)).Dom

The direct embedding preserves halting behavior.

theorem code_implies_isTM_of_shifted_converter {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] (hconv : ShiftedEncodingConverter T) (L : Language T) (c : Turing.ToPartrec.Code) (hL : ∀ (w : List T), w ∈ L ↔ (c.eval [Encodable.encode w]).Dom) : is_TM L

Once the reduced converter exists, any ToPartrec.Code-semidecidable language is is_TM.

This is the sound replacement target for the current arithmetic converter: the Code-level list encoding is already handled by composedCode, and the tape-level converter only needs to write shiftedEncoding w.

theorem code_implies_isTM_direct {T : Type} [DecidableEq T] [Fintype T] [Primcodable T] (L : Language T) (c : Turing.ToPartrec.Code) (hL : ∀ (w : List T), w ∈ L ↔ (c.eval [Encodable.encode w]).Dom) : is_TM L