OAI/Algebra/GroupRing/ConePicture.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TorsionFreeZeroDivisors.SphericalPicture.Data line 15

   Source documentation

   A finite lifted spherical boundary map; empty boundary components are not recorded. Unlike the disk certificate there is NO marked exceptional boundary. This is combinatorial data, not yet a claim about a continuous sphere map.

   structure Data where
   …

2. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.Reduced line 27
3. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.reindex line 31
4. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.band line 42
5. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.tighten line 58
6. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.unequal_backtrack line 74
7. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.boundaryRep line 79
8. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.boundaryRep_cycle line 80
9. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.occurrences line 81
10. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.paths line 82
11. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.occurrences_nonempty line 83
12. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.paths_nonempty line 84
13. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.paths_length line 87
14. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.occurrences_succ line 88
15. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.occurrences_last line 90
16. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.paths_chain line 96
17. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.paths_closed line 105
18. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.pathCoordinates line 114
19. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.pathCoordinates_apply line 117
20. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.paths_dart line 119
21. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.pathCoordinates_rotate line 123
22. def OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.system line 141
23. def OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.coordinates line 169
24. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.dart line 171
25. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.rotation line 175
26. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.rotation_conjugate line 184
27. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.partner_compatible line 191
28. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.partner_reduced line 198
29. def OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.pairing line 215
30. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.pairing_genusZero line 221
31. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.pairing_euler line 227
32. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.system_ordinary line 231
33. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.separator line 235

    Source documentation

    Unconditional sharp split for the prepared all-cyclic spherical system.

    lemma separator (hL : 2≤GirthAsymptotics.L (TypedGraphs.size rep)) (hd : GraphSample.Diameters rep r)
        (S : Finset ((pairing (x:=x) (y:=y) a hr).prepared hL hd).P) :
    …

    Mentions: OAI.TorsionFreeZeroDivisors.GirthAsymptotics.L, OAI.TorsionFreeZeroDivisors.TypedGraphs.size, OAI.TorsionFreeZeroDivisors.GraphSample.Diameters, OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.pairing

34. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.excluded line 253

    Source documentation

    There is no NONEMPTY reduced spherical boundary certificate in the sample.

    theorem excluded [Nonempty O] (hL : 2≤GirthAsymptotics.L (TypedGraphs.size rep))
        (hd : GraphSample.Diameters rep r) (hsample : r∈ActualPatternEvent.samples rep)
        (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.BoundedSystem, OAI.TorsionFreeZeroDivisors.PlanarParameters.C, OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε, OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.D, OAI.TorsionFreeZeroDivisors.PlanarParameters.K, OAI.TorsionFreeZeroDivisors.PlanarParameters.sides

35. inductive OAI.TorsionFreeZeroDivisors.SphericalPicture.ReducesToEmpty line 267

    Source documentation

    Literal finite surgery trace, including the empty terminal picture. This records no geometric realization or implicit essentiality hypothesis.

    inductive ReducesToEmpty : {O : Type} → [Fintype O] → Data (O:=O) Γ label inv → Prop
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SphericalPicture.Data

36. def OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.deletionCoordinates line 280
37. lemma OAI.TorsionFreeZeroDivisors.SphericalPicture.Data.remaining_two_fewer line 286
38. theorem OAI.TorsionFreeZeroDivisors.SphericalPicture.reduces_of_no_reduced line 292

    Source documentation

    Strong induction on the actual number of boundary occurrences: each nonterminal step deletes two occurrences.

    theorem reduces_of_no_reduced (hinv : Function.Involutive inv)
        (hlabel : ∀d,label (Γ.reverse d)=inv (label d))
        (hex : ∀{O : Type}[Fintype O][Nonempty O](a : Data (O:=O) Γ label inv),¬a.Reduced)
    …

    Mentions: OAI.TorsionFreeZeroDivisors.SphericalPicture.Data

39. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.SpherePicture.reduces_to_empty line 320
40. abbrev OAI.TorsionFreeZeroDivisors.ConePicture.Radial line 337
41. abbrev OAI.TorsionFreeZeroDivisors.ConePicture.Dart line 338
42. def OAI.TorsionFreeZeroDivisors.ConePicture.reverse line 339
43. def OAI.TorsionFreeZeroDivisors.ConePicture.origin line 342
44. def OAI.TorsionFreeZeroDivisors.ConePicture.graph line 347

    Source documentation

    The one-skeleton in an abstract graph cone after its root radial edge is collapsed. Physical graph edges and all other radial edges are retained.

    def graph : PortGraph V (Dart Γ R) where
    …

    Mentions: OAI.TorsionFreeZeroDivisors.ConePicture.Dart

45. def OAI.TorsionFreeZeroDivisors.ConePicture.labels line 359
46. def OAI.TorsionFreeZeroDivisors.ConePicture.inverse line 362
47. lemma OAI.TorsionFreeZeroDivisors.ConePicture.inverse_inverse line 365
48. lemma OAI.TorsionFreeZeroDivisors.ConePicture.label_reverse line 369
49. lemma OAI.TorsionFreeZeroDivisors.ConePicture.reduced_old line 376
50. def OAI.TorsionFreeZeroDivisors.ConePicture.oldData line 392

    Source documentation

    Removing the ghost radial alphabet from a reduced picture changes NEITHER its permutation genus nor its boundary representatives.

    def oldData (hr : a.Reduced) : Data (O:=O) Γ label inv where
    …

51. lemma OAI.TorsionFreeZeroDivisors.ConePicture.oldData_reduced line 407
52. theorem OAI.TorsionFreeZeroDivisors.ConePicture.reduces_to_empty line 421

    Source documentation

    Actual triangular cone presentations introduce no extra reduced spherical pictures: every paired radial occurrence is the very same physical radial edge.

    theorem reduces_to_empty
        (hex : ∀{P : Type}[Fintype P][Nonempty P](b : Data (O:=P) Γ label inv),¬b.Reduced) :
    …