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

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Effective source and target orders for the finite planar processor. Extraction goes from right to left; insertion goes from left to right. The orders are stable merge sorts of rational centers, including tied centers.

  1. def OAI.ForcedComputation.PlanarRouting.sortBy line 13
  2. theorem OAI.ForcedComputation.PlanarRouting.sortBy_perm line 16
  3. theorem OAI.ForcedComputation.PlanarRouting.sortBy_length line 19
  4. theorem OAI.ForcedComputation.PlanarRouting.mem_sortBy line 22
  5. theorem OAI.ForcedComputation.PlanarRouting.sortBy_pairwise line 25
  6. theorem OAI.ForcedComputation.PlanarRouting.sortBy_get_le line 32
  7. theorem OAI.ForcedComputation.PlanarRouting.sortBy_nodup line 37
  8. def OAI.ForcedComputation.PlanarRouting.rank line 40
  9. theorem OAI.ForcedComputation.PlanarRouting.get_rank line 44
  10. theorem OAI.ForcedComputation.PlanarRouting.rank_injective line 48
  11. def OAI.ForcedComputation.Recorder.Planar.sourceOrder line 60
  12. def OAI.ForcedComputation.Recorder.Planar.targetOrder line 65
  13. theorem OAI.ForcedComputation.Recorder.Planar.sourceOrder_perm line 70
  14. theorem OAI.ForcedComputation.Recorder.Planar.targetOrder_perm line 73
  15. theorem OAI.ForcedComputation.Recorder.Planar.sourceOrder_nodup line 76
  16. theorem OAI.ForcedComputation.Recorder.Planar.targetOrder_nodup line 80
  17. theorem OAI.ForcedComputation.Recorder.Planar.sourceOrder_complete line 84
  18. theorem OAI.ForcedComputation.Recorder.Planar.targetOrder_complete line 89
  19. theorem OAI.ForcedComputation.Recorder.Planar.sourceOrder_centers line 94
  20. theorem OAI.ForcedComputation.Recorder.Planar.targetOrder_centers line 106
  21. theorem OAI.ForcedComputation.Recorder.Planar.sourceOrder_sweep_gap line 118

    Source documentation

    Later source rows do not intersect the active extraction tube.

    theorem sourceOrder_sweep_gap (M : Alternating.Machine) (hM : M.WellFormed)
    {i j : Fin (sourceOrder M hM).length} (hij : i < j) (endpoint : ℚ) :
    let R := (instruction M hM ((sourceOrder M hM).get i)).source
…

    Mentions: OAI.Alternating.Machine, OAI.ForcedComputation.Recorder.Planar.sourceOrder, OAI.ForcedComputation.Recorder.Planar.instruction

  22. theorem OAI.ForcedComputation.Recorder.Planar.targetOrder_sweep_gap line 134

    Source documentation

    Earlier inserted targets do not intersect the active insertion tube.

    theorem targetOrder_sweep_gap (M : Alternating.Machine) (hM : M.WellFormed)
    {i j : Fin (targetOrder M hM).length} (hij : i < j) (endpoint : ℚ) :
    let R := (instruction M hM ((targetOrder M hM).get j)).target
…

    Mentions: OAI.Alternating.Machine, OAI.ForcedComputation.Recorder.Planar.targetOrder, OAI.ForcedComputation.Recorder.Planar.instruction