IncidenceCycle.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A cycle in the component--quartet incidence diagram

There is one edge per leaf. Parallel edges already give the two-edge cycle used in the manuscript; otherwise the incidence graph is simple, and at least as many edges as vertices force a cycle.

theorem OAI.Ostmann.forest_card_edges_lt line 16

Source documentation

A finite forest on a nonempty vertex set has fewer edges than vertices.

theorem forest_card_edges_lt {V : Type*} [Fintype V] [Nonempty V]
    (G : SimpleGraph V) [Fintype G.edgeSet] (hG : G.IsAcyclic) :
    G.edgeFinset.card < Fintype.card V := by
…

theorem OAI.Ostmann.exists_cycle_of_card_edges_ge line 27
def OAI.Ostmann.incidenceGraph line 37

theorem OAI.Ostmann.incidence_parallel_or_cycle line 47

Source documentation

The incidence diagram has either parallel leaves or a genuine simple cycle.

theorem incidence_parallel_or_cycle {L C Q : Type*} [Fintype L] [Fintype C] [Fintype Q]
    [Nonempty L] (component : L → C) (quartet : L → Q)
    (hcard : Fintype.card C + Fintype.card Q ≤ Fintype.card L) :
    (∃ i j : L, i ≠ j ∧ component i = component j ∧ quartet i = quartet j) ∨
      ∃ v : C ⊕ Q, ∃ c : (incidenceGraph component quartet).Walk v v, c.IsCycle := by
…

Mentions: OAI.Ostmann.incidenceGraph