OAI/Computability/WLIdentification/MachineCells.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.WLIdentification.Machine.State line 9
  2. abbrev OAI.WLIdentification.Machine.Symbol line 10
  3. abbrev OAI.WLIdentification.Machine.Letter line 11
  4. def OAI.WLIdentification.Machine.action line 14

    Source documentation

    Extend the finite transition table by its stipulated frozen halts.

    def action (M : Machine) (q : M.State) (a : M.Symbol) : M.State × M.Symbol × Move :=
…

    Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.Move

  5. theorem OAI.WLIdentification.Machine.action_halt line 17
  6. def OAI.WLIdentification.Machine.localRule line 22

    Source documentation

    A completely fixed radius-one alphabet table. The arbitrary multihead cases are settled by center, then left, then right priority.

    def localRule (M : Machine) (a b c : M.Letter) : M.Letter :=
…

    Mentions: OAI.WLIdentification.Machine

  7. structure OAI.WLIdentification.Machine.TapeConfig line 39

    Source documentation

    The same head/tape representation on any cyclic position alphabet.

    structure TapeConfig (M : Machine) (X : Type) where
…

    Mentions: OAI.WLIdentification.Machine

  8. def OAI.WLIdentification.Machine.TapeConfig.letter line 47
  9. def OAI.WLIdentification.Machine.TapeConfig.advance line 50
  10. theorem OAI.WLIdentification.Machine.TapeConfig.localRule_correct line 61

    Source documentation

    The finite local table is an actual one-head machine step, including seam crossings and halted configurations; no cellular-automaton theorem is assumed.

    theorem localRule_correct (e : X ≃ X)
    (hfix : ∀ x, e x ≠ x) (htwo : ∀ x, e x ≠ e.symm x)
    (c : M.TapeConfig X) (x : X) :
    M.localRule (c.letter (e.symm x)) (c.letter x) (c.letter (e x)) =
      (c.advance e).letter x := by
…

    Mentions: OAI.WLIdentification.Machine.TapeConfig.letter

  11. theorem OAI.WLIdentification.Machine.TapeConfig.advance_halted line 92
  12. def OAI.WLIdentification.Machine.ringInitial line 101

    Source documentation

    The literal input convention, transferred to a finite line segment.

    def ringInitial (M : Machine) {d : ℕ} (w : Word) : M.TapeConfig (BinaryAddress.Bits d) where
…

    Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.Word, OAI.WLIdentification.BinaryAddress.Bits

  13. def OAI.WLIdentification.Machine.ringRun line 106
  14. abbrev OAI.WLIdentification.Machine.inputSpan line 116

    Source documentation

    The literal bounded input segment, with one head marker.

    abbrev inputSpan (w : Word) := max 1 w.length

    Mentions: OAI.WLIdentification.Word

  15. abbrev OAI.WLIdentification.Machine.InitialSeed line 118
  16. def OAI.WLIdentification.Machine.initialSeedLetter line 120
  17. def OAI.WLIdentification.Machine.initialSeedMap line 124
  18. theorem OAI.WLIdentification.Machine.ringInitial_blank line 128
  19. theorem OAI.WLIdentification.Machine.initialSeed_correct line 139
  20. abbrev OAI.WLIdentification.Machine.compiledCircuit line 168

    Source documentation

    The concrete compressed tableau, now with no semantic seed assumption.

    noncomputable abbrev compiledCircuit (M : Machine) (d : ℕ) (w : Word) :=
…

    Mentions: OAI.WLIdentification.Machine, OAI.WLIdentification.Word

  21. theorem OAI.WLIdentification.Machine.compiledCircuit_iff line 174
  22. theorem OAI.WLIdentification.BinaryAddress.value_rotation line 186
  23. theorem OAI.WLIdentification.BinaryAddress.rotation_ne_self line 195
  24. theorem OAI.WLIdentification.BinaryAddress.rotation_ne_symm line 202
  25. theorem OAI.WLIdentification.Machine.ringRun_zero line 217
  26. theorem OAI.WLIdentification.Machine.ringRun_succ line 220
  27. theorem OAI.WLIdentification.Machine.evolution_ringRun line 224
  28. theorem OAI.WLIdentification.Machine.exists_letter_accept line 235
  29. theorem OAI.WLIdentification.Machine.compiledCircuit_ringRun line 245
  30. def OAI.WLIdentification.BinaryAddress.residue line 255
  31. theorem OAI.WLIdentification.BinaryAddress.value_residue line 257
  32. theorem OAI.WLIdentification.BinaryAddress.residue_zero line 262
  33. theorem OAI.WLIdentification.BinaryAddress.residue_add_one line 265
  34. theorem OAI.WLIdentification.BinaryAddress.residue_sub_one line 273
  35. theorem OAI.WLIdentification.BinaryAddress.residue_injective_window line 279
  36. theorem OAI.WLIdentification.BinaryAddress.value_residue_of_nonneg line 296
  37. theorem OAI.WLIdentification.BinaryAddress.value_residue_negative line 299