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

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Quantitative collar separation for the pulses that leave another branch at rest. Horizontal sweeps avoid parking boxes; vertical sweeps stay inside their own narrow parking columns.

  1. theorem OAI.ForcedComputation.PlanarRouting.verticalFrom_lower line 13
  2. theorem OAI.ForcedComputation.PlanarRouting.verticalFrom_upper line 20
  3. theorem OAI.ForcedComputation.PlanarRouting.verticalTo_lower line 27
  4. theorem OAI.ForcedComputation.PlanarRouting.verticalTo_upper line 33
  5. theorem OAI.ForcedComputation.PlanarRouting.column_gap_of_horizontal_bounds line 39
  6. theorem OAI.ForcedComputation.PlanarRouting.verticalFrom_parking_gap line 51
  7. theorem OAI.ForcedComputation.PlanarRouting.verticalTo_parking_gap line 63
  8. theorem OAI.ForcedComputation.PlanarRouting.verticalFrom_low_gap line 75
  9. theorem OAI.ForcedComputation.PlanarRouting.verticalTo_low_gap line 85
  10. theorem OAI.ForcedComputation.Recorder.Planar.target_insertion_clearance line 101
  11. theorem OAI.ForcedComputation.Recorder.Planar.instruction_narrow_widths line 121
  12. def OAI.ForcedComputation.Recorder.Planar.parkingRegion line 137
  13. theorem OAI.ForcedComputation.Recorder.Planar.extractHorizontal_parking_gap line 141
  14. theorem OAI.ForcedComputation.Recorder.Planar.insertHorizontal_parking_gap line 147
  15. theorem OAI.ForcedComputation.Recorder.Planar.extractVertical_parking_gap line 158
  16. theorem OAI.ForcedComputation.Recorder.Planar.insertVertical_parking_gap line 166
  17. theorem OAI.ForcedComputation.Recorder.Planar.scaling_parking_gap line 174
  18. theorem OAI.ForcedComputation.Recorder.Planar.extractVertical_source_gap line 181
  19. theorem OAI.ForcedComputation.Recorder.Planar.insertVertical_target_gap line 188