OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/LatticeArithmetic.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

The finite integer arithmetic of the periodic-lattice processor. A configuration uses two fixed-width stacks and one state digit. Every integer address is decoded by its least nonnegative residue, including negative lifts of the same point on the torus.

  1. def OAI.ForcedComputation.Lattice.stackBase line 12
  2. def OAI.ForcedComputation.Lattice.period line 14
  3. def OAI.ForcedComputation.Lattice.pack line 16
  4. def OAI.ForcedComputation.Lattice.leftStack line 18
  5. def OAI.ForcedComputation.Lattice.rightStack line 20
  6. def OAI.ForcedComputation.Lattice.stateDigit line 22
  7. theorem OAI.ForcedComputation.Lattice.stackBase_pos line 24
  8. theorem OAI.ForcedComputation.Lattice.period_pos line 27
  9. theorem OAI.ForcedComputation.Lattice.period_eq line 30
  10. theorem OAI.ForcedComputation.Lattice.prepend_lt line 33
  11. theorem OAI.ForcedComputation.Lattice.pack_lt line 36
  12. theorem OAI.ForcedComputation.Lattice.pack_left line 41
  13. theorem OAI.ForcedComputation.Lattice.pack_div line 45
  14. theorem OAI.ForcedComputation.Lattice.pack_right line 50
  15. theorem OAI.ForcedComputation.Lattice.pack_state line 55
  16. theorem OAI.ForcedComputation.Lattice.leftStack_lt line 60
  17. theorem OAI.ForcedComputation.Lattice.rightStack_lt line 63
  18. theorem OAI.ForcedComputation.Lattice.stateDigit_lt line 66
  19. theorem OAI.ForcedComputation.Lattice.pack_decode line 74
  20. def OAI.ForcedComputation.Lattice.address line 79
  21. theorem OAI.ForcedComputation.Lattice.address_lt line 81
  22. theorem OAI.ForcedComputation.Lattice.address_periodic line 84
  23. theorem OAI.ForcedComputation.Lattice.address_nat line 89
  24. theorem OAI.ForcedComputation.Lattice.address_congr line 93
  25. def OAI.ForcedComputation.Lattice.nextLeft line 98

    Source documentation

    Move 0 is left, move 1 is stationary, and move 2 is right.

    def nextLeft (b L a : ℕ) (m : Fin 3) : ℕ :=
…
  26. def OAI.ForcedComputation.Lattice.nextRight line 101
  27. theorem OAI.ForcedComputation.Lattice.left_move_formula line 105
  28. theorem OAI.ForcedComputation.Lattice.stationary_move_formula line 113
  29. theorem OAI.ForcedComputation.Lattice.quotient_power_lt line 120
  30. theorem OAI.ForcedComputation.Lattice.next_stacks_lt line 126
  31. structure OAI.ForcedComputation.Lattice.Rule line 151
  32. structure OAI.ForcedComputation.Lattice.Table line 158

    Source documentation

    A finite lookup table, without any assumption about addresses visited by a run.

    structure Table (b : ℕ) where
…
  33. def OAI.ForcedComputation.Lattice.Table.lookup line 163
  34. def OAI.ForcedComputation.Lattice.readTransition line 166
  35. def OAI.ForcedComputation.Lattice.transition line 173
  36. def OAI.ForcedComputation.Lattice.haltFlag line 176
  37. theorem OAI.ForcedComputation.Lattice.transition_periodic line 179
  38. theorem OAI.ForcedComputation.Lattice.haltFlag_periodic line 185
  39. theorem OAI.ForcedComputation.Lattice.readTransition_lt line 191
  40. theorem OAI.ForcedComputation.Lattice.transition_lt line 204
  41. theorem OAI.ForcedComputation.Lattice.readTransition_pack line 208