OrderedSweep.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Quantitative separation during ordered horizontal extraction and insertion. Only the active rectangle's right endpoint changes during its swept box.

def OAI.ForcedComputation.PlanarRouting.EndpointGap line 14
Source documentation
A rational coordinate gap between two filled rectangles.
```
def EndpointGap (δ : ℚ) (R S : RationalBox 2) : Prop :=
…
```
theorem OAI.ForcedComputation.PlanarRouting.endpointGap_of_le_boxGap line 19
Source documentation
The existing computable maximum of the four signed endpoint gaps supplies an actual separating coordinate.
```
theorem endpointGap_of_le_boxGap {R S : RationalBox 2} {δ : ℚ}
    (hδ : δ ≤ boxGap R S) : EndpointGap δ R S := by
…
```
Mentions: OAI.ForcedComputation.PlanarRouting.EndpointGap
theorem OAI.ForcedComputation.PlanarRouting.separated_endpointGap line 28
def OAI.ForcedComputation.PlanarRouting.rightSweep line 36
Source documentation
The full bounding box swept when a rectangle is moved horizontally to a point on its right. endpoint is the right edge of the translated rectangle.
```
def rightSweep (R : RationalBox 2) (endpoint : ℚ) : RationalBox 2 :=
…
```
theorem OAI.ForcedComputation.PlanarRouting.rightSweep_positive line 39

theorem OAI.ForcedComputation.PlanarRouting.left_gap_of_center_order line 47

Source documentation

Center order rules out a separated obstacle lying to the right.

theorem left_gap_of_center_order {a b c d δ : ℚ}
    (hab : a ≤ b) (hcd : c ≤ d) (hδ : 0 < δ) (hcenter : c + d ≤ a + b)
    (hgap : b + δ ≤ c ∨ d + δ ≤ a) : d + δ ≤ a := by
…

theorem OAI.ForcedComputation.PlanarRouting.rightSweep_gap line 57
Source documentation
A stationary rectangle with no larger horizontal center retains the same quantitative gap while the active rectangle sweeps to the right.
```
theorem rightSweep_gap {R S : RationalBox 2} {δ : ℚ}
    (hR : R.positive) (hS : S.positive) (hδ : 0 < δ)
    (hcenter : S.lower 0 + S.upper 0 ≤ R.lower 0 + R.upper 0)
    (hgap : EndpointGap δ R S) (endpoint : ℚ) :
    EndpointGap δ (rightSweep R endpoint) S := by
…
```
Mentions: OAI.ForcedComputation.PlanarRouting.EndpointGap, OAI.ForcedComputation.PlanarRouting.rightSweep
theorem OAI.ForcedComputation.PlanarRouting.rightSweep_gap_of_centers line 68
theorem OAI.ForcedComputation.PlanarRouting.EndpointGap.separated line 79