Noncrossing.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Noncrossing column words

These are the exact combinatorial separation tools used in the surviving-seed packing argument. The circular set has been cut at index 0.

def OAI.PlanarL1.ColumnOrder.Noncrossing line 15
Source documentation
No two links have four alternating, distinct endpoints in cyclic order.
```
def Noncrossing {n : ℕ} (G : SimpleGraph (Fin n)) : Prop :=
…
```
lemma OAI.PlanarL1.ColumnOrder.noncrossing_comap_rotate line 19
lemma OAI.PlanarL1.ColumnOrder.noncrossing_comap_iterate line 43
lemma OAI.PlanarL1.ColumnOrder.noncrossing_comap_cycle line 51

theorem OAI.PlanarL1.ColumnOrder.adj_stays_between line 59

Source documentation

An edge cannot leave the strict interior of a chord without meeting one of the chord endpoints.

theorem adj_stays_between {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {a b x y : Fin n} (hab : G.Adj a b)
    (hax : a < x) (hxb : x < b) (hxy : G.Adj x y)
    (hya : y ≠ a) (hyb : y ≠ b) : a < y ∧ y < b := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

theorem OAI.PlanarL1.ColumnOrder.walk_stays_between line 73
Source documentation
A column word avoiding the endpoints of a chord remains on its starting strict side. This is the induction behind the chord-separation lemma.
```
theorem walk_stays_between {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {a b x y : Fin n} (hab : G.Adj a b)
    (p : G.Walk x y) (hx : a < x ∧ x < b)
    (ha : a ∉ p.support) (hb : b ∉ p.support) : a < y ∧ y < b := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing
theorem OAI.PlanarL1.ColumnOrder.chord_separation line 93
Source documentation
Geometry, Lemma geo:chord-separation, with a cut in the circular order outside the chosen strict interval. It applies to paths as well as walks.
```
theorem chord_separation {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {a b x y : Fin n} (hab : G.Adj a b)
    (p : G.Walk x y) (hx : a < x ∧ x < b)
    (hy : y < a ∨ b < y) : a ∈ p.support ∨ b ∈ p.support := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing
def OAI.PlanarL1.ColumnOrder.JumpsAcross line 103
Source documentation
Occurrence of a step of the word that skips the specified index strictly.
```
def JumpsAcross {n : ℕ} {G : SimpleGraph (Fin n)} (i : Fin n)
    {x y : Fin n} (p : G.Walk x y) : Prop :=
…
```
theorem OAI.PlanarL1.ColumnOrder.visits_or_skips line 109
Source documentation
Geometry, Lemma geo:skipping: passage from one side of an index to the other either visits it or has a step jumping strictly across it.
```
theorem visits_or_skips {n : ℕ} {G : SimpleGraph (Fin n)} {i x y : Fin n}
    (p : G.Walk x y) (hx : x < i) (hy : i < y) :
    i ∈ p.support ∨ JumpsAcross i p := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.JumpsAcross
lemma OAI.PlanarL1.ColumnOrder.adj_between_connected line 133
Source documentation
A connected set is a barrier between any two of its vertices in the linear order. The edge and the set's connecting paths may belong to different subgraphs; only noncrossing in the common ambient graph matters.
```
lemma adj_between_connected {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {S : Set (Fin n)} (hS : (G.induce S).Preconnected)
    {a b x y : Fin n} (ha : a ∈ S) (hb : b ∈ S)
    (hx : a < x ∧ x < b) (hxy : G.Adj x y) (hxs : x ∉ S) (hys : y ∉ S) :
    a < y ∧ y < b := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing
lemma OAI.PlanarL1.ColumnOrder.walk_same_gap line 162
Source documentation
Paths avoiding a connected set have constant membership in every interval whose endpoints belong to that set. This is the cut-independent content of geo:gap: such a path stays in one open circular gap.
```
lemma walk_same_gap {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {S : Set (Fin n)} (hS : (G.induce S).Preconnected)
    {x y : Fin n} (p : G.Walk x y) (hp : ∀ v ∈ p.support, v ∉ S)
    {a b : Fin n} (ha : a ∈ S) (hb : b ∈ S) :
    (a < x ∧ x < b) ↔ (a < y ∧ y < b) := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

lemma OAI.PlanarL1.ColumnOrder.connected_noninterleaving line 183

Source documentation

Disjoint connected vertex sets cannot have representatives in alternating circular order. This upgrades the individual-chord barrier to branch sets.

lemma connected_noninterleaving {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {S T : Set (Fin n)}
    (hS : (G.induce S).Preconnected) (hT : (G.induce T).Preconnected)
    (hdis : Disjoint S T) {a b c d : Fin n}
    (ha : a ∈ S) (hb : b ∈ T) (hc : c ∈ S) (hd : d ∈ T)
    (hab : a < b) (hbc : b < c) (hcd : c < d) : False := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

structure OAI.PlanarL1.ColumnOrder.BranchModel line 202
Source documentation
A genuine finite branch-set model of a graph minor. Each branch is nonempty and connected; branches are disjoint and edges are witnessed by actual ambient edges. No topological or minor-exclusion axiom is hidden here.
```
structure BranchModel {n : ℕ} {W : Type*} (H : SimpleGraph W)
    (G : SimpleGraph (Fin n)) where
…
```
lemma OAI.PlanarL1.ColumnOrder.BranchModel.representative_injective line 214
lemma OAI.PlanarL1.ColumnOrder.BranchModel.union_connected line 220
lemma OAI.PlanarL1.ColumnOrder.BranchModel.noncrossing line 228
Source documentation
Noncrossing is inherited by every genuine branch-set minor, using any chosen representative of each branch. This proves the needed minor closure directly from walk separation, without a planar cone or a Jordan-curve axiom.
```
lemma noncrossing (B : BranchModel H G) (hnc : Noncrossing G)
    (r : W ↪ Fin n) (hr : ∀ i, r i ∈ B.branch i) : Noncrossing (H.map r) := by
…
```
Mentions: OAI.PlanarL1.ColumnOrder.BranchModel, OAI.PlanarL1.ColumnOrder.Noncrossing

lemma OAI.PlanarL1.ColumnOrder.common_neighbors_opposite line 249

Source documentation

For two fixed hubs in a noncrossing graph, two distinct common neighbors must lie on opposite open circular arcs of the hubs.

lemma common_neighbors_opposite {n : ℕ} {G : SimpleGraph (Fin n)}
    (hnc : Noncrossing G) {a b c d : Fin n} (hab : a < b) (hcd : c ≠ d)
    (hac : G.Adj a c) (had : G.Adj a d) (hbc : G.Adj b c) (hbd : G.Adj b d) :
    (a < c ∧ c < b) ↔ ¬ (a < d ∧ d < b) := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

lemma OAI.PlanarL1.ColumnOrder.no_three_common_neighbors line 275

lemma OAI.PlanarL1.ColumnOrder.BranchModel.no_three_common_neighbors line 292

Source documentation

Geometry geo:outerplanar: no noncrossing circular graph has a branch-set minor with two hubs and three distinct common neighbors.

lemma BranchModel.no_three_common_neighbors {n : ℕ} {W : Type*}
    {H : SimpleGraph W} {G : SimpleGraph (Fin n)} (B : BranchModel H G)
    (hnc : Noncrossing G) {a b c d e : W} (hab : a ≠ b)
    (hcd : c ≠ d) (hce : c ≠ e) (hde : d ≠ e)
    (hac : H.Adj a c) (had : H.Adj a d) (hae : H.Adj a e)
    (hbc : H.Adj b c) (hbd : H.Adj b d) (hbe : H.Adj b e) : False := by
…

Mentions: OAI.PlanarL1.ColumnOrder.BranchModel, OAI.PlanarL1.ColumnOrder.Noncrossing

lemma OAI.PlanarL1.ColumnOrder.connector_core line 312

Source documentation

Trimming a connector after its last visit to one set and before its first visit to the other. The nonadjacency assumption guarantees a nonempty core. The proof minimizes the number of edges, not the metric length.

lemma connector_core {V : Type*} {G : SimpleGraph V} {C L T : Set V}
    (hCL : Disjoint C L) (hno : ∀ x ∈ C, ∀ y ∈ L, ¬ G.Adj x y)
    {x y : V} (hx : x ∈ C) (hy : y ∈ L) (p : G.Walk x y)
    (hp : ∀ v ∈ p.support, v ∈ T) :
    ∃ K : Set V, K.Nonempty ∧ (G.induce K).Preconnected ∧ K ⊆ T ∧
      Disjoint K C ∧ Disjoint K L ∧
      (∃ a ∈ C, ∃ b ∈ K, G.Adj a b) ∧
      (∃ a ∈ L, ∃ b ∈ K, G.Adj a b) := by
…

lemma OAI.PlanarL1.ColumnOrder.no_three_cores line 379

Source documentation

Three disjoint connected connector cores between two disjoint connected sets would give the forbidden K₂,₃ minor.

lemma no_three_cores {n : ℕ} {G : SimpleGraph (Fin n)} (hnc : Noncrossing G)
    {C L : Set (Fin n)} (hC : C.Nonempty) (hL : L.Nonempty)
    (hc : (G.induce C).Preconnected) (hl : (G.induce L).Preconnected)
    (hCL : Disjoint C L) (K : Fin 3 → Set (Fin n))
    (hne : ∀ i, (K i).Nonempty) (hconn : ∀ i, (G.induce (K i)).Preconnected)
    (hdis : Pairwise (fun i j => Disjoint (K i) (K j)))
    (hdC : ∀ i, Disjoint (K i) C) (hdL : ∀ i, Disjoint (K i) L)
    (heC : ∀ i, ∃ a ∈ C, ∃ b ∈ K i, G.Adj a b)
    (heL : ∀ i, ∃ a ∈ L, ∃ b ∈ K i, G.Adj a b) : False := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

lemma OAI.PlanarL1.ColumnOrder.no_three_connectors line 440

Source documentation

The projected disjoint short portions used in the two-portals argument cannot exist. This includes the trimming and nonempty-interior justifications.

lemma no_three_connectors {n : ℕ} {G : SimpleGraph (Fin n)} (hnc : Noncrossing G)
    {C L : Set (Fin n)} (hc : (G.induce C).Preconnected)
    (hl : (G.induce L).Preconnected) (hCL : Disjoint C L)
    (hno : ∀ x ∈ C, ∀ y ∈ L, ¬ G.Adj x y)
    (x y : Fin 3 → Fin n) (hx : ∀ i, x i ∈ C) (hy : ∀ i, y i ∈ L)
    (p : ∀ i, G.Walk (x i) (y i))
    (hdis : Pairwise (fun i j => Disjoint
      {v | v ∈ (p i).support} {v | v ∈ (p j).support})) : False := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing

def OAI.PlanarL1.ColumnOrder.componentColumns line 456
Source documentation
The vertices of an induced-graph component, as a set in the original vertex type. Components here are Mathlib's actual reachability quotients.
```
def componentColumns {V : Type*} {G : SimpleGraph V} {S : Set V}
    (C : (G.induce S).ConnectedComponent) : Set V := Subtype.val '' C.supp
```
lemma OAI.PlanarL1.ColumnOrder.componentColumns_subset line 459
lemma OAI.PlanarL1.ColumnOrder.componentColumns_connected line 464
lemma OAI.PlanarL1.ColumnOrder.componentColumns_adj line 477

lemma OAI.PlanarL1.ColumnOrder.componentColumns_of_walk line 486

Source documentation

Any walk inside the induced vertex set propagates membership in an actual connected component.

lemma componentColumns_of_walk {V : Type*} {G : SimpleGraph V} {S : Set V}
    (C : (G.induce S).ConnectedComponent) {x y : V} (p : G.Walk x y)
    (hx : x ∈ componentColumns C) (hp : ∀ v ∈ p.support, v ∈ S) :
    y ∈ componentColumns C := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.ColumnOrder.exists_component_containing line 498

Source documentation

A nonempty induced-connected subset lies in one actual component of any larger induced subgraph.

lemma exists_component_containing {V : Type*} {G : SimpleGraph V} {S T : Set V}
    (hne : S.Nonempty) (hS : (G.induce S).Preconnected) (hST : S ⊆ T) :
    ∃ C : (G.induce T).ConnectedComponent, S ⊆ componentColumns C := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

lemma OAI.PlanarL1.ColumnOrder.component_eq_of_column line 515

Source documentation

Components of one induced graph sharing an original vertex are equal.

lemma component_eq_of_column {V : Type*} {G : SimpleGraph V} {S : Set V}
    {C D : (G.induce S).ConnectedComponent} {i : V}
    (hC : i ∈ componentColumns C) (hD : i ∈ componentColumns D) : C = D := by
…

Mentions: OAI.PlanarL1.ColumnOrder.componentColumns

def OAI.PlanarL1.ColumnOrder.componentAbove line 525

Source documentation

The parent component under inclusion of vertex sets.

def componentAbove {V : Type*} {G : SimpleGraph V} {S T : Set V}
    (hST : S ⊆ T) (C : (G.induce S).ConnectedComponent) :
    (G.induce T).ConnectedComponent :=
…

lemma OAI.PlanarL1.ColumnOrder.componentColumns_above line 530

lemma OAI.PlanarL1.ColumnOrder.connected_two_balls line 543

Source documentation

A discrete connected union of two metric balls has controlled diameter. The single edge allowance avoids assuming any continuous realization of the column graph. It will be absorbed by the source's 10D constant.

lemma connected_two_balls {V X : Type*} [PseudoMetricSpace X] {G : SimpleGraph V}
    (hG : G.Preconnected) (f : V → X) (p q : X) {R a : ℝ} (hR : 0 ≤ R)
    (ha : 0 ≤ a) (hedge : ∀ i j, G.Adj i j → dist (f i) (f j) ≤ a)
    (hcover : ∀ i, dist (f i) p ≤ R ∨ dist (f i) q ≤ R) (x y : V) :
    dist (f x) (f y) ≤ 4 * R + a := by
…

lemma OAI.PlanarL1.ColumnOrder.walk_comap_equiv line 599
Source documentation
Walks transport through a relabelling without introducing any new visited columns. This is used to cut the circular order at a chosen root.
```
lemma walk_comap_equiv {n : ℕ} {G : SimpleGraph (Fin n)} (e : Fin n ≃ Fin n)
    {i j : Fin n} (w : G.Walk (e i) (e j)) :
    ∃ p : (G.comap e).Walk i j, ∀ z ∈ p.support, e z ∈ w.support := by
…
```

lemma OAI.PlanarL1.ColumnOrder.collision line 615

Source documentation

Collision inequality for a profile whose strict sublevels connect back to zero. The ceiling is kept explicit: only thresholds at or below it are used.

lemma collision {n : ℕ} {G : SimpleGraph (Fin (n + 1))}
    (hnc : Noncrossing G) (f : Fin (n + 1) → ℝ) (D : ℝ)
    (hbound : ∀ i, f i ≤ D)
    (hpath : ∀ t ≤ D, ∀ i, f i < t →
      ∃ w : G.Walk i 0, ∀ z ∈ w.support, f z < t)
    {p q : Fin (n + 1)} (_hpq : p < q) (hadj : G.Adj p q) (heq : f p = f q)
    (hp : p ≠ 0) (z : Fin (n + 1)) (hpz : p ≤ z) (hzq : z ≤ q) : f p ≤ f z := by
…

Mentions: OAI.PlanarL1.ColumnOrder.Noncrossing