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

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Rational filled rectangles and reciprocal affine maps for all three head moves. These are the exact rows of the radix table in Section 4 of paper 379-01.

  1. inductive OAI.ForcedComputation.Radix.HeadMove line 15
  2. def OAI.ForcedComputation.Radix.sourceBox line 19
  3. def OAI.ForcedComputation.Radix.targetBox line 22
  4. def OAI.ForcedComputation.Radix.headFactor line 27
  5. def OAI.ForcedComputation.Radix.radixInstruction line 32
  6. theorem OAI.ForcedComputation.Radix.headFactor_pos line 35
  7. theorem OAI.ForcedComputation.Radix.sourceBox_positive line 39
  8. theorem OAI.ForcedComputation.Radix.targetBox_positive line 45
  9. theorem OAI.ForcedComputation.Radix.radixInstruction_image line 61
  10. def OAI.ForcedComputation.Radix.normalizedMove line 71
  11. def OAI.ForcedComputation.Radix.planeOfPair line 76
  12. theorem OAI.ForcedComputation.Radix.radixInstruction_action line 78
  13. def OAI.ForcedComputation.Radix.scaledBox line 91
  14. theorem OAI.ForcedComputation.Radix.scaledBox_center line 94
  15. theorem OAI.ForcedComputation.Radix.scaledBox_halfWidth line 99
  16. theorem OAI.ForcedComputation.Radix.scaledBox_positive line 104
  17. def OAI.ForcedComputation.Radix.scaledInstruction line 110
  18. theorem OAI.ForcedComputation.Radix.scaledInstruction_image line 114
  19. def OAI.ForcedComputation.Radix.embedPlane line 131
  20. theorem OAI.ForcedComputation.Radix.scaledBox_image line 134
  21. theorem OAI.ForcedComputation.Radix.scaledInstruction_action line 162