OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarProgramBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Uniform chart margins for every filled tube and parking box in the finite planar compiler. These bounds concern the whole rectangles, including points which do not encode tapes.

  1. def OAI.ForcedComputation.PlanarRouting.Between line 13
  2. theorem OAI.ForcedComputation.PlanarRouting.endpoints_of_carrier line 16
  3. theorem OAI.ForcedComputation.PlanarRouting.centerQ_between line 29
  4. theorem OAI.ForcedComputation.PlanarRouting.recenter_between line 37
  5. theorem OAI.ForcedComputation.PlanarRouting.recenter_halfWidthQ line 47
  6. theorem OAI.ForcedComputation.PlanarRouting.translationTube_between line 52
  7. theorem OAI.ForcedComputation.PlanarRouting.between_mono line 58
  8. theorem OAI.ForcedComputation.Recorder.Planar.instruction_endpoint_bounds line 69
  9. theorem OAI.ForcedComputation.Recorder.Planar.instruction_halfWidthQ_bound line 88
  10. theorem OAI.ForcedComputation.Recorder.Planar.parkingFor_between line 123
  11. theorem OAI.ForcedComputation.Recorder.Planar.horizontalCenter_between line 132
  12. theorem OAI.ForcedComputation.Recorder.Planar.phaseRectangle_between line 143
  13. theorem OAI.ForcedComputation.Recorder.Planar.Action.rectangle_between line 184
  14. theorem OAI.ForcedComputation.Recorder.Planar.compiledPulse_inUnit line 196