CycleLists.lean`

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TorsionFreeZeroDivisors.CycleLists.orbit line 12
lemma OAI.TorsionFreeZeroDivisors.CycleLists.mem_orbit line 13
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_nonempty line 19
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_nodup line 21
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_head line 26
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_next line 31
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_rotate line 38
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_succ line 46
lemma OAI.TorsionFreeZeroDivisors.CycleLists.orbit_last line 51
def OAI.TorsionFreeZeroDivisors.CycleLists.words line 56
def OAI.TorsionFreeZeroDivisors.CycleLists.atIndex line 57
lemma OAI.TorsionFreeZeroDivisors.CycleLists.atIndex_cycle line 59
lemma OAI.TorsionFreeZeroDivisors.CycleLists.atIndex_bijective line 64
def OAI.TorsionFreeZeroDivisors.CycleLists.coordinates line 78
lemma OAI.TorsionFreeZeroDivisors.CycleLists.atIndex_rotate line 80
lemma OAI.TorsionFreeZeroDivisors.CycleLists.coordinates_rotate line 83
def OAI.TorsionFreeZeroDivisors.CycleLists.rootedRep line 87
Source documentation
Prescribe the representative of one root cycle without disturbing others.
```
def rootedRep (z : O) (c : Cycle f) : O := if c=cycle f z then z else Quotient.out c
…
```
lemma OAI.TorsionFreeZeroDivisors.CycleLists.rootedRep_cycle line 89
lemma OAI.TorsionFreeZeroDivisors.CycleLists.rootedRep_root line 95
def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.rootCycle line 103
def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.boundaryRep line 104
def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences line 105
def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths line 106
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_nonempty line 107
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_nodup line 108
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_nonempty line 109
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_length line 112
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_cycle line 113
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_root_head line 117
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.root_occurrence_position line 121
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_succ line 131
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_succ_ne_first line 133
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.occurrences_last line 140
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.ordinary_last_ne_first line 143
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_chain line 153
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_closed line 163
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_root_begins line 173
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_root_ends line 175
def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.pathCoordinates line 180
Source documentation
Every literal boundary position is exactly one surviving picture occurrence.
```
def pathCoordinates : (Σ c : Cycle a.closedRotation,Fin (a.paths hxy c).length)≃a.Occ :=
…
```
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.pathCoordinates_apply line 183
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.paths_dart line 185
lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.pathCoordinates_rotate line 189
def OAI.TorsionFreeZeroDivisors.ComparedBlocks.Comparisons.empty line 207
def OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.system line 232
def OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.coordinates line 274
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.dart line 276
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.rotation line 280
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.partner_compatible line 291
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.partner_reduced line 298
def OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.pairing line 305
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.rotation_conjugate line 312
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.pairing_euler line 321
Source documentation
Literal finite marked-certificate reduction supplies the Euler hypothesis of the actual boundary-pairing exclusion; nothing geometric is assumed here.
```
lemma pairing_euler : (pairing a hzw hr hz).Euler := by
…
```
Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.pairing
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.system_ordinary line 329
lemma OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.pairing_genusZero line 332
theorem OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.excluded line 341
Source documentation
Actual finite picture exclusion, conditional only on the still-missing sharp planar separator for its literal prepared interval graph. This is not an unconditional topology theorem or a proof of the manuscript's main result.
```
theorem excluded (hL : 2≤GirthAsymptotics.L (TypedGraphs.size rep))
    (hd : GraphSample.Diameters rep r) (hsample : r∈ActualPatternEvent.samples rep)
    (oneStep : ∀ S : Finset ((pairing a hzw hr hz).prepared hL hd).P,
      PlanarParameters.K PathSystem.ε ClosedWords.D<S.card →
      Nonempty (RecursiveSeparator.Split
        (PairingClusters.Rel (fun p : Position (fun t=>(((pairing a hzw hr hz).prepared hL hd).paths t).length)=>p.1)
          ((pairing a hzw hr hz).prepared hL hd).comparisons.pairing.partner) S))
    (havoid : IsEmpty (BoundedSystem (PlanarParameters.C PathSystem.ε ClosedWords.D)
      (PlanarParameters.K PathSystem.ε ClosedWords.D) (PlanarParameters.sides PathSystem.ε ClosedWords.D) rep r x y)) : False :=
…
```
Mentions: OAI.TorsionFreeZeroDivisors.GirthAsymptotics.L, OAI.TorsionFreeZeroDivisors.TypedGraphs.size, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.ActualPatternEvent.samples, OAI.TorsionFreeZeroDivisors.SampleGraph.Picture.pairing, OAI.TorsionFreeZeroDivisors.PlanarParameters.K, OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε, OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.D, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split, OAI.TorsionFreeZeroDivisors.PairingClusters.Rel, OAI.TorsionFreeZeroDivisors.SampleGraph.BoundedSystem, OAI.TorsionFreeZeroDivisors.PlanarParameters.C, OAI.TorsionFreeZeroDivisors.PlanarParameters.sides