Distance.lean`

73 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.PlanarL1.Columns.Model.Point.paths_nonempty line 16
def OAI.PlanarL1.Columns.Model.Point.distance line 21
lemma OAI.PlanarL1.Columns.Model.Point.lengths_bddBelow line 24
lemma OAI.PlanarL1.Columns.Model.Point.distance_le line 28
lemma OAI.PlanarL1.Columns.Model.Point.distance_nonneg line 32
lemma OAI.PlanarL1.Columns.Model.Point.height_change_le line 36
lemma OAI.PlanarL1.Columns.Model.Point.distance_self line 40
lemma OAI.PlanarL1.Columns.Model.Point.distance_triangle line 44
lemma OAI.PlanarL1.Columns.Model.Point.distance_comm line 54
instance OAI.PlanarL1.Columns.Model.Point.(instance at line 65) line 65
lemma OAI.PlanarL1.Columns.Model.Point.dist_same_column line 73
Source documentation
The full vertical interval is isometric, before or after the quotient. No path's vertical variation can improve upon direct travel.
```
lemma dist_same_column (x y : M.Point J root) (h : x.column = y.column) :
    dist x y = |x.height - y.height| := by
…
```
def OAI.PlanarL1.Columns.Model.Point.withHeight line 84
Source documentation
Vertical motion on a chosen column representative.
```
def withHeight (x : M.Point J root) (H : ℝ) (hH : H ∈ J) : M.Point J root :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.withHeight_self line 87
lemma OAI.PlanarL1.Columns.Model.Point.dist_withHeight line 90
lemma OAI.PlanarL1.Columns.Model.Point.dist_le_switch line 93

lemma OAI.PlanarL1.Columns.Model.Point.dist_midpoints_le line 100

Source documentation

The source's adjacent-midpoint estimate: one available switch costs at most the width of the band.

lemma dist_midpoints_le (x y : M.Point J root) {H a : ℝ}
    (hx : x.height = H) (hy : y.height = H)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (h : (M.activeGraph J).Adj x.column y.column) : dist x y ≤ a := by
…

def OAI.PlanarL1.Columns.Model.Point.simpleLengths line 110
Source documentation
Lengths realized by words with no repeated column.
```
def simpleLengths (x y : M.Point J root) : Set ℝ :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.mem_simpleLengths line 114
lemma OAI.PlanarL1.Columns.Model.Point.simpleLengths_nonempty line 120
lemma OAI.PlanarL1.Columns.Model.Point.isCompact_simpleLengths line 125
lemma OAI.PlanarL1.Columns.Model.Point.exists_shortest line 137
Source documentation
Geometry, geo:geodesics: finite intrinsic distances are attained by a switching path with no repeated column. Compactness is required of the actual switch-height sets, rather than of an artificial discretization.
```
lemma exists_shortest (hJ : IsClosed J) (x y : M.Point J root) :
    ∃ p : M.Path J x.column y.column,
      p.word.IsPath ∧ p.length x.height y.height = dist x y := by
…
```

lemma OAI.PlanarL1.Columns.Model.Point.dist_le_of_shared_column line 157

Source documentation

Two short paths whose projected words meet on a column give a short connection, with only one band-width paid for the vertical transfer.

lemma dist_le_of_shared_column (x y : M.Point J root) {i j v : Fin n}
    (p : M.Path J x.column i) (q : M.Path J y.column j)
    {H T a : ℝ} (hH : H ∈ J) (hT : T ∈ J)
    (hwidth : ∀ r ∈ J, ∀ s ∈ J, |r - s| ≤ a)
    (hpv : v ∈ p.word.support) (hqv : v ∈ q.word.support) :
    dist x y ≤ p.length x.height H + q.length y.height T + a := by
…

lemma OAI.PlanarL1.Columns.Model.Point.zero_distance_iff line 178
Source documentation
The source's quotient identifies precisely finite chains of switches at a single height. This verifies that metric separation has not introduced any extra quotient relations.
```
lemma zero_distance_iff (hJ : IsClosed J) (x y : M.Point J root) :
    dist x y = 0 ↔ x.height = y.height ∧
      (M.activeGraph {x.height}).Reachable x.column y.column := by
