OAI/Computability/SpaceSimulation/OneTape/Sweeps.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Fifths.Single.across line 9
2. def OAI.Fifths.Single.crossings line 10
3. theorem OAI.Fifths.Single.crossings_mono line 12
4. theorem OAI.Fifths.Single.tick_value line 18
5. theorem OAI.Fifths.Single.waited line 22
6. theorem OAI.Fifths.Single.sweep_time line 36

   Source documentation

   Sweep from time t with the currently selected block. If neither cap nor crossing reached, advanced just one tick per local iteration. At a crossing bank its credit. Unselected buffers unchanged throughout.

   theorem sweep_time (t : ℕ) (l : t ≤ W.T) (n : ℕ) :
       let i := M.place x W t
   …

7. theorem OAI.Fifths.Single.visited line 68
8. theorem OAI.Fifths.Single.story_ok line 88
9. def OAI.Fifths.Single.doneAt line 99
10. def OAI.Fifths.Single.predict line 101
11. theorem OAI.Fifths.Single.reported line 104
12. theorem OAI.Fifths.Single.closes line 112
13. theorem OAI.Fifths.Single.divides_shift line 121

    Source comment

    At most one crossing per unit move when summing across offsets.

    private theorem divides_shift {b u m : ℕ}
        (h : (u+m)/b ≠ (u+(m+1))/b) : b ∣ u+m+1 := by
    …

14. theorem OAI.Fifths.Single.unique_cross line 126
15. theorem OAI.Fifths.Single.atMostOne line 157
16. theorem OAI.Fifths.Single.offsets line 186
17. theorem OAI.Fifths.Single.sufficient line 194