Unrestricted Grammars → Turing Machines

This file proves that every language generated by an unrestricted grammar is TM-recognizable (internally): RE ⊆ TM.

Main results

• re_implies_tm — is_RE L → is_TM L (TM-recognizable)

Strategy

1. Restrict the grammar to finitely many nonterminals.
2. Show grammar membership is a Computable₂ search: w ∈ L ↔ ∃ seq, grammarTest g seq w.
3. The µ-search is Nat.Partrec (via search_is_partrec), giving a Code.
4. Apply code_implies_isTM_direct to get is_TM L.

Step 4 uses the direct encoding bridge (CodeToTMDirect.lean).

theorem re_implies_tm {T : Type} [DecidableEq T] [Fintype T] (L : Language T) (hL : is_RE L) : is_TM L

Every recursively enumerable language (generated by an unrestricted grammar) is internally TM-recognizable with finite states.

theorem RE_subset_TM {T : Type} [DecidableEq T] [Fintype T] : RE ⊆ TM

Every recursively enumerable language over a finite alphabet is TM-recognizable.