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

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Rational parking columns and filled translation tubes for the planar processor. The same horizontal compression used by the recorder leaves a quantitative gap between every two parking columns.

  1. def OAI.ForcedComputation.PlanarRouting.centerQ line 18
  2. def OAI.ForcedComputation.PlanarRouting.halfWidthQ line 20
  3. theorem OAI.ForcedComputation.PlanarRouting.centerQ_cast line 22
  4. theorem OAI.ForcedComputation.PlanarRouting.halfWidthQ_cast line 25
  5. def OAI.ForcedComputation.PlanarRouting.recenter line 28
  6. theorem OAI.ForcedComputation.PlanarRouting.recenter_center line 31
  7. theorem OAI.ForcedComputation.PlanarRouting.recenter_halfWidth line 38
  8. theorem OAI.ForcedComputation.PlanarRouting.recenter_positive line 44
  9. theorem OAI.ForcedComputation.PlanarRouting.recenter_image line 51
  10. def OAI.ForcedComputation.PlanarRouting.translationTube line 78

    Source documentation

    A filled tube containing every intermediate translated rectangle.

    def translationTube (R : RationalBox 2) (p : Fin 2 → ℚ) : RationalBox 2 :=
…
  11. theorem OAI.ForcedComputation.PlanarRouting.translationTube_positive line 82
  12. theorem OAI.ForcedComputation.PlanarRouting.translationPath_mem_tube line 87
  13. def OAI.ForcedComputation.PlanarRouting.parkingScale line 113
  14. def OAI.ForcedComputation.PlanarRouting.parkingCenter line 115
  15. def OAI.ForcedComputation.PlanarRouting.parkingBox line 119

    Source documentation

    This contains the whole four-shear trajectory, not only its endpoints.

    def parkingBox (n : ℕ) (κ : ℚ) (i : Fin n) : RationalBox 2 :=
…
  16. theorem OAI.ForcedComputation.PlanarRouting.parkingScale_pos line 124
  17. theorem OAI.ForcedComputation.PlanarRouting.parkingScale_le line 128
  18. theorem OAI.ForcedComputation.PlanarRouting.parkingCenter_bounds line 134
  19. theorem OAI.ForcedComputation.PlanarRouting.parkingCenter_gap line 148
  20. theorem OAI.ForcedComputation.PlanarRouting.parkingBox_positive line 163
  21. theorem OAI.ForcedComputation.PlanarRouting.parkingBox_bounds line 169
  22. theorem OAI.ForcedComputation.PlanarRouting.parkingBox_gap line 194
  23. theorem OAI.ForcedComputation.PlanarRouting.parkingBox_separation line 204
  24. theorem OAI.ForcedComputation.PlanarRouting.recenter_subset_parking line 212
  25. theorem OAI.ForcedComputation.PlanarRouting.low_rectangle_parking_gap line 231
  26. theorem OAI.ForcedComputation.PlanarRouting.instruction_scaling_mem_parking line 241

    Source documentation

    The actual anisotropic scaling path of an instruction stays in its parking box. Both input and output widths are used, since either reciprocal factor may be large.

    theorem instruction_scaling_mem_parking {n : ℕ} {κ : ℚ} (hκ : 0 ≤ κ)
    (i : Fin n) (r : Instruction) (hr : 0 < r.factor)
    (himage : r.affine '' r.source.carrier = r.target.carrier)
    (hsx : r.source.halfWidth 0 ≤ (parkingScale n : ℝ) * (κ : ℝ) / 2)
    (htx : r.target.halfWidth 0 ≤ (parkingScale n : ℝ) * (κ : ℝ) / 2)
    (hsy : r.source.halfWidth 1 ≤ (3 / 8 : ℝ) * (κ : ℝ) / 2)
    (hty : r.target.halfWidth 1 ≤ (3 / 8 : ℝ) * (κ : ℝ) / 2)
    {x : Plane} (hx : x ∈ r.source.carrier) (t : ℝ) :
    PlanarHamiltonian.anisotropicRoute (parkingScale n) (3 / 8) r.factor
      (fun j => (parkingCenter n i j : ℝ))
      (x + ((fun j => (parkingCenter n i j : ℝ)) - r.source.center)) t ∈
        (parkingBox n κ i).carrier := by
…

    Mentions: OAI.ForcedComputation.PlanarRouting.parkingScale, OAI.ForcedComputation.PlanarHamiltonian.anisotropicRoute, OAI.ForcedComputation.PlanarRouting.parkingCenter, OAI.ForcedComputation.PlanarRouting.parkingBox