OAI/Combinatorics/PlanarL1/Crossings.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.ColumnOrder.overlapping_words line 12

   Source documentation

   The combinatorial core of overlapping traversals: a path reaching a middle profile value intersects any path crossing that value if each switch has small profile error. Monotonicity is needed only on their common arc.

   lemma overlapping_words {n : ℕ} {G : SimpleGraph (Fin n)}
       (hnc : Noncrossing G) {S : Set (Fin n)} {q : Fin n → ℝ}
       (hq : MonotoneOn q S) {x x' y y' i : Fin n}
       (p : G.Walk x x') (r : G.Walk y y')
       (hp : ∀ v ∈ p.support, v ∈ S) (hr : ∀ v ∈ r.support, v ∈ S)
       (hi : i ∈ p.support) {δ : ℝ}
       (hx : q x + δ < q i) (hy : q y < q i) (hy' : q i < q y')
       (hs : ∀ e ∈ r.darts, |q e.fst - q e.snd| ≤ δ) :
       ∃ v, v ∈ p.support ∧ v ∈ r.support := by
   …

   Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

2. lemma OAI.PlanarL1.Columns.Model.Path.exists_trace_of_mem_support line 61
3. lemma OAI.PlanarL1.Columns.Model.Field.profile_error line 81
4. lemma OAI.PlanarL1.Columns.Model.Field.profile_switch_error line 88
5. lemma OAI.PlanarL1.Columns.Model.Field.overlap_columns line 102

   Source documentation

   Ordered overlap with an arbitrary cut of the circular order. The same proof applies to the other arc by negating the field and reversing paths. Its conclusion is actual shared-column support, prior to metric estimates.

   lemma overlap_columns (F : M.Field J L) (hJ : Set.OrdConnected J)
       (e : Fin n ≃ Fin n) (hnc : ColumnOrder.Noncrossing ((M.activeGraph J).comap e))
       (S : Set (Fin n)) (T : J)
       (ho : MonotoneOn (fun i => F.value (e i) T) S)
       {η u v : ℝ} (hw : ∀ a ∈ J, ∀ b ∈ J, |a-b| ≤ η)
       (hgap : 8*(L*η) < v-u)
       {i j k l : Fin n} (p : M.Path J i j) (r : M.Path J k l)
       (a b c d : J)
       (hp : ∀ z ∈ p.word.support, e.symm z ∈ S)
       (hr : ∀ z ∈ r.word.support, e.symm z ∈ S)
       (ha : F.value i a ≤ u) (hb : v ≤ F.value j b)
       (hc : F.value k c ≤ u) (hd : v ≤ F.value l d) :
   …

   Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

6. lemma OAI.PlanarL1.ColumnOrder.first_exit line 166

   Source documentation

   Stop at the first vertex outside a set. The constructed walk consists only of original visited columns, and its last step crosses the set boundary.

   lemma first_exit {V : Type*} {G : SimpleGraph V} {S : Set V} {x y : V}
       (p : G.Walk x y) (hx : x ∈ S) (hy : y ∉ S) :
       ∃ a b, G.Adj a b ∧ a ∈ S ∧ b ∉ S ∧
         ∃ r : G.Walk x b,
           (∀ v ∈ r.support, v ∈ p.support) ∧
           (∀ v ∈ r.support, v ∈ S ∨ v = b) := by
   …

7. lemma OAI.PlanarL1.ColumnOrder.traverse_band line 201

   Source documentation

   A discrete traversal of a value band. Every visited column lies in the band enlarged by one switch error; no continuous path-parameter choice or first/last hitting time is postulated.

   lemma traverse_band {V : Type*} {G : SimpleGraph V} (q : V → ℝ) {δ u v : ℝ}
       (hδ : 0 ≤ δ) (huv : u < v) (hedge : ∀ {a b}, G.Adj a b → |q a-q b| ≤ δ)
       {x y : V} (p : G.Walk x y) (hx : q x ≤ u) (hy : v ≤ q y) :
       ∃ a b, ∃ r : G.Walk a b,
         q a ≤ u ∧ v ≤ q b ∧
         (∀ z ∈ r.support, z ∈ p.support) ∧
         (∀ z ∈ r.support, u-δ ≤ q z ∧ q z ≤ v+δ) := by
   …

8. def OAI.PlanarL1.Columns.Model.Path.widen line 252

   Source documentation

   The same finite path is permitted in a larger band.

   def widen (hJI : J ⊆ I) {i j : Fin n} : M.Path J i j → M.Path I i j
     | .nil i => .nil i
     | .cons H hH hs p => .cons H (hJI hH) hs (widen hJI p)

