PortSubdivision.lean`

55 declarations, 0 contain sorry, 0 declared as axioms

Quantitative edge switching for the girth conditioning in types.tex 116–147. The simple-graph lemmas are also applicable to the canonical threefold subdivision of a port multigraph (loops become triangles). No random-graph existence or cone-topology conclusion is assumed in these lemmas.

structure OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph line 9
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.reverse_reverse_apply line 18
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.subdivision line 22
Source documentation
The canonical threefold subdivision, including loops and parallel edges.
```
def subdivision : SimpleGraph (V ⊕ D) where
…
```
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.adj_original line 45
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.adj_original_port line 46
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.adj_port_original line 48
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.adj_ports line 50
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.port_adj_iff line 53
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.cycle_middle_at_port line 59
Source documentation
Every cycle through a port uses its middle edge, since the other port neighbor is unique and the cycle cannot immediately backtrack.
```
theorem cycle_middle_at_port (d : D) (p : Γ.subdivision.Walk (.inr d) (.inr d))
    (hp : p.IsCycle) : s(Sum.inr d,Sum.inr (Γ.reverse d)) ∈ p.edges := by
…
```
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.cycle_has_middle line 73
Source documentation
No cycle lives entirely in the spokes; a short cycle always gives a middle edge eligible for a matching transposition.
```
theorem cycle_has_middle [DecidableEq V] [DecidableEq D] {a : V ⊕ D}
    (p : Γ.subdivision.Walk a a) (hp : p.IsCycle) :
    ∃ d, s(Sum.inr d,Sum.inr (Γ.reverse d)) ∈ p.edges := by
…
```
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.originalNeighborEquiv line 90
Source documentation
The neighbor fiber at an original vertex is exactly its port fiber.
```
def originalNeighborEquiv (v : V) :
    Γ.subdivision.neighborSet (.inl v) ≃ {d : D // Γ.origin d = v} where
…
```
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.portNeighborEquiv line 101
Source documentation
A port has exactly two neighbors: its original vertex and its reverse port. They lie in disjoint summands even when the original edge is a graph loop.
```
def portNeighborEquiv (d : D) : Γ.subdivision.neighborSet (.inr d) ≃ Bool where
…
```
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.card_original_neighbors line 112
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.card_port_neighbors line 116
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.moveMatches line 122
Source documentation
Conjugating the reversal while keeping port origins fixed is a matching switch, not a relabeling of the original graph.
```
def moveMatches (σ : Equiv.Perm D) : PortGraph V D where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch line 136
Source documentation
Transpose two equally oriented ports. Their reverse ports are not moved.
```
def switch (d e : D) : PortGraph V D := Γ.moveMatches (Equiv.swap d e)
```
Mentions: OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch_origin line 138
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch_reverse_left line 140
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch_reverse_right line 144
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch_reverse_unchanged line 148

theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch_adj line 156

Source documentation

The subdivision changes exactly the two middle edges, preserving every origin-port incidence, including incidences belonging to original loops.

theorem switch_adj (d e : D) (hde : d ≠ e) (hdr : d ≠ Γ.reverse e)
    (a b : V ⊕ D) :
    (Γ.switch d e).subdivision.Adj a b ↔
      (Γ.subdivision.Adj a b ∧ s(a,b) ≠ s(Sum.inr d,Sum.inr (Γ.reverse d)) ∧
        s(a,b) ≠ s(Sum.inr e,Sum.inr (Γ.reverse e))) ∨
      s(a,b) = s(Sum.inr d,Sum.inr (Γ.reverse e)) ∨
      s(a,b) = s(Sum.inr e,Sum.inr (Γ.reverse d)) := by
…

theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.label_swap line 209
Source documentation
Transposing two occurrences of the same label preserves every port label.
```
theorem label_swap {T : Type*} (label : D → T) (d e : D) (h : label d = label e)
    (f : D) : label ((Equiv.swap d e) f) = label f := by
…
```
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.switch_preserves_labels line 217

inductive OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk line 227

Source documentation

Multigraph walks remember the traversed port, not just endpoint vertices.

inductive Walk : V → V → Type _
  | nil (v : V) : Walk v v
  | cons {v w : V} (d : D) (hd : Γ.origin d = v)
      (p : Walk (Γ.origin (Γ.reverse d)) w) : Walk v w

namespace Walk
variable {Γ} {a b c : V}

def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.length line 235
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.darts line 239
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.append line 243
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.length_darts line 247
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.length_append line 250
def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.IsReduced line 257
Source documentation
Source immersion is exactly nonbacktracking of consecutive ports.
```
def IsReduced (p : Γ.Walk a b) : Prop :=
…
```

def OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.toSubdivision line 261

Source documentation

No changes to endpoints or to the original multigraph are made by subdividing.

def toSubdivision {a b : V} : Γ.Walk a b → Γ.subdivision.Walk (.inl a) (.inl b)
  | .nil a => .nil
  | .cons d hd p =>
    .cons (show Γ.subdivision.Adj (.inl a) (.inr d) from hd)
      (.cons (show Γ.subdivision.Adj (.inr d) (.inr (Γ.reverse d)) from rfl)
        (.cons (show Γ.subdivision.Adj (.inr (Γ.reverse d)) (.inl (Γ.origin (Γ.reverse d))) from rfl) p.toSubdivision))

theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.length_toSubdivision line 268
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.toSubdivision_append line 274
theorem OAI.TorsionFreeZeroDivisors.PortSubdivision.PortGraph.Walk.reduced_toSubdivision line 282
Source documentation
Immersion of the original port path is preserved by the subdivision. In particular the encoding does not spuriously remove a short circuit.
```
theorem reduced_toSubdivision (p : Γ.Walk a b) (hp : p.IsReduced) :
    p.toSubdivision.edges.IsChain (· ≠ ·) := by
…
```

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.split_at_edge line 322

Source documentation

Decompose at a specified edge occurrence, with its actual orientation.

theorem split_at_edge (p : G.Walk a b) (e : Sym2 V) (he : e ∈ p.edges) :
    ∃ (x y : V) (hxy : G.Adj x y) (p₁ : G.Walk a x) (p₂ : G.Walk y b),
      s(x,y) = e ∧ p = p₁.append (.cons hxy p₂) := by
…

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.alternate_walk line 336

Source documentation

Removing an edge of a closed trail leaves an alternate walk one shorter, without using the removed edge.

theorem alternate_walk (p : G.Walk a a) (hp : p.IsTrail)
    (e : Sym2 V) (he : e ∈ p.edges) :
    ∃ (x y : V) (q : G.Walk x y),
      s(x,y) = e ∧ e ∉ q.edges ∧ q.length + 1 = p.length := by
…

def OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge line 357
Source documentation
Adjoining one new edge.
```
def addEdge (G : SimpleGraph V) (x y : V) : SimpleGraph V :=
…
```
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge_adj line 360
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.transfer_addEdge line 365
Source documentation
A walk avoiding the newly adjoined edge lies in the old graph.
```
theorem transfer_addEdge (p : (addEdge G x y).Walk a b)
    (hp : s(x,y) ∉ p.edges) :
    ∃ q : G.Walk a b, q.length = p.length := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.girth_addEdge line 379
Source documentation
Adding an edge whose endpoints have no short old connecting path preserves the lower girth bound. The path hypothesis includes either orientation.
```
theorem girth_addEdge (L : ℕ) (hG : (L : ℕ∞) ≤ G.egirth)
    (hx : ∀ p : G.Walk x y, L ≤ p.length + 1) :
    (L : ℕ∞) ≤ (addEdge G x y).egirth := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.first_new_edge line 409
Source documentation
Before the first occurrence of a new edge, a walk lies wholly in G. No simplicity assumption is required for this decomposition.
```
theorem first_new_edge (p : (addEdge G x y).Walk a b) :
    (∃ q : G.Walk a b, q.length ≤ p.length) ∨
    (∃ q : G.Walk a x, q.length + 1 ≤ p.length) ∨
    (∃ q : G.Walk a y, q.length + 1 ≤ p.length) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.length_lower_addEdge line 429
Source documentation
A lower path-length bound is stable under a new edge if both of its endpoints are sufficiently far from the starting vertex.
```
theorem length_lower_addEdge (N : ℕ)
    (hab : ∀ q : G.Walk a b, N ≤ q.length)
    (hax : ∀ q : G.Walk a x, N ≤ q.length + 1)
    (hay : ∀ q : G.Walk a y, N ≤ q.length + 1)
    (p : (addEdge G x y).Walk a b) : N ≤ p.length := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.girth_alternate_lower line 442
Source documentation
In a graph of girth at least L, an alternate path across an old edge has length at least L-1. This is precisely the nonbad-edge input to the matching transposition argument.
```
theorem girth_alternate_lower (L : ℕ) (hG : (L : ℕ∞) ≤ G.egirth)
    (hxy : G.Adj x y) (p : (G.deleteEdges {s(x,y)}).Walk x y) :
    L ≤ p.length + 1 := by
…
```
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.girth_switch line 464
Source documentation
Two-switching in a simple graph: delete xy and uz, then add xz and uy. The distance condition is the manuscript's separation of the two endpoint sets. All previous prescribed edges survive provided neither deleted edge was among those prescriptions.
```
theorem girth_switch (L : ℕ) {x y u z : V}
    (hG : (L : ℕ∞) ≤ G.egirth) (huz : G.Adj u z)
    (hfar : ∀ a ∈ ({x,y} : Set V), ∀ b ∈ ({u,z} : Set V),
      ∀ p : G.Walk a b, 2 * L < p.length) :
    (L : ℕ∞) ≤
      (addEdge (addEdge (G.deleteEdges {s(x,y),s(u,z)}) x z) u y).egirth := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.short_cycle_descends_add line 498
Source documentation
Short cycles in an edge-adjoined graph descend to the old graph whenever there is no short alternate path. This needs no girth assumption on the old graph, and so also applies during the initial bad-edge repair algorithm.
```
theorem short_cycle_descends_add (L : ℕ)
    (hx : ∀ p : G.Walk x y, L ≤ p.length + 1)
    (p : (addEdge G x y).Walk a a) (hp : p.IsCycle) (hlen : p.length < L) :
    ∃ q : G.Walk a a, q.IsCycle ∧ q.edges = p.edges ∧ q.length = p.length := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.nonbad_alternate_lower line 525

Source documentation

Local nonbadness of one edge suffices for the alternate-path estimate.

theorem nonbad_alternate_lower (L : ℕ) (hxy : G.Adj x y)
    (hnonbad : ∀ a (c : G.Walk a a), c.IsCycle → c.length < L → s(x,y) ∉ c.edges)
    (p : (G.deleteEdges {s(x,y)}).Walk x y) : L ≤ p.length + 1 := by
…

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.short_cycle_descends_switch line 552

Source documentation

The repair two-switch creates no short cycle, even before girth has been repaired everywhere. Deleting a bad edge therefore strictly reduces the bad edge set; this local assertion is the core of the repair argument.

theorem short_cycle_descends_switch (L : ℕ) {x y u z : V}
    (huz : G.Adj u z)
    (hnonbad : ∀ a (c : G.Walk a a), c.IsCycle → c.length < L → s(u,z) ∉ c.edges)
    (hfar : ∀ a ∈ ({x,y} : Set V), ∀ b ∈ ({u,z} : Set V),
      ∀ p : G.Walk a b, 2 * L < p.length)
    (p : (addEdge (addEdge (G.deleteEdges {s(x,y),s(u,z)}) x z) u y).Walk a a)
    (hp : p.IsCycle) (hlen : p.length < L) :
    ∃ q : (G.deleteEdges {s(x,y),s(u,z)}).Walk a a,
      q.IsCycle ∧ q.edges = p.edges ∧ q.length = p.length := by
…

Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.shortest_cycle_descends_switch line 588

Source documentation

At the shortest-cycle threshold, no nonbadness requirement is needed on the auxiliary edge: a new cycle using both new edges is strictly longer than the old girth. This permits deterministic girth repair.

theorem shortest_cycle_descends_switch (L : ℕ) {x y u z : V}
    (hG : (L : ℕ∞) ≤ G.egirth) (huz : G.Adj u z)
    (hfar : ∀ a ∈ ({x,y} : Set V), ∀ b ∈ ({u,z} : Set V),
      ∀ p : G.Walk a b, 2 * (L+1) < p.length)
    (p : (addEdge (addEdge (G.deleteEdges {s(x,y),s(u,z)}) x z) u y).Walk a a)
    (hp : p.IsCycle) (hlen : p.length < L+1) :
    ∃ q : (G.deleteEdges {s(x,y),s(u,z)}).Walk a a,
      q.IsCycle ∧ q.edges = p.edges ∧ q.length = p.length := by
…

Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge

def OAI.TorsionFreeZeroDivisors.GirthSwitch.badEdges line 621
Source documentation
The exact set minimized by the finite repair argument.
```
def badEdges (G : SimpleGraph V) (L : ℕ) : Set (Sym2 V) :=
…
```
theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.badEdges_subset line 624

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.badEdges_strict line 630

Source documentation

Edgewise transfer of short cycles strictly reduces the bad edge set as soon as a specified old bad edge has been deleted.

theorem badEdges_strict {L : ℕ} [Fintype V] (e : Sym2 V) (he : e ∈ badEdges G L)
    (hdesc : ∀ a (p : H.Walk a a), p.IsCycle → p.length < L →
      ∃ q : G.Walk a a, q.IsCycle ∧ q.edges = p.edges ∧ q.length = p.length)
    (hdel : e ∉ badEdges H L) :
    (badEdges H L).toFinite.toFinset.card < (badEdges G L).toFinite.toFinset.card := by
…

Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.badEdges

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.girth_improve_one line 654

Source documentation

Finite extremal repair raises the girth by one. Unlike the manuscript's probabilistic initialization, this argument only needs the uniform far-edge supply; all objects and the final girth condition are unchanged.

theorem girth_improve_one [Fintype V] (L : ℕ) (P : SimpleGraph V → Prop)
    (hne : ∃ G, P G ∧ (L : ℕ∞) ≤ G.egirth)
    (hswitch : ∀ G, P G → ∀ a (p : G.Walk a a), p.IsCycle →
      ∃ x y u z, s(x,y) ∈ p.edges ∧ G.Adj u z ∧
        (∀ a ∈ ({x,y} : Set V), ∀ b ∈ ({u,z} : Set V),
          ∀ p : G.Walk a b, 2 * (L+1) < p.length) ∧
        P (addEdge (addEdge (G.deleteEdges {s(x,y),s(u,z)}) x z) u y)) :
    ∃ G, P G ∧ ((L+1 : ℕ) : ℕ∞) ≤ G.egirth := by
…

Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.exists_large_girth line 697

Source documentation

Arbitrarily specified finite girth follows by finitely many exact transpositions if the family has a uniform distant auxiliary edge supply.

theorem exists_large_girth [Fintype V] (N : ℕ) (P : SimpleGraph V → Prop)
    (hne : ∃ G, P G)
    (hswitch : ∀ G, P G → ∀ a (p : G.Walk a a), p.IsCycle →
      ∃ x y u z, s(x,y) ∈ p.edges ∧ G.Adj u z ∧
        (∀ a ∈ ({x,y} : Set V), ∀ b ∈ ({u,z} : Set V),
          ∀ p : G.Walk a b, 2 * N < p.length) ∧
        P (addEdge (addEdge (G.deleteEdges {s(x,y),s(u,z)}) x z) u y)) :
    ∃ G, P G ∧ (N : ℕ∞) ≤ G.egirth := by
…

Mentions: OAI.TorsionFreeZeroDivisors.GirthSwitch.addEdge

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.short_reduced_isPath line 725
Source documentation
Below the girth, a nonbacktracking walk cannot repeat a vertex. This is the quantitative version of Mathlib's forest lemma.
```
theorem short_reduced_isPath (L : ℕ) (hG : L ≤ G.egirth)
    (p : G.Walk a b) (hlen : p.length < L)
    (h : p.edges.IsChain (· ≠ ·)) : p.IsPath := by
…
```

theorem OAI.TorsionFreeZeroDivisors.GirthSwitch.reduced_closed_length line 759

Source documentation

Every nonempty immersed circuit has at least the graph's girth.

theorem reduced_closed_length (L : ℕ) (hG : L ≤ G.egirth)
    (p : G.Walk a a) (hne : 0 < p.length)
    (h : p.edges.IsChain (· ≠ ·)) : L ≤ p.length := by
…