GraphWedge.lean`

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.GraphWedge.retraction_pair_edist_le line 13
Source documentation
Each original edge belongs to exactly one block; a collapsed loop may have zero cost in either retraction. This local statement implies the full global, all-edge metric lower bound.
```
lemma retraction_pair_edist_le (r : V→A) (s : V→B)
    (h : ∀ {u v},H.Adj u v → G.edist (r u) (r v)+K.edist (s u) (s v) ≤ 1)
    (u v : V) : G.edist (r u) (r v)+K.edist (s u) (s v) ≤ H.edist u v := by
…
```
lemma OAI.FKCRT.GraphWedge.hom_edist_le line 33
structure OAI.FKCRT.GraphWedge.Data line 43
Source documentation
Combinatorial data of an actual one-vertex union. Distances are not part of these hypotheses; they are derived from the adjacency data below.
```
structure Data where
…
```
lemma OAI.FKCRT.GraphWedge.Data.cost_le line 62
theorem OAI.FKCRT.GraphWedge.Data.edist_left line 70
Source documentation
Attachments cannot shorten distances within any block.
```
theorem edist_left (D : Data G K H) (x y : A) : H.edist (D.left x) (D.left y)=G.edist x y := by
…
```
Mentions: OAI.FKCRT.GraphWedge.Data
theorem OAI.FKCRT.GraphWedge.Data.edist_right line 75
theorem OAI.FKCRT.GraphWedge.Data.edist_cross line 81
Source documentation
Distances between blocks add exactly through their shared pole.
```
theorem edist_cross (D : Data G K H) (x : A) (y : B) :
    H.edist (D.left x) (D.right y)=G.edist x D.poleLeft+K.edist D.poleRight y := by
…
```
Mentions: OAI.FKCRT.GraphWedge.Data
def OAI.FKCRT.PermutationWedge.sideSetoid line 104
abbrev OAI.FKCRT.PermutationWedge.Side line 108
def OAI.FKCRT.PermutationWedge.sideMk line 109
abbrev OAI.FKCRT.PermutationWedge.Vertex line 110
def OAI.FKCRT.PermutationWedge.vertex line 111
def OAI.FKCRT.PermutationWedge.dartGraph line 113
def OAI.FKCRT.PermutationWedge.sideGraph line 116
def OAI.FKCRT.PermutationWedge.inclusion line 123
Source comment
The maps below operate on the actual rotation-cycle quotients.
```
def inclusion : Side p S→Vertex (swap a b*p) := Quotient.lift
…
```
Mentions: OAI.FKCRT.PermutationWedge.Side, OAI.FKCRT.PermutationWedge.Vertex
lemma OAI.FKCRT.PermutationWedge.inclusion_mk line 127
lemma OAI.FKCRT.PermutationWedge.inclusion_injective line 129
def OAI.FKCRT.PermutationWedge.retractD line 139
lemma OAI.FKCRT.PermutationWedge.retractD_eq_of_join line 143
def OAI.FKCRT.PermutationWedge.retract line 156
lemma OAI.FKCRT.PermutationWedge.retract_vertex line 159
lemma OAI.FKCRT.PermutationWedge.retract_inclusion line 161
def OAI.FKCRT.PermutationWedge.flipInclusion line 165
lemma OAI.FKCRT.PermutationWedge.flipInclusion_injective line 169
def OAI.FKCRT.PermutationWedge.flipRetractD line 179
lemma OAI.FKCRT.PermutationWedge.flipRetractD_eq_of_join line 183
def OAI.FKCRT.PermutationWedge.flipRetract line 191
lemma OAI.FKCRT.PermutationWedge.flipRetract_vertex line 194
lemma OAI.FKCRT.PermutationWedge.flipRetract_flipInclusion line 196
lemma OAI.FKCRT.PermutationWedge.flipRetract_inclusion line 200
lemma OAI.FKCRT.PermutationWedge.retract_flipInclusion line 205
lemma OAI.FKCRT.PermutationWedge.inclusion_poles line 210
def OAI.FKCRT.PermutationWedge.inclusionHom line 215
def OAI.FKCRT.PermutationWedge.flipInclusionHom line 224
lemma OAI.FKCRT.PermutationWedge.retraction_edge line 233
def OAI.FKCRT.PermutationWedge.data line 265
Source documentation
Actual permutation-map insertion satisfies graph-wedge adjacency data. No metric or distance assertion is supplied as an assumption.
```
def data : GraphWedge.Data (sideGraph e p S he)
    (sideGraph e p Sᶜ (fun d => not_congr (he d))) (dartGraph e (swap a b*p)) where
…
```
Mentions: OAI.FKCRT.GraphWedge.Data, OAI.FKCRT.PermutationWedge.sideGraph, OAI.FKCRT.PermutationWedge.dartGraph
abbrev OAI.FKCRT.Chords.Opener line 290
def OAI.FKCRT.Chords.Cross line 292
def OAI.FKCRT.Chords.graph line 296
def OAI.FKCRT.Chords.Inside line 301
lemma OAI.FKCRT.Chords.opener_endpoints_ne line 304
lemma OAI.FKCRT.Chords.inside_propagates line 322
Source documentation
A chord which crosses a chord strictly inside a third chord must either be inside the third chord or cross it. Endpoint disjointness is explicit.
```
lemma inside_propagates (a : Perm (Fin N)) (ha : Function.Involutive a)
    (f x y : Opener a) (hyf : y≠f) (hc : Cross a x y)
    (hn : ¬Cross a f y) (hx : Inside a f x) : Inside a f y := by
…
```
Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.Chords.Cross, OAI.FKCRT.Chords.Inside
theorem OAI.FKCRT.Chords.component_gap line 339
Source documentation
A chord outside the root crossing component has no root-component endpoint in its interior. This is the algebraic corner-separation lemma: it requires neither a Jordan-curve assumption nor a stipulated block law.
```
theorem component_gap (a : Perm (Fin N)) (ha : Function.Involutive a)
    (r f : Opener a) (hroot : r.val≤f.val) (hf : ¬(graph a).Reachable r f)
    (x : Opener a) (hx : (graph a).Reachable r x) :
    ¬(f.val < x.val ∧ x.val < a f.val) ∧
      ¬(f.val < a x.val ∧ a x.val < a f.val) := by
…
```
Mentions: OAI.FKCRT.Chords.Opener, OAI.FKCRT.Chords.graph
def OAI.FKCRT.Chords.componentDarts line 371
Source documentation
Actual endpoint set of the root crossing component.
```
def componentDarts (a : Perm (Fin N)) (r : Opener a) : Finset (Fin N) :=
…
```
Mentions: OAI.FKCRT.Chords.Opener
lemma OAI.FKCRT.Chords.mem_componentDarts line 374
lemma OAI.FKCRT.Chords.external_not_component line 379
def OAI.FKCRT.Chords.gapIndex line 397
Source documentation
The gap index is determined solely by the ordered root-component darts. The two ends of every exterior matched pair have the same gap index.
```
def gapIndex (a : Perm (Fin N)) (r : Opener a) (d : Fin N) : ℕ :=
…
```
Mentions: OAI.FKCRT.Chords.Opener
theorem OAI.FKCRT.Chords.exterior_same_gap line 400