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

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Height bounds for whole instruction rectangles, rather than just encoded points. These bounds supply the clock and observer margins of the routing segments, including their filled interiors.

  1. theorem OAI.ForcedComputation.Recorder.Planar.coordinateMap_nonterminal_vertical line 13
  2. theorem OAI.ForcedComputation.Recorder.Planar.instruction_source_nonhalting line 26
  3. theorem OAI.ForcedComputation.Recorder.Planar.instruction_source_vertical line 34
  4. theorem OAI.ForcedComputation.Recorder.Planar.instruction_target_nonterminal_vertical line 46
  5. theorem OAI.ForcedComputation.Recorder.Planar.shifted_vertical_band line 57
  6. theorem OAI.ForcedComputation.Recorder.Planar.shifted_instruction_source_height line 67
  7. theorem OAI.ForcedComputation.Recorder.Planar.shifted_instruction_target_nonterminal_height line 74