9. lemma OAI.PlanarL1.Columns.Model.Path.length_widen line 256
10. def OAI.PlanarL1.Columns.Model.Point.NearColumns line 270

    Source documentation

    Geometric control of visits to a set of columns. The witnesses are actual points at heights in J and actual ambient-band distances from the center.

    def NearColumns (x : M.Point I root) (J : Set ℝ) (A : ℝ) (S : Set (Fin n)) : Prop :=
    …

11. lemma OAI.PlanarL1.Columns.Model.Point.NearColumns.mono line 273
12. lemma OAI.PlanarL1.Columns.Model.Point.NearColumns.union line 277
13. lemma OAI.PlanarL1.Columns.Model.Point.near_path line 283

    Source documentation

    Every visited column of a path of length A from x has a point genuinely reachable within A, even when the ambient metric permits leaving J.

    lemma near_path (hJI : J ⊆ I) (x : M.Point I root) (hx : x.height ∈ J)
        {j : Fin n} (p : M.Path J x.column j) {H A : ℝ} (hH : H ∈ J)
        (hA : p.length x.height H ≤ A) :
        x.NearColumns J A {v | v ∈ p.word.support} := by
    …

14. lemma OAI.PlanarL1.Columns.Model.Point.dist_le_of_near_intersection line 300

    Source documentation

    Metric completion of the overlapping-traversal argument. Only one vertical transfer is needed, hence eta rather than the source's 2 eta.

    lemma dist_le_of_near_intersection (x y : M.Point I root) {A B η : ℝ}
        {S T : Set (Fin n)} (hx : x.NearColumns J A S) (hy : y.NearColumns J B T)
        (hw : ∀ a ∈ J, ∀ b ∈ J, |a-b| ≤ η) {v : Fin n} (hvS : v ∈ S) (hvT : v ∈ T) :
        dist x y ≤ A+B+η := by
    …

15. lemma OAI.PlanarL1.ColumnOrder.ordered_chord_barrier line 321

    Source documentation

    A crosslink joining the two monotone arcs separates all strict lower profile values from all strict upper values. This uses noncrossing of the ambient graph, not an assumed connectivity of a scalar level set.

    lemma ordered_chord_barrier {n : ℕ} {G : SimpleGraph (Fin n)}
        (hnc : Noncrossing G) (f : Fin n → ℝ) (m : Fin n)
        (hleft : ∀ i j, i ≤ j → j ≤ m → f i ≤ f j)
        (hright : ∀ i j, m ≤ i → i ≤ j → f j ≤ f i)
        {a b x y : Fin n} (ham : a ≤ m) (hmb : m ≤ b)
        (hab : G.Adj a b) (heq : f a = f b)
        (p : G.Walk x y) (hx : f x < f a) (hy : f a < f y) :
        a ∈ p.support ∨ b ∈ p.support := by
    …

    Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

16. lemma OAI.PlanarL1.Columns.Model.Field.ordered_maximum line 356
17. lemma OAI.PlanarL1.Columns.Model.Field.arcSign_one_lt line 363
18. lemma OAI.PlanarL1.Columns.Model.Field.arcSign_neg_one_gt line 371
19. lemma OAI.PlanarL1.Columns.Model.Field.crosslink_barrier line 384

    Source documentation

    Actual crosslink barrier for arbitrary finite paths in any band. The crosslink itself may be outside that band, as required by the empty-wall rectangle argument.

    lemma crosslink_barrier (F : M.Field I L) {a b : Fin (k+1)} (ho : F.OrderedFrom a b)
        (H : I) {u v : Fin (k+1)} (hs : H.val ∈ M.heights u v)
        (hu : arcSign a b u = 1) (hv : arcSign a b v = -1)
        {x y : Fin (k+1)} (p : (M.activeGraph J).Walk x y)
        (hx : F.value x H < F.value u H) (hy : F.value u H < F.value y H) :
        u ∈ p.support ∨ v ∈ p.support := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.Field.arcSign

20. lemma OAI.PlanarL1.Columns.Model.Point.dist_le_of_near_link line 417

    Source documentation

    Two controlled column sets each hitting an endpoint of the same actual link can be joined through that link at its prescribed height.

    lemma dist_le_of_near_link (x y : M.Point I root) {A B D H : ℝ}
        {S T : Set (Fin n)} (hx : x.NearColumns J A S) (hy : y.NearColumns J B T)
        (hD : ∀ t ∈ J, |t-H| ≤ D) (hH : H ∈ I)
        {u v : Fin n} (hlink : H ∈ M.heights u v)
        (hp : u ∈ S ∨ v ∈ S) (hq : u ∈ T ∨ v ∈ T) :
        dist x y ≤ A+B+2*D := by
    …

21. lemma OAI.PlanarL1.Columns.Model.Field.wall_traversal_distance line 467

    Source documentation

    Empty-wall rectangle, in its geometric form before inserting the source constants. A hypothetical wall point between both controlled traversals creates a quantitatively short ambient path.

    lemma wall_traversal_distance (F : M.Field I L) {a b : Fin (k+1)}
        (ho : F.OrderedFrom a b) (H : I) {c A B D : ℝ}
        (hw : (c,H.val) ∈ F.wall a b)
        (x y : M.Point I root) {x₀ x₁ y₀ y₁ : Fin (k+1)}
        (p : (M.activeGraph J).Walk x₀ x₁) (q : (M.activeGraph J).Walk y₀ y₁)
        (hp : x.NearColumns J A {v | v ∈ p.support})
        (hq : y.NearColumns J B {v | v ∈ q.support})
        (hD : ∀ t ∈ J, |t-H.val| ≤ D)
        (hx₀ : F.value x₀ H < c) (hx₁ : c < F.value x₁ H)
        (hy₀ : F.value y₀ H < c) (hy₁ : c < F.value y₁ H) :
        dist x y ≤ A+B+2*D := by
    …

22. abbrev OAI.PlanarL1.Columns.Model.Field.eval line 504
23. structure OAI.PlanarL1.Columns.Model.Field.Excursions line 509

    Source documentation

    The genuine pair of short low/high paths in : no scalar separation or arc conclusion is included as an assumption.

    structure Excursions (F : M.Field I L) (hJI : J ⊆ I) (z : M.Point I root) (A ε : ℝ) where
    …

24. def OAI.PlanarL1.Columns.Model.Field.Excursions.traversal line 526
25. lemma OAI.PlanarL1.Columns.Model.Field.Excursions.near_traversal line 530
26. lemma OAI.PlanarL1.Columns.Model.Field.Excursions.low_profile line 541
27. lemma OAI.PlanarL1.Columns.Model.Field.Excursions.high_profile line 551
28. lemma OAI.PlanarL1.Columns.Model.Field.empty_rectangle line 565

    Source documentation

    The closed wall-free rectangle with the manuscript's exact numerical margins, uniform in every field, every finite column model and every size.

    lemma empty_rectangle {k : ℕ} {M : Model (k+1)} {I J : Set ℝ} {root : Fin (k+1)}
        (F : M.Field I 4) {a b : Fin (k+1)} (ho : F.OrderedFrom a b)
        {R η : ℝ} (hR : 0 < R) (hη : η ≤ R/1000000)
        (hJI : J ⊆ I) (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ η)
        (x y : M.Point I root)
        (Ex : F.Excursions hJI x (2*R) (2*R/5))
        (Ey : F.Excursions hJI y (2*R) (2*R/5))
        (hclose : |F.eval x-F.eval y| ≤ R/1000)
        (hfar : 4*R+2*(R/50+η) < dist x y)
        (H : I) {c : ℝ} (hc : |c-F.eval x| ≤ R/5) (hH : |H.val-x.height| ≤ R/50) :
        (c,H.val) ∉ F.wall a b := by
    …

    Mentions: OAI.PlanarL1.Columns.Model

29. lemma OAI.PlanarL1.Columns.Model.Field.infDist_lower_of_rectangle line 597

    Source documentation

    Quantitative wall avoidance implies an infimum-distance bound at any center whose max-norm ball fits into the verified empty rectangle.

    lemma infDist_lower_of_rectangle {k : ℕ} {M : Model (k+1)} {I : Set ℝ} {L : NNReal}
        (F : M.Field I L) (a b : Fin (k+1)) (T : I)
        {s h U V r : ℝ}
        (hempty : ∀ (c : ℝ) (H : I), |c-s| ≤ U → |H.val-h| ≤ V → (c,H.val) ∉ F.wall a b)
        (i : Fin (k+1)) (hU : |F.value i T-s|+r ≤ U) (hV : |T.val-h|+r ≤ V) :
        r ≤ Metric.infDist (F.value i T,T.val) (F.wall a b) := by
    …

    Mentions: OAI.PlanarL1.Columns.Model

30. lemma OAI.PlanarL1.ColumnOrder.overlapping_ranges line 626

    Source documentation

    Discrete profile intervals suffice for overlap. The midpoint visit is constructed by stopping at the first exiting column, including its switch error.

    lemma overlapping_ranges {n : ℕ} {G : SimpleGraph (Fin n)} (hnc : Noncrossing G)
        {S : Set (Fin n)} {q : Fin n → ℝ} (hq : MonotoneOn q S)
        {δ u v : ℝ} (hgap : 2*δ < v-u)
        (hedge : ∀ {a b}, G.Adj a b → |q a-q b| ≤ δ)
        {x x' y y' : Fin n} (p : G.Walk x x') (r : G.Walk y y')
        (hp : ∀ z ∈ p.support, z ∈ S) (hr : ∀ z ∈ r.support, z ∈ S)
        (hx : q x ≤ u) (hx' : v ≤ q x') (hy : q y ≤ u) (hy' : v ≤ q y')
        (hδ : 0 ≤ δ) : ∃ z, z ∈ p.support ∧ z ∈ r.support := by
    …

    Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

31. lemma OAI.PlanarL1.ColumnOrder.overlapping_ranges_anti line 645
32. lemma OAI.PlanarL1.ColumnOrder.walk_label_const line 666
33. lemma OAI.PlanarL1.Columns.Model.Field.same_arc_overlap line 692

    Source documentation

    Profile overlap on either open arc; the cyclic relabelling and the antitone second arc are both explicit.

    lemma same_arc_overlap (F : M.Field I L) {a b : Fin (k+1)}
        (ho : F.OrderedFrom a b) (H : I) {δ u v σ : ℝ}
        (hσ : σ = 1 ∨ σ = -1) (hδ : 0 ≤ δ) (hgap : 2*δ < v-u)
        (hedge : ∀ {i j}, (M.activeGraph J).Adj i j → |F.value i H-F.value j H| ≤ δ)
        {x x' y y' : Fin (k+1)} (p : (M.activeGraph J).Walk x x')
        (r : (M.activeGraph J).Walk y y')
        (hp : ∀ z ∈ p.support, arcSign a b z = σ)
        (hr : ∀ z ∈ r.support, arcSign a b z = σ)
        (hx : F.value x H ≤ u) (hx' : v ≤ F.value x' H)
        (hy : F.value y H ≤ u) (hy' : v ≤ F.value y' H) :
        ∃ z, z ∈ p.support ∧ z ∈ r.support := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.Field.arcSign

34. lemma OAI.PlanarL1.Columns.Model.Field.strip_arc_const line 742

    Source documentation

    An empty wall rectangle rules out every boundary column and every side-changing active switch in a slightly narrower reference-profile strip.

    lemma strip_arc_const (F : M.Field I L) (a b : Fin (k+1)) (T : I)
        (hJI : J ⊆ I) {s h U V W D : ℝ}
        (hempty : ∀ (c : ℝ) (H : I), |c-s| ≤ U → |H.val-h| ≤ V → (c,H.val) ∉ F.wall a b)
        (hT : |T.val-h| ≤ V) (hD : ∀ t ∈ J, |t-T.val| ≤ D)
        (hV : ∀ t ∈ J, |t-h| ≤ V) (hW : W+L*D ≤ U) (hD0 : 0 ≤ D) :
        (∀ i, |F.value i T-s| ≤ W → arcSign a b i ≠ 0) ∧
        (∀ {i j}, (M.activeGraph J).Adj i j → |F.value i T-s| ≤ W →
          |F.value j T-s| ≤ W → arcSign a b i = arcSign a b j) := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.Field.arcSign

35. lemma OAI.PlanarL1.ColumnOrder.center_exit_band line 771

    Source documentation

    A center-to-exit traversal of a scalar strip, with the visited center retained and the support enlarged by only one edge error.

    lemma center_exit_band {V : Type*} {G : SimpleGraph V} (q : V → ℝ)
        {s r c δ : ℝ} (hcr : c < r) (hδ : 0 ≤ δ)
        (hedge : ∀ {a b}, G.Adj a b → |q a-q b| ≤ δ)
        {x y : V} (p : G.Walk x y) (hx : |q x-s| ≤ c) (hy : s+r ≤ q y) :
        ∃ a b, ∃ t : G.Walk a b,
          (∀ z ∈ t.support, z ∈ p.support) ∧ x ∈ t.support ∧
          (∀ z ∈ t.support, |q z-s| ≤ r+δ) ∧
          ((q a ≤ s+c ∧ s+r ≤ q b) ∨ (q a ≤ s-r ∧ s-c ≤ q b)) := by
    …

36. lemma OAI.PlanarL1.ColumnOrder.two_lane_centers line 815

    Source documentation

    Two disjoint low-to-high traversals, each issuing from a central column, must have opposite central labels when the strip has precisely two lanes and same-lane overlapping ranges intersect. This is the finite-word form of the last two paragraphs of 's two-side argument.

    lemma two_lane_centers {V : Type*} {G : SimpleGraph V} (q label : V → ℝ)
        {s r c δ : ℝ} (hc : 0 ≤ c) (hδ : 0 ≤ δ) (hgap : 2*δ < r-c)
        (hedge : ∀ {a b}, G.Adj a b → |q a-q b| ≤ δ)
        (hlabels : ∀ z, |q z-s| ≤ r+δ → label z = 1 ∨ label z = -1)
        (hconstant : ∀ {a b}, G.Adj a b → |q a-s| ≤ r+δ → |q b-s| ≤ r+δ → label a = label b)
        (hover : ∀ {a b d e : V} (p : G.Walk a b) (t : G.Walk d e) {u v σ : ℝ},
          σ = 1 ∨ σ = -1 → 2*δ < v-u →
          (∀ z ∈ p.support, label z = σ) → (∀ z ∈ t.support, label z = σ) →
          q a ≤ u → v ≤ q b → q d ≤ u → v ≤ q e →
          ∃ z, z ∈ p.support ∧ z ∈ t.support)
        {x₀ x₁ y₀ y₁ x y : V} (P : G.Walk x₀ x₁) (Q : G.Walk y₀ y₁)
        (U : G.Walk x x₁) (Vw : G.Walk y y₁)
    …

37. def OAI.PlanarL1.Columns.Model.Field.restrict line 901
38. lemma OAI.PlanarL1.Columns.Model.Field.two_side_arcs line 912

    Source documentation

    Quantitative opposite-arc conclusion from genuine short excursions. The only extra displayed inequality says exactly that the constructed short join would contradict the given separation; at R=10^-8 it follows from d≥1.

    lemma two_side_arcs (F : M.Field I 4) {a b : Fin (k+1)} (ho : F.OrderedFrom a b)
        {root : Fin (k+1)} {R η : ℝ} (hR : 0 < R) (hη : η ≤ R/1000000)
        (hJI : J ⊆ I) (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ η)
        (x y : M.Point I root)
        (Ex : F.Excursions hJI x (2*R) (2*R/5))
        (Ey : F.Excursions hJI y (2*R) (2*R/5))
        (hclose : |F.eval x-F.eval y| ≤ R/1000)
        (hfar : 4*R+2*(R/50+η) < dist x y) :
        arcSign a b x.column ≠ 0 ∧ arcSign a b y.column ≠ 0 ∧
        arcSign a b x.column ≠ arcSign a b y.column ∧
        R/100 ≤ Metric.infDist (F.eval x,x.height) (F.wall a b) ∧
        R/100 ≤ Metric.infDist (F.eval y,y.height) (F.wall a b) := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.Field.arcSign

39. lemma OAI.PlanarL1.Columns.Model.Field.abs_add_eq_abs_sub_of_opposite line 989
40. theorem OAI.PlanarL1.Columns.Model.Field.two_side line 1001

    Source documentation

    Full quantitative two-side lemma (, ord:two-side) in intrinsic band coordinates. An ambient application uses the source hypothesis d_I=d.

    theorem two_side (F : M.Field I 4) {a b : Fin (k+1)} (ho : F.OrderedFrom a b)
        (hI : IsClosed I) {root : Fin (k+1)} {η : ℝ}
        (hη : η ≤ (1:ℝ)/100000000/1000000)
        (hJI : J ⊆ I) (hw : ∀ s ∈ J, ∀ t ∈ J, |s-t| ≤ η)
        (x y : M.Point I root) (hlo : 1 ≤ dist x y) (hhi : dist x y ≤ 2)
        (Ex : F.Excursions hJI x (2*((1:ℝ)/100000000)) (2*((1:ℝ)/100000000)/5))
        (Ey : F.Excursions hJI y (2*((1:ℝ)/100000000)) (2*((1:ℝ)/100000000)/5))
        (hclose : |F.eval x-F.eval y| ≤ (1:ℝ)/100000000/1000) :
        (F.transverse (by norm_num) a b).eval x * (F.transverse (by norm_num) a b).eval y < 0 ∧
        (1:ℝ)/100000000/100 ≤ |(F.transverse (by norm_num) a b).eval x| ∧
        (1:ℝ)/100000000/100 ≤ |(F.transverse (by norm_num) a b).eval y| ∧
        |(F.transverse (by norm_num) a b).eval x| ≤ 8 ∧
    …

    Mentions: OAI.PlanarL1.Columns.Model.Field.eval