PlanarMap.lean`

26 declarations, 0 contain sorry, 0 declared as axioms

The parity argument in source sections/factors.tex. We count reversible flags, retaining parallel edges instead of identifying them in a simple graph.

def OAI.TorsionFreeZeroDivisors.PlanarMap.componentVertices line 15
lemma OAI.TorsionFreeZeroDivisors.PlanarMap.mem_componentVertices line 17
lemma OAI.TorsionFreeZeroDivisors.PlanarMap.componentVertices_disjoint line 19
def OAI.TorsionFreeZeroDivisors.PlanarMap.extendComponent line 27
Source documentation
Add the untouched small components to a separator of the unique large component. The original deletion set and hence its sharp cost are retained.
```
def extendComponent (c : G.ConnectedComponent)
    (P : Split G.Adj (componentVertices G c))
    (hsmall : ∀ d : G.ConnectedComponent,d≠c→3*(componentVertices G d).card≤2*Fintype.card V) :
    Split G.Adj Finset.univ := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.componentVertices
theorem OAI.TorsionFreeZeroDivisors.PlanarMap.Model.univ_split line 102
Source documentation
Sharp separator for any finite genus-zero rotation map, including empty and disconnected graphs.
```
theorem Model.univ_split (M : Model G) : Nonempty (Split G.Adj Finset.univ) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.Model
theorem OAI.TorsionFreeZeroDivisors.PlanarMap.Model.split line 140
Source documentation
The exact sharp separator on every induced vertex set.
```
theorem Model.split (M : Model G) (S : Finset V) : Nonempty (Split G.Adj S) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.PlanarMap.Model
def OAI.TorsionFreeZeroDivisors.BoundaryRotation.cyclesEquiv line 159
Source documentation
Actual boundary cycles are exactly the nonempty boundary words.
```
def cyclesEquiv : Cycle (perm len) ≃ T :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.BoundaryRotation.perm
lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.cyclesEquiv_cycle line 167
def OAI.TorsionFreeZeroDivisors.BoundaryRotation.interaction line 170
def OAI.TorsionFreeZeroDivisors.BoundaryRotation.graphIso line 177
def OAI.TorsionFreeZeroDivisors.BoundaryRotation.model line 193
theorem OAI.TorsionFreeZeroDivisors.BoundaryRotation.split line 205
Source documentation
The sharp separator for the literal interaction relation, retaining loops as required by the existing recursive charging theorem.
```
theorem split (α : Equiv.Perm (Position len)) (ha : Function.Involutive α)
    (hz : MapEuler.GenusZero (perm len) α) (S : Finset T) :
    Nonempty (RecursiveSeparator.Split (PairingClusters.Rel (fun x=>x.1) α) S) := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.BoundaryRotation.perm, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split, OAI.TorsionFreeZeroDivisors.PairingClusters.Rel
theorem OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.separator_obligation line 221
Source documentation
Discharge the former sharp planar-separator obligation of every reduced disk picture, using its actual genus-zero segmented interaction map.
```
theorem separator_obligation : SeparatorObligation r x y hL hd := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.SeparatorObligation
lemma OAI.TorsionFreeZeroDivisors.Factors.odd_nsmul line 239

theorem OAI.TorsionFreeZeroDivisors.Factors.odd_fibre_cancellation line 247

Source documentation

Odd fibres allow an invariant sum over vertices to be computed over flags. The fixed-point-free involution of flags then cancels it in characteristic two.

theorem odd_fibre_cancellation {P F R : Type*} [Fintype P] [Fintype F]
    [AddCommMonoid R] (h2 : ∀ x : R,x+x=0) (proj : F → P) (rev : F → F)
    (hr : Function.Involutive rev) (hne : ∀ e,rev e≠e)
    (hodd : ∀ p,Odd (Finset.univ.filter (fun e => proj e=p)).card)
    (f : P → R) (hf : ∀ e,f (proj (rev e))=f (proj e)) :
    ∑ p,f p=0 := by
…

abbrev OAI.TorsionFreeZeroDivisors.Factors.DartA line 267
abbrev OAI.TorsionFreeZeroDivisors.Factors.DartB line 268
abbrev OAI.TorsionFreeZeroDivisors.Factors.Flag line 269
def OAI.TorsionFreeZeroDivisors.Factors.base line 270
def OAI.TorsionFreeZeroDivisors.Factors.fibreEquiv line 273
Source documentation
The entire common outgoing set, not a quotient of its parallel steps.
```
def fibreEquiv (p : A×B) : {e : Flag outA outB // base outA outB e=p} ≃
    {t : T // t∈outA p.1∩outB p.2} where
…
```
Mentions: OAI.TorsionFreeZeroDivisors.Factors.Flag, OAI.TorsionFreeZeroDivisors.Factors.base
lemma OAI.TorsionFreeZeroDivisors.Factors.fibre_card line 296
def OAI.TorsionFreeZeroDivisors.Factors.reverse line 304
lemma OAI.TorsionFreeZeroDivisors.Factors.reverse_involutive line 307
lemma OAI.TorsionFreeZeroDivisors.Factors.reverse_ne line 313

theorem OAI.TorsionFreeZeroDivisors.Factors.product_zero line 322

Source documentation

The source factors on full components; compatibility is the literal path-order rule along every outgoing edge.

theorem product_zero
    (hrA : Function.Involutive rA) (hrB : Function.Involutive rB)
    (hbar : ∀ t,bar t≠t) (hodd : ∀ a b,Odd (outA a∩outB b).card)
    (letter : T→G) (g : A→G) (h : B→G)
    (hg : ∀ d : DartA outA,g (rA d).val.1=g d.val.1*letter d.val.2)
    (hh : ∀ d : DartB outB,h (rB d).val.1=h d.val.1*letter d.val.2) :
    (∑ a,MonoidAlgebra.single (g a) (1 : ZMod 2)) *
      (∑ b,MonoidAlgebra.single ((h b)⁻¹) (1 : ZMod 2))=0 := by
…

Mentions: OAI.TorsionFreeZeroDivisors.Factors.DartA, OAI.TorsionFreeZeroDivisors.Factors.DartB

theorem OAI.TorsionFreeZeroDivisors.Factors.sum_nonzero line 355

Source documentation

Only the root must have a unique label; no non-root injectivity is needed.

theorem sum_nonzero (root : A) (g : A→G) (hroot : g root=1)
    (hunique : ∀ a,g a=1 → a=root) :
    (∑ a,MonoidAlgebra.single (g a) (1 : ZMod 2))≠0 := by
…