OAI/Computability/SpaceSimulation/Epoch/Core.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Fifths.Radix.join_lt line 8
  2. theorem OAI.Fifths.Radix.pack_append line 16
  3. theorem OAI.Fifths.Radix.get_join_zero line 25

    Source comment

    Needed to fix first digit pasting a suffix.
    theorem get_join_zero (m n u v : ℕ) (h : 0 < n) :
    get m (u + m^n*v) 0 = get m u 0 := by
…

    Mentions: OAI.Fifths.Radix.get

  4. structure OAI.Fifths.Tour line 38

    Source documentation

    A deterministic reference visit touches one selected block. All bounded state carried between visits, other than the blocks, is a raw c-bit controller. k>0, b=k*k; block tapings have at most b controller-width digits.

    structure Tour where
…
  5. structure OAI.Fifths.Scene line 50
  6. def OAI.Fifths.Tour.b line 58
  7. def OAI.Fifths.Tour.E line 59
  8. def OAI.Fifths.Tour.m line 60
  9. def OAI.Fifths.Tour.width line 61
  10. def OAI.Fifths.Tour.guessLength line 62
  11. theorem OAI.Fifths.Tour.m_pos line 64
  12. theorem OAI.Fifths.Tour.powers line 65
  13. theorem OAI.Fifths.Tour.b_pos line 66
  14. theorem OAI.Fifths.Tour.k_le line 67
  15. def OAI.Fifths.Tour.step line 69
  16. def OAI.Fifths.Tour.story line 73
  17. structure OAI.Fifths.Tour.FiniteWords line 77
  18. theorem OAI.Fifths.Tour.ctrl_step line 83
  19. theorem OAI.Fifths.Tour.cells_step line 85
  20. theorem OAI.Fifths.Tour.finite_story line 91
  21. def OAI.Fifths.Tour.replayStep line 106

    Source documentation

    Proposed transcript Z has controller at each digit. Scan local block i from block data B. Continue applying the visits even on a failed test. Normalize initial B (no-op on semantic arguments).

    def replayStep (i Z j : ℕ) (s : ℕ × Bool) : ℕ × Bool :=
…
  22. def OAI.Fifths.Tour.replay line 113
  23. theorem OAI.Fifths.Tour.replay_lt line 117
  24. def OAI.Fifths.Tour.agrees line 131

    Source documentation

    Offered replay from step t. Predicates need only check each block separately.

    def agrees (Z t n : ℕ) : Prop :=
…
  25. def OAI.Fifths.Tour.replayOn line 134
  26. theorem OAI.Fifths.Tour.replay_true line 136
  27. theorem OAI.Fifths.Tour.passes_agree line 152
  28. def OAI.Fifths.Tour.log line 185

    Source documentation

    Epoch prefix history stores n+1 controllers beginning at visit-number t.

    def log (t n : ℕ) : ℕ :=
…
  29. theorem OAI.Fifths.Tour.log_lt line 187
  30. theorem OAI.Fifths.Tour.log_agrees line 189
  31. theorem OAI.Fifths.Tour.agrees_log line 192
  32. def OAI.Fifths.Tour.suffix line 197
  33. theorem OAI.Fifths.Tour.suffix_lt line 199
  34. theorem OAI.Fifths.Tour.log_extend line 202