OAI/Computability/SpaceSimulation/Epoch/Nodes.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Lay out the implicit word graph in flat (epoch,column) order.

  1. def OAI.Fifths.Tour.stride line 13

    Source documentation

    First N array columns, then start and k round history columns.

    def stride := D.N+D.k+1
  2. def OAI.Fifths.Tour.total line 14
  3. abbrev OAI.Fifths.Tour.Vertex line 15
  4. theorem OAI.Fifths.Tour.stride_pos line 16
  5. theorem OAI.Fifths.Tour.total_pos line 17
  6. def OAI.Fifths.Tour.epoch line 19
  7. def OAI.Fifths.Tour.col line 20
  8. def OAI.Fifths.Tour.mkV line 21
  9. def OAI.Fifths.Tour.hV line 23
  10. theorem OAI.Fifths.Tour.epoch_lt line 25
  11. theorem OAI.Fifths.Tour.col_lt line 27
  12. theorem OAI.Fifths.Tour.re_V line 28
  13. theorem OAI.Fifths.Tour.mkV_val line 34
  14. theorem OAI.Fifths.Tour.epoch_v line 40
  15. theorem OAI.Fifths.Tour.col_v line 46
  16. def OAI.Fifths.Tour.round line 54

    Source documentation

    Round index 0 on array columns too, so all calls can parse their local functions in uniform space regardless of type.

    def round (v : D.Vertex) := D.col v - D.N
  17. theorem OAI.Fifths.Tour.round_le line 55
  18. def OAI.Fifths.Tour.valueOf line 61
  19. def OAI.Fifths.Tour.firstOf line 65
  20. def OAI.Fifths.Tour.baseOf line 68
  21. def OAI.Fifths.Tour.guesses line 70
  22. def OAI.Fifths.Tour.header line 73
  23. def OAI.Fifths.Tour.childrenOf line 76
  24. def OAI.Fifths.Tour.proposal line 81
  25. def OAI.Fifths.Tour.offer line 85
  26. def OAI.Fifths.Tour.validAt line 90
  27. def OAI.Fifths.Tour.circuit line 98
  28. def OAI.Fifths.Tour.target line 111
  29. def OAI.Fifths.Tour.coinsEasy line 113

    Source comment

    meter values
    def coinsEasy := D.circuit.price 0
  30. def OAI.Fifths.Tour.coinsHard line 114
  31. def OAI.Fifths.Tour.per line 115
  32. def OAI.Fifths.Tour.coins line 116
  33. theorem OAI.Fifths.Tour.hc line 122

    Source comment

    flat-coordinates API
    theorem hc {e j} (p : e < D.E) (h : j ≤ D.k) :
    D.col (D.hV e j) = D.N+j := D.col_v p (by unfold stride; omega)

    Mentions: OAI.Fifths.Tour.stride

  34. theorem OAI.Fifths.Tour.he line 124
  35. theorem OAI.Fifths.Tour.hr line 126
  36. theorem OAI.Fifths.Tour.ac line 128
  37. theorem OAI.Fifths.Tour.ae line 130
  38. theorem OAI.Fifths.Tour.at_array line 132
  39. theorem OAI.Fifths.Tour.at_history line 135
  40. theorem OAI.Fifths.Tour.either line 140

    Source documentation

    Useful for correctness proofs.

    theorem either (v : D.Vertex) :
    (∃ e < D.E, ∃ j < D.N, v = D.mkV e j) ∨
    (∃ e < D.E, ∃ j ≤ D.k, v = D.hV e j) := by
…