`Transition`

definition

show as: view math explainer →

module: IndisputableMonolith.Information.ChurchTuring
domain: Information
line: 57 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Information.ChurchTuring on GitHub at line 57.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  54  alphabet_nonempty : alphabetSize > 0
  55
  56/-- A TM transition: (state, symbol) → (new_state, new_symbol, direction). -/
  57structure Transition where
  58  currentState : ℕ
  59  currentSymbol : ℕ
  60  newState : ℕ
  61  newSymbol : ℕ
  62  moveRight : Bool  -- True = right, False = left
  63
  64/-! ## Universal Turing Machine -/
  65
  66/-- A Universal Turing Machine (UTM) can simulate any other TM.
  67
  68    Given:
  69    - Description of TM T (on tape)
  70    - Input x
  71
  72    UTM computes T(x).
  73
  74    This is the foundation of programmable computers! -/
  75structure UniversalTM where
  76  base : TuringMachine
  77  /-- Can simulate any other TM -/
  78  universal : Bool := true
  79
  80/-- **THEOREM**: A UTM exists.
  81
  82    Proof: Construct explicit UTM (Turing 1936).
  83    Small UTM: (2 states, 18 symbols) or (7 states, 4 symbols). -/
  84theorem utm_exists : True := trivial
  85
  86/-! ## Ledger as Universal Computer -/
  87

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.