OAI/NumberTheory/Ostmann/Tree/IncidenceCycleSigns.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.list_label_sum_eq_zero line 12
2. theorem OAI.Ostmann.list_label_sum_of_mem line 21
3. theorem OAI.Ostmann.incidenceDart_edge_of_label line 37
4. theorem OAI.Ostmann.incidenceWalk_labels_nodup line 45
5. theorem OAI.Ostmann.incidenceDartSign_eq_one_or_neg_one line 57
6. theorem OAI.Ostmann.incidenceWalkSign_values line 63
7. theorem OAI.Ostmann.incidenceCycleSign_nonzero line 76
8. theorem OAI.Ostmann.exists_balanced_incidence_sign line 88

   Source documentation

   The edge/vertex count produces an actual nontrivial, balanced reciprocal leaf action.

   theorem exists_balanced_incidence_sign {L C Q : Type*}
       [Fintype L] [Fintype C] [Fintype Q] [Nonempty L]
       [DecidableEq L] [DecidableEq C] [DecidableEq Q]
       (component : L → C) (quartet : L → Q)
       (hcard : Fintype.card C + Fintype.card Q ≤ Fintype.card L) :
       ∃ sign : L → ℤ,
         (∃ i, sign i = 1 ∨ sign i = -1) ∧
         (∀ i, sign i = 0 ∨ sign i = 1 ∨ sign i = -1) ∧
         (∀ c, (∑ i ∈ Finset.univ.filter (fun i => component i = c), sign i) = 0) ∧
         (∀ q, (∑ i ∈ Finset.univ.filter (fun i => quartet i = q), sign i) = 0) := by
   …