…
```

lemma OAI.PlanarL1.Columns.Model.Point.shortest_sublevel line 194

Source documentation

Exact shortest paths to a fixed-height column stay in its distance sublevel after projection to column indices. This is the metric assertion underlying geo:sublevel, not merely a graph-connectivity assumption.

lemma shortest_sublevel (hJ : IsClosed J) (o y : M.Point J root) :
    ∃ p : M.Path J o.column y.column,
      p.length o.height y.height = dist o y ∧
      ∀ v ∈ p.word.support, ∃ hv : (M.activeGraph J).Reachable root v,
        dist o (⟨v, y.height, y.inBand, hv⟩ : M.Point J root) ≤ dist o y := by
…

def OAI.PlanarL1.Columns.Model.Point.sublevel line 213
Source documentation
The fixed-height radial sublevel in the active column graph. Columns outside the chosen component are absent, as for the source's value +∞.
```
def sublevel (o : M.Point J root) (H : ℝ) (hH : H ∈ J) (t : ℝ) : Set (Fin n) :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.mem_sublevel_iff line 217
lemma OAI.PlanarL1.Columns.Model.Point.sublevel_preconnected line 225
lemma OAI.PlanarL1.Columns.Model.Point.sublevel_connected line 247
Source documentation
Geometry, Lemma geo:sublevel, including the actual nonemptiness hypothesis and connectivity in the induced graph, not merely in the ambient component.
```
lemma sublevel_connected (hJ : IsClosed J) (o : M.Point J root)
    (H : ℝ) (hH : H ∈ J) (t : ℝ) (hne : (o.sublevel H hH t).Nonempty) :
    ((M.activeGraph J).induce (o.sublevel H hH t)).Connected := by
…
```

lemma OAI.PlanarL1.Columns.Model.Point.short_connector line 256

Source documentation

The short connector in the portal argument. We use the connected fixed-height sublevel at t - 12a; this changes the source's intermediate 13a estimate to 14a, still strictly below the required 100a separation.

lemma short_connector (hJ : IsClosed J) (o x : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a) (ht : 30 * a ≤ t)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (hx : t ≤ dist o (x.withHeight H hH)) (hnear : dist o x < t + a) :
    ∃ v ∈ o.sublevel H hH (t - 12 * a), ∃ T ∈ J,
      ∃ p : M.Path J x.column v, p.length x.height T ≤ 14 * a := by
…

lemma OAI.PlanarL1.Columns.Model.Point.no_three_far_entrances line 299

Source documentation

Quantitative exclusion behind the two-portals lemma: three entrance-range midpoints in a connected high set cannot be mutually more than 100 widths apart. No minor-exclusion or short-connector hypothesis is assumed.

lemma no_three_far_entrances (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    {C : Set (Fin n)} (hC : ((M.activeGraph J).induce C).Preconnected)
    (hhigh : ∀ z : M.Point J root, z.column ∈ C → t ≤ dist o (z.withHeight H hH))
    (x : Fin 3 → M.Point J root) (hxc : ∀ i, (x i).column ∈ C)
    (hnear : ∀ i, dist o (x i) < t + a)
    (hfar : Pairwise (fun i j => 100 * a < dist (x i) (x j))) : False := by
…

lemma OAI.PlanarL1.Columns.Model.Point.two_portal_midpoints line 355

Source documentation

Two entrances cover all entrance midpoints. The two chosen values may coincide, representing the one-portal case; both are actual entrances.

lemma two_portal_midpoints (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    {C : Set (Fin n)} (hC : ((M.activeGraph J).induce C).Preconnected)
    (hhigh : ∀ z : M.Point J root, z.column ∈ C → t ≤ dist o (z.withHeight H hH))
    {E : Set (M.Point J root)} (hne : E.Nonempty)
    (heC : ∀ x ∈ E, x.column ∈ C) (hnear : ∀ x ∈ E, dist o x < t + a) :
    ∃ p ∈ E, ∃ q ∈ E, ∀ x ∈ E, dist x p ≤ 100 * a ∨ dist x q ≤ 100 * a := by
…

lemma OAI.PlanarL1.Columns.Model.Point.two_portals line 393

Source documentation

Geometry geo:portals, the full-column covering conclusion with the stated 200a constant. The entrance-range hypothesis is derived from adjacency by dist_midpoints_le; the two portal centers are selected from E itself.

lemma two_portals (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    {C : Set (Fin n)} (hC : ((M.activeGraph J).induce C).Preconnected)
    (hhigh : ∀ z : M.Point J root, z.column ∈ C → t ≤ dist o (z.withHeight H hH))
    {E : Set (M.Point J root)} (hne : E.Nonempty)
    (heC : ∀ x ∈ E, x.column ∈ C) (hnear : ∀ x ∈ E, dist o x < t + a) :
    ∃ p ∈ E, ∃ q ∈ E, ∀ x : M.Point J root, x.withHeight H hH ∈ E →
      dist x p ≤ 200 * a ∨ dist x q ≤ 200 * a := by
…

def OAI.PlanarL1.Columns.Model.Point.superlevel line 417
Source documentation
Radial superlevels contain exactly the reachable columns whose midpoints have radial value at least the threshold.
```
def superlevel (o : M.Point J root) (H : ℝ) (hH : H ∈ J) (t : ℝ) : Set (Fin n) :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.mem_superlevel_iff line 421
def OAI.PlanarL1.Columns.Model.Point.entrances line 432
Source documentation
The actual entrance midpoints of a radial high component. The adjacent low column, rather than a separate entrance-range hypothesis, is part of the definition.
```
def entrances (o : M.Point J root) (H : ℝ) (hH : H ∈ J) (t : ℝ)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent) :
    Set (M.Point J root) :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.entrance_radial line 439

lemma OAI.PlanarL1.Columns.Model.Point.exit_superlevel line 458

Source documentation

Exit a high component along an attained shortest path. The final high column is an actual entrance. The estimate retains the distance to the radial threshold, and is the geometric input for both cell diameters and portal levels.

lemma exit_superlevel (hJ : IsClosed J) (o x : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ht : a / 2 < t)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent)
    (hx : x.column ∈ ColumnOrder.componentColumns C) :
    ∃ z : M.Point J root, z.withHeight H hH ∈ o.entrances H hH t C ∧
      dist x z ≤ dist o x - t + a / 2 := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.entrances_nonempty line 505

Source documentation

Nonempty radial high components have entrances above the initial half-width. This discharges the existence clause of geo:portals.

lemma entrances_nonempty (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ht : a / 2 < t)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent) :
    (o.entrances H hH t C).Nonempty := by
…

lemma OAI.PlanarL1.Columns.Model.Point.component_two_portals line 518

Source documentation

Geometry geo:portals with the actual radial component and actual entrances. In particular no covering or radial-range conclusion is assumed.

lemma component_two_portals (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent)
    (hne : (o.entrances H hH t C).Nonempty) :
    ∃ p ∈ o.entrances H hH t C, ∃ q ∈ o.entrances H hH t C,
      (t ≤ dist o p ∧ dist o p < t + a) ∧
      (t ≤ dist o q ∧ dist o q < t + a) ∧
      ∀ x : M.Point J root, x.withHeight H hH ∈ o.entrances H hH t C →
        dist x p ≤ 200 * a ∨ dist x q ≤ 200 * a := by
…

lemma OAI.PlanarL1.Columns.Model.Point.component_portal_cover line 538

Source documentation

The geodesic-to-root estimate behind radial cells: every point of a high component whose radial distance is bounded is close to a chosen portal.

lemma component_portal_cover (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a) (ht : a / 2 < t)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent) :
    ∃ p ∈ o.entrances H hH t C, ∃ q ∈ o.entrances H hH t C,
      ∀ x : M.Point J root, x.column ∈ ColumnOrder.componentColumns C →
        dist x p ≤ dist o x - t + 201 * a ∨
        dist x q ≤ dist o x - t + 201 * a := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

def OAI.PlanarL1.Columns.Model.Point.layer line 559
Source documentation
The half-open radial layer of the source. Its connected components, not components of the ambient graph, are the cell column sets.
```
def layer (o : M.Point J root) (H : ℝ) (hH : H ∈ J) (q D : ℝ) : Set (Fin n) :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.layer_subset_superlevel line 564
lemma OAI.PlanarL1.Columns.Model.Point.mem_layer_iff line 569

lemma OAI.PlanarL1.Columns.Model.Point.radial_cell_diameter line 580

Source documentation

The weak-diameter assertion of geo:cells for the literal full-column cell. Paths measuring distance may leave the cell, exactly as in the source.

lemma radial_cell_diameter (hJ : IsClosed J) (o : M.Point J root)
    {H a q D : ℝ} (hH : H ∈ J) (ha : 0 < a) (hthin : a ≤ D / 1000)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.layer H hH q D)).ConnectedComponent)
    (x y : M.Point J root) (hx : x.column ∈ ColumnOrder.componentColumns C)
    (hy : y.column ∈ ColumnOrder.componentColumns C) : dist x y ≤ 10 * D := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.radial_difference_le line 635
Source documentation
Changing to the fixed midheight costs at most one band width in any radial comparison. This also controls all zero-distance representatives.
```
lemma radial_difference_le (o x y : M.Point J root) {H a : ℝ} (hH : H ∈ J)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2) :
    |dist o (x.withHeight H hH) - dist o (y.withHeight H hH)| ≤ dist x y + a := by
…
```

lemma OAI.PlanarL1.Columns.Model.Point.path_radial_bound line 654

Source documentation

A column visited by a short switching path has a nearby radial midpoint. The conclusion uses the actual path prefix, rather than a shortest path constrained to a radial cell.

lemma path_radial_bound (o x y : M.Point J root) {H a : ℝ} (hH : H ∈ J)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2) (p : M.Path J x.column y.column)
    {i : Fin n} (hi : i ∈ p.word.support) :
    ∃ hr : (M.activeGraph J).Reachable root i,
      |dist o (⟨i, H, hH, hr⟩ : M.Point J root) - dist o (x.withHeight H hH)| ≤
        p.length x.height y.height + a := by
…

lemma OAI.PlanarL1.Columns.Model.Point.radial_cell_padding line 676

Source documentation

Deterministic padding in one actual radial layer. All representatives of all endpoints are covered because the lemma is stated on the pseudometric space of representatives.

lemma radial_cell_padding (o x y : M.Point J root) {H a q D ρ : ℝ}
    (hH : H ∈ J) (ha : 0 ≤ a) (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.layer H hH q D)).ConnectedComponent)
    (hx : x.column ∈ ColumnOrder.componentColumns C)
    (hlow : q + ρ + 2 * a < dist o (x.withHeight H hH))
    (hupp : dist o (x.withHeight H hH) < q + D - ρ - 2 * a)
    (p : M.Path J x.column y.column) (hp : p.length x.height y.height ≤ ρ) :
    y.column ∈ ColumnOrder.componentColumns C := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.radial_ball_padding line 690
def OAI.PlanarL1.Columns.Model.Point.frontier line 702
Source documentation
The literal full-column frontier of a column cell in the active graph.
```
def frontier (C : Set (Fin n)) : Set (Fin n) :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.frontier_radial line 707
Source documentation
A frontier midpoint is within one width of a layer threshold. The neighbor cannot be in the same layer, since the cell is a component there.
```
lemma frontier_radial (o z : M.Point J root) {H a q D : ℝ} (hH : H ∈ J)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.layer H hH q D)).ConnectedComponent)
    (hz : z.column ∈ frontier (M := M) (J := J) (ColumnOrder.componentColumns C)) :
…
```
Mentions: OAI.PlanarL1.Columns.Model.Point.frontier, OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.radial_frontier_distance line 733

Source documentation

Exact strict avoidance of the frontier, the second assertion of geo:padding. The empty-frontier case is automatic, not assigned distance 0.

lemma radial_frontier_distance (o x z : M.Point J root) {H a q D ρ : ℝ}
    (hH : H ∈ J) (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.layer H hH q D)).ConnectedComponent)
    (hlow : q + ρ + 2 * a < dist o (x.withHeight H hH))
    (hupp : dist o (x.withHeight H hH) < q + D - ρ - 2 * a)
    (hz : z.column ∈ frontier (M := M) (J := J) (ColumnOrder.componentColumns C)) :
…

Mentions: OAI.PlanarL1.Columns.Model.Point.frontier, OAI.PlanarL1.ColumnOrder.componentColumns

def OAI.PlanarL1.Columns.Model.Point.columnMap line 748
Source documentation
Every fixed column is an isometric copy of its allowed height interval.
```
def columnMap (i : Fin n) (hi : (M.activeGraph J).Reachable root i) : J → M.Point J root :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.columnMap_isometry line 751
lemma OAI.PlanarL1.Columns.Model.Point.fullColumns_compact line 760
Source documentation
Compactness of any full-column subset in a compact band, including the literal radial cells and their frontiers. This argument works before taking the separation quotient and does not require a false Hausdorff assumption.
```
lemma fullColumns_compact (hJ : IsCompact J) (C : Set (Fin n)) :
    IsCompact {x : M.Point J root | x.column ∈ C} := by
…
```
lemma OAI.PlanarL1.Columns.Model.Point.frontier_minimizer line 780
Source documentation
A continuous scalar frontier constraint attains its infimum whenever there is a frontier point. Used by the main raise-or-descend test.
```
lemma frontier_minimizer (hJ : IsCompact J) (C : Set (Fin n))
    (s : M.Point J root → ℝ) (hs : Continuous s) (x : M.Point J root) (c : ℝ)
    (hne : ∃ z : M.Point J root, z.column ∈ frontier (M := M) (J := J) C) :
…
```
Mentions: OAI.PlanarL1.Columns.Model.Point.frontier

lemma OAI.PlanarL1.Columns.Model.Point.exists_between line 796

Source documentation

The metric interpolation property of an actual attained shortest path. This is the geodesic fact used by the small-ball and descending-path arguments.

lemma exists_between (hJ : IsClosed J) (hconv : Set.OrdConnected J)
    (x y : M.Point J root) {ℓ : ℝ} (hℓ : 0 ≤ ℓ) (hlen : ℓ ≤ dist x y) :
    ∃ z : M.Point J root, dist x z = ℓ ∧ dist z y = dist x y - ℓ := by
…

lemma OAI.PlanarL1.Columns.Model.Point.descent_along_shortest line 814

Source documentation

Every point on a shortest descending path retains the endpoint's deficit bound. This is main:ray-prefix, expressed by exact arclength distances.

lemma descent_along_shortest {s : M.Point J root → ℝ} {ε : ℝ}
    (hs : ∀ u v, s u - s v ≤ dist u v) (x z v : M.Point J root)
    (hshort : dist x v + dist v z = dist x z)
    (hdrop : s z ≤ s x - dist x z + ε) :
    s v ≤ s x - dist x v + ε := by
…

def OAI.PlanarL1.Columns.Model.Point.ballColumns line 824
Source documentation
All representatives of the intrinsic closed ball, projected to columns. Using representatives includes columns identified by zero-length paths.
```
def ballColumns (x : M.Point J root) (ρ : ℝ) : Set (Fin n) :=
…
```
lemma OAI.PlanarL1.Columns.Model.Point.mem_ballColumns line 827
lemma OAI.PlanarL1.Columns.Model.Point.path_ballColumns line 830
lemma OAI.PlanarL1.Columns.Model.Point.ballColumns_preconnected line 844
Source documentation
The projection of an actual closed ball is induced-connected. This is not an assumed graph property in the local interpolation argument.
```
lemma ballColumns_preconnected (hJ : IsClosed J) (x : M.Point J root) (ρ : ℝ) :
    ((M.activeGraph J).induce (x.ballColumns ρ)).Preconnected := by
…
```
lemma OAI.PlanarL1.Columns.Model.Point.ballColumns_nonempty line 860

lemma OAI.PlanarL1.Columns.Model.Point.ball_radial_spread line 865

Source documentation

The sharper 2ρ+a version of the source's 2ρ+2a radial spread.

lemma ball_radial_spread (o x y z : M.Point J root) {H a ρ : ℝ} (hH : H ∈ J)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (hy : dist x y ≤ ρ) (hz : dist x z ≤ ρ) :
    |dist o (y.withHeight H hH) - dist o (z.withHeight H hH)| ≤ 2 * ρ + a := by
…

lemma OAI.PlanarL1.Columns.Model.Point.exit_superlevel_to line 877

Source documentation

A shortest path to any point outside a high component reaches an actual entrance within its total length. Unlike exit_superlevel, no radial decrease to the root is needed.

lemma exit_superlevel_to (hJ : IsClosed J) (o x y : M.Point J root)
    {H t : ℝ} (hH : H ∈ J)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent)
    (hx : x.column ∈ ColumnOrder.componentColumns C)
    (hy : y.column ∉ ColumnOrder.componentColumns C) :
    ∃ z : M.Point J root, z.withHeight H hH ∈ o.entrances H hH t C ∧
      dist x z ≤ dist x y := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.near_component_portal line 905

Source documentation

Any point in a high component and within L of a point outside it is within L+200a of one of its two fixed entrance portals.

lemma near_component_portal (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ha : 0 < a)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent)
    (hne : (o.entrances H hH t C).Nonempty) :
    ∃ p ∈ o.entrances H hH t C, ∃ q ∈ o.entrances H hH t C,
      ∀ x y : M.Point J root, x.column ∈ ColumnOrder.componentColumns C →
        y.column ∉ ColumnOrder.componentColumns C →
        dist x p ≤ dist x y + 200 * a ∨ dist x q ≤ dist x y + 200 * a := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.ball_radial_minimum line 925

Source documentation

The fixed-height radial profile attains its minimum among the finite set of columns represented in a nonempty closed ball.

lemma ball_radial_minimum (o x : M.Point J root) {H ρ : ℝ} (hH : H ∈ J)
    (hρ : 0 ≤ ρ) :
    ∃ y : M.Point J root, dist x y ≤ ρ ∧
      ∀ z : M.Point J root, dist x z ≤ ρ →
        dist o (y.withHeight H hH) ≤ dist o (z.withHeight H hH) := by
…

lemma OAI.PlanarL1.Columns.Model.Point.ball_two_layers line 949

Source documentation

The exact geometric content of the one-chain small-ball argument: there are only two consecutive radial layer depths in a sufficiently small ball, and all its representatives lie in one node at the lower depth.

lemma ball_two_layers (hJ : IsClosed J) (o x : M.Point J root)
    {H a ρ δ : ℝ} (hH : H ∈ J) (hρ : 0 ≤ ρ) (hδ : 0 < δ)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2) (hsmall : 2 * ρ + a < δ) :
    ∃ k : ℕ, ∃ y : M.Point J root,
      ∃ C : ((M.activeGraph J).induce (o.superlevel H hH (k * δ))).ConnectedComponent,
        dist x y ≤ ρ ∧ dist o (y.withHeight H hH) < (k + 1) * δ ∧
        (∀ z : M.Point J root, dist x z ≤ ρ →
          z.column ∈ ColumnOrder.componentColumns C ∧
          (k : ℝ) * δ ≤ dist o (z.withHeight H hH) ∧
          dist o (z.withHeight H hH) < (k + 2) * δ) := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.Columns.Model.Point.mem_zero_component line 986
Source documentation
At depth zero the single radial node contains every reachable column, including the chosen basepoint column.
```
lemma mem_zero_component (o x : M.Point J root) {H : ℝ} (hH : H ∈ J)
    (C : ((M.activeGraph J).induce (o.superlevel H hH 0)).ConnectedComponent) :
    x.column ∈ ColumnOrder.componentColumns C := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.componentColumns
structure OAI.PlanarL1.Columns.Model.Point.PortalData line 999
Source documentation
Two fixed geometric portals, with all bounds required by the actual interpolation hierarchy. Repeated portals encode the one-portal case.
```
structure PortalData (o : M.Point J root) (H : ℝ) (hH : H ∈ J) (a t : ℝ)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent) where
…
```

lemma OAI.PlanarL1.Columns.Model.Point.portalData_nonempty line 1017

Source documentation

The portal data are constructed from the proved geometry, including the root convention; they are not assumptions on the interpolation input.

lemma portalData_nonempty (hJ : IsClosed J) (o : M.Point J root)
    {H a t : ℝ} (hH : H ∈ J) (ho : o.height = H) (ha : 0 < a)
    (hhalf : ∀ T ∈ J, |H - T| ≤ a / 2) (ht : t = 0 ∨ a / 2 < t)
    (C : ((M.activeGraph J).induce (o.superlevel H hH t)).ConnectedComponent) :
    Nonempty (o.PortalData H hH a t C) := by
…

lemma OAI.PlanarL1.Columns.Model.Point.PortalData.near_of_radial line 1050
Source documentation
Layer points and points only slightly beyond its top are close to a fixed portal. The radial allowance is kept explicit for child portals.
```
lemma near_of_radial (K : o.PortalData H hH a t C)
    {δ e : ℝ} (x : M.Point J root) (hx : x.column ∈ ColumnOrder.componentColumns C)
    (hr : dist o x ≤ t + δ + e) :
    min (dist x K.left) (dist x K.right) ≤ δ + e + 201 * a := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.componentColumns
lemma OAI.PlanarL1.Columns.Model.Point.PortalData.near_layer line 1056

lemma OAI.PlanarL1.Columns.Model.Point.PortalData.near_exit line 1069

Source documentation

A near-exit point is in the equality collar of these same portals; there is no resampling or reselecting a different portal pair.

lemma near_exit (K : o.PortalData H hH a t C) (hJ : IsClosed J)
    (x y : M.Point J root) (hx : x.column ∈ ColumnOrder.componentColumns C)
    (hy : y.column ∉ ColumnOrder.componentColumns C) :
    min (dist x K.left) (dist x K.right) ≤ dist x y + 200 * a := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns