Spheres.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Release075.TriangleSphere line 10
Source documentation
A finite labelled spherical map, possibly with several connected components. All faces are triangles; there is no distinguished outer face.
```
structure TriangleSphere {E V : Type} (flip : E → E) (color : E → V)
    (face : E → E → E → Prop) where
…
```
structure OAI.Release075.TriangleSphere.Dipole line 32
theorem OAI.Release075.TriangleSphere.reverse_not_sameCycle line 41

theorem OAI.Release075.TriangleSphere.dipole_of_link_backtrack line 64

Source documentation

Internal reversal of a link walk creates a cancellable pair, when the face labels are determined by two consecutive sides.

theorem dipole_of_link_backtrack
    (hf : ∀ a b c, face a b c → color a ≠ color b ∧ color b ≠ color c ∧ color c ≠ color a)
    (hflip : ∀ e, flip (flip e) = e)
    (hmirror : ∀ a b c, face a b c → face (flip a) (flip c) (flip b))
    (hunique : ∀ a b c c', face a b c → face a b c' → c = c')
    (x : D.Dart)
    (hback : D.label x = D.label ((D.reverse*D.next) ((D.reverse*D.next) x))) :
    Nonempty D.Dipole := by
…

theorem OAI.Release075.TriangleSphere.noDipole_link_reduced line 107
abbrev OAI.Release075.TriangleSphere.vertexPerm line 119
def OAI.Release075.TriangleSphere.paint line 121
theorem OAI.Release075.TriangleSphere.paint_cl line 125
def OAI.Release075.TriangleSphere.vertexAngle line 128
theorem OAI.Release075.TriangleSphere.sum_angles line 131
theorem OAI.Release075.TriangleSphere.local_angle_lower line 167
theorem OAI.Release075.TriangleSphere.empty_of_angles line 204
Source documentation
Angular Gauss--Bonnet on a closed genus-zero map forbids a nonempty reduced sphere. This is a statement about actual finite permutation maps, not an asphericity or torsion-freeness assumption.
```
theorem empty_of_angles (q : V ≃ Fin 3)
    (hf : ∀ a b c, face a b c → color a ≠ color b ∧ color b ≠ color c ∧ color c ≠ color a)
    (hmin : ∀ v, 10 ≤ D.vertexAngle q v) : IsEmpty D.Dart := by
…
```

theorem OAI.Release075.MarkedLineData.sphere_empty_of_noDipole line 236

Source documentation

Every nonempty spherical map over the actual presentation has a dipole.

theorem sphere_empty_of_noDipole
    (D : TriangleSphere (d.presentation hr).flipEdge (d.presentation hr).edgeTarget
      (d.presentation hr).TriangleFace) (hD : IsEmpty D.Dipole) : IsEmpty D.Dart := by
…

Mentions: OAI.Release075.TriangleSphere

def OAI.Release075.TriangleSphere.cornerSum line 269
Source documentation
Evaluate once at every oriented corner. For cyclic face values this is three times the ordinary integral face chain; no unproved chain-complex property is used.
```
def cornerSum (D : TriangleSphere flip color face) (F : E → E → E → M) : M :=
…
```
Mentions: OAI.Release075.TriangleSphere

theorem OAI.Release075.TriangleSphere.Dipole.delete line 274

Source documentation

Remove an actual dipole, preserving every additive cyclic antisymmetric face evaluation.

theorem Dipole.delete {D : TriangleSphere flip color face} (P : D.Dipole)
    (F : E → E → E → M)
    (hrot : ∀ a b c, face a b c → F b c a = F a b c)
    (hmir : ∀ a b c, face a b c → F (flip a) (flip c) (flip b) = -F a b c) :
    ∃ D' : TriangleSphere flip color face,
      Fintype.card D'.Dart < Fintype.card D.Dart ∧ D'.cornerSum F = D.cornerSum F := by
…

Mentions: OAI.Release075.TriangleSphere

theorem OAI.Release075.TriangleSphere.cornerSum_eq_zero line 360

Source documentation

Diagrammatic reducibility annihilates integral spherical face chains.

theorem cornerSum_eq_zero
    (hempty : ∀ D : TriangleSphere flip color face, IsEmpty D.Dipole → IsEmpty D.Dart)
    (F : E → E → E → M)
    (hrot : ∀ a b c, face a b c → F b c a = F a b c)
    (hmir : ∀ a b c, face a b c → F (flip a) (flip c) (flip b) = -F a b c)
    (D : TriangleSphere flip color face) : D.cornerSum F = 0 := by
…

Mentions: OAI.Release075.TriangleSphere

def OAI.Release075.TriangleSphere.forgetLift line 383
def OAI.Release075.TriangleSphere.Dipole.lift line 398
Source documentation
Matching opposite face labels at a shared lifted edge forces matching group coordinates on the other two edges. Thus reduction cannot hide a downstairs dipole.
```
def Dipole.lift {D : TriangleSphere d.liftedFlip d.liftedTarget d.LiftedFace}
    (P : D.forgetLift.Dipole) : D.Dipole := by
…
```
Mentions: OAI.Release075.TriangleSphere
theorem OAI.Release075.TriangleSphere.noDipole_forgetLift line 432
theorem OAI.Release075.MarkedLineData.lifted_sphere_empty_of_noDipole line 440