theorem TMCodingInstance.stdDecode_encode (n : ℕ) : stdDecode (stdEncode n) = some n

The decoder is a left inverse of the encoder: stdDecode ∘ stdEncode = some.

def TMCodingInstance.stdLanguageOf (M : ℕ) : Set (List Bool)

The language recognized by TM index M: the set of strings accepted by the standard behavior.

theorem TMCodingInstance.stdPair_injective (a b c d : List Bool) : stdPair a b = stdPair c d → a = c ∧ b = d

The pairing function is injective in both arguments simultaneously.

theorem TMCodingInstance.stdSmn_spec_behavior (e x : ℕ) (w : List Bool) : stdBehavior (stdSmn e x) w = stdBehavior e (stdPair w (stdEncode x))

s-m-n specification at the behavior level: running stdSmn e x on w behaves exactly like running e on the paired input ⟨w, ⟨x⟩⟩.

theorem TMCodingInstance.stdSmn_spec (e x : ℕ) (w : List Bool) : w ∈ stdLanguageOf (stdSmn e x) ↔ stdPair w (stdEncode x) ∈ stdLanguageOf e

s-m-n specification at the language level: w is in L(stdSmn e x) iff ⟨w, ⟨x⟩⟩ is in L(e).

def TMCodingInstance.stdIsComputable (f : ℕ → ℕ) : Prop

A function f : ℕ → ℕ on TM indices is computable (behavior version): there is a single index e such that stdSmn e x and f x define extensionally equal behaviors for every x.

def TMCodingInstance.stdIsComputableLang (f : ℕ → ℕ) : Prop

A function f : ℕ → ℕ on TM indices is computable (language version): there is an index e such that stdSmn e x and f x recognize the same language for every x.

theorem TMCodingInstance.stdRepresentable (h : ℕ → ℕ) : stdIsComputable h → ∃ (e : ℕ), ∀ (x : ℕ) (w : List Bool), stdBehavior (stdSmn e x) w = stdBehavior (h x) w

Representability: every behavior-computable function h has an index e witnessing its computability. (Restatement of the definition.)

theorem TMCodingInstance.stdIsComputable_smn_diag : stdIsComputable fun (x : ℕ) => stdSmn x x

The diagonal s-m-n function x ↦ stdSmn x x is computable.

theorem TMCodingInstance.stdIsComputable_comp (f g : ℕ → ℕ) : stdIsComputable f → stdIsComputable g → stdIsComputable (f ∘ g)

Computable functions on indices are closed under composition (behavior version).

theorem TMCodingInstance.stdIsComputable_smn_apply (e : ℕ) : stdIsComputable (stdSmn e)

For every index e, partial application x ↦ stdSmn e x is computable.

theorem TMCodingInstance.stdRepresentableLang (h : ℕ → ℕ) : stdIsComputableLang h → ∃ (e : ℕ), ∀ (x : ℕ), stdLanguageOf (stdSmn e x) = stdLanguageOf (h x)

Representability for the language version: any IsComputableLang function is witnessed by an index.

theorem TMCodingInstance.stdIsComputableLang_smn_diag : stdIsComputableLang fun (x : ℕ) => stdSmn x x

The diagonal s-m-n function is computable at the language level.

theorem TMCodingInstance.stdIsComputableLang_comp (f g : ℕ → ℕ) : stdIsComputableLang f → stdIsComputableLang g → stdIsComputableLang (f ∘ g)

Composition closure for language-computability.

theorem TMCodingInstance.stdIsComputableLang_smn_apply (e : ℕ) : stdIsComputableLang (stdSmn e)

For every e, partial application x ↦ stdSmn e x is language-computable.

theorem TMCodingInstance.stdLanguages_beyond_length (n : ℕ) : ∃ (M : ℕ), ∀ (M' : ℕ), (stdEncode M').length < n → stdLanguageOf M' ≠ stdLanguageOf M

For any bound n, there exists a TM M whose language is different from the language of every TM whose encoding is shorter than n. (Used to construct "large" TMs in the MIN_TM proof.)

theorem TMCodingInstance.stdRecognizable_enumSearch_computable (P : ℕ → Prop) : TuringMachine.IsTuringRecognizable {s : List Bool | ∃ (M : ℕ), stdEncode M = s ∧ P M} → ∀ (t : ℕ → ℕ), (∀ (M : ℕ), P (t M) ∧ (stdEncode M).length < (stdEncode (t M)).length) → stdIsComputableLang t

Enumeration-search principle: if the set of encodings of indices satisfying P is Turing-recognizable and t selects, for every M, a strictly longer encoded index with P (t M), then t is language-computable.

noncomputable def RecursionTheorem.standardTMCoding : TMCoding Bool

The standard TMCoding instance for RecursionTheorem, packaging the behavior-level encoding, pairing, s-m-n, and computability operations into the abstract TMCoding Bool structure used by the recursion theorem development.

noncomputable def TuringMachine.standardTMCoding : TMCoding Bool

The standard TMCoding instance for TuringMachine, packaging the language-level data (languageOf, language-computability, enumSearch, etc.) into a single coding used by the general TM theory.