OAI/GroupTheory/Hyperbolic/Ribbons.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Release075.AngleDiskCounts line 11

   Source documentation

   The numerical incidence identities of a nonempty planar triangle disk, with boundary visits counted with multiplicity (including both sides of naked edges). All fields are finite counts or angle data. No group conclusion is assumed.

   structure AngleDiskCounts where
   …

2. def OAI.Release075.AngleDiskCounts.curvature line 27
3. theorem OAI.Release075.AngleDiskCounts.gauss_bonnet line 30

   Source documentation

   Gauss--Bonnet includes repeated boundary visits and naked edges.

   theorem gauss_bonnet : ∑ v, D.curvature v = 10 := by
   …

4. theorem OAI.Release075.AngleDiskCounts.cannot_have_geodesic_boundary line 40

   Source documentation

   Curvature obstruction for a boundary all of whose cyclic turns have link length >=π: an interior reduced link contributes >=2π and a single exterior visit contributes >=π. Multiple visits require no turn estimate.

   theorem cannot_have_geodesic_boundary
       (hinterior : ∀ v, D.visits v = 0 → 10 ≤ D.angles v)
       (hboundary : ∀ v, D.visits v = 1 → 5 ≤ D.angles v) : False := by
   …

5. def OAI.Release075.AngleDiskCounts.interior line 60
6. def OAI.Release075.AngleDiskCounts.boundary line 64
7. def OAI.Release075.AngleDiskCounts.boundaryLength line 68
8. theorem OAI.Release075.AngleDiskCounts.vertices_partition line 70
9. theorem OAI.Release075.AngleDiskCounts.boundary_card_le_length line 75
10. theorem OAI.Release075.AngleDiskCounts.face_vertex_formula line 87

    Source documentation

    The Euler/incidence formula in terms of interior and boundary vertices.

    theorem face_vertex_formula :
        D.faces + D.boundaryLength + 2 = 2*D.interior.card + 2*D.boundary.card := by
    …

11. theorem OAI.Release075.AngleDiskCounts.linear_face_bound line 95
12. theorem OAI.Release075.AngleDiskCounts.polygon_original_vertex_bound line 117

    Source documentation

    For a simple geodesic polygon only its designated corners can contribute positive boundary curvature. Original interior vertices cost two angle units. This is the exact quantitative count used for uniform inradius.

    theorem polygon_original_vertex_bound (original corners : Finset D.Vertex)
        (hvisits : ∀ v, D.visits v ≤ 1)
        (hcorner : ∀ v ∈ corners, D.visits v = 1)
        (horiginal : ∀ v ∈ original, D.visits v = 0)
        (hstrict : ∀ v ∈ original, 12 ≤ D.angles v)
        (hinterior : ∀ v, D.visits v = 0 → 10 ≤ D.angles v)
        (hboundary : ∀ v, D.visits v = 1 → v ∉ corners → 5 ≤ D.angles v) :
        2*(original.card : ℝ) + 10 ≤ 5*corners.card := by
    …

13. structure OAI.Release075.TriangleRibbon line 172

    Source documentation

    An oriented combinatorial triangle filling. Darts are incoming at the corner they carry; reverse * face rotates those corners about a vertex. This records finite incidence data, NOT existence of a filling for a nullword. Its single distinguished face is the prescribed exterior walk, including spurs.

    structure TriangleRibbon where
    …

14. abbrev OAI.Release075.TriangleRibbon.vertexPerm line 189
15. abbrev OAI.Release075.TriangleRibbon.Vertex line 190
16. abbrev OAI.Release075.TriangleRibbon.Edge line 191
17. abbrev OAI.Release075.TriangleRibbon.Face line 192
18. def OAI.Release075.TriangleRibbon.weight line 194
19. def OAI.Release075.TriangleRibbon.cornerAngle line 196
20. def OAI.Release075.TriangleRibbon.visits line 199
21. def OAI.Release075.TriangleRibbon.angles line 202
22. theorem OAI.Release075.TriangleRibbon.cornerAngle_nonneg line 205
23. theorem OAI.Release075.TriangleRibbon.angles_nonneg line 209
24. theorem OAI.Release075.TriangleRibbon.card_face_fiber line 216
25. theorem OAI.Release075.TriangleRibbon.face_angle_sum line 221
26. theorem OAI.Release075.TriangleRibbon.dart_card line 233
27. theorem OAI.Release075.TriangleRibbon.visits_sum line 236
28. theorem OAI.Release075.TriangleRibbon.exterior_count line 248
29. theorem OAI.Release075.TriangleRibbon.all_angles_sum line 257
30. def OAI.Release075.TriangleRibbon.counts line 277

    Source documentation

    All arithmetic hypotheses of the earlier curvature identity are now derived from actual edge/face/vertex permutations and face-color bijections.

    noncomputable def counts : AngleDiskCounts where
    …

    Mentions: OAI.Release075.AngleDiskCounts

31. def OAI.Release075.SumWalk.left line 295

    Source documentation

    Forget the disjoint summand tag from a walk in the left component.

    def left {a b : U} : (G.sum H).Walk (.inl a) (.inl b) → G.Walk a b
      | .nil => .nil
      | .cons (v := .inl _) h p => (left p).cons (SimpleGraph.sum_adj_inl.mp h)
    …

32. theorem OAI.Release075.SumWalk.left_length line 300
33. theorem OAI.Release075.SumWalk.map_left line 304
34. theorem OAI.Release075.SumWalk.left_reduced line 308
35. def OAI.Release075.SumWalk.right line 320

    Source documentation

    The right-component extraction is left extraction after the graph sum swap.

    def right {a b : V} (p : (G.sum H).Walk (.inr a) (.inr b)) : H.Walk a b :=
    …

36. theorem OAI.Release075.SumWalk.right_length line 323
37. theorem OAI.Release075.SumWalk.right_reduced line 327
38. theorem OAI.Release075.IsBoundary.sameCycle line 339
39. theorem OAI.Release075.IsBoundary.mem_iff_sameCycle line 361
40. theorem OAI.Release075.PermCycles.three_color_bijective line 373
41. abbrev OAI.Release075.TriangleFilling.ActiveDart line 405
42. def OAI.Release075.TriangleFilling.activeReverse line 406
43. def OAI.Release075.TriangleFilling.activeNext line 407
44. theorem OAI.Release075.TriangleFilling.activeReverse_val line 409
45. theorem OAI.Release075.TriangleFilling.activeNext_val line 410
46. theorem OAI.Release075.TriangleFilling.activeReverse_involutive line 412
47. theorem OAI.Release075.TriangleFilling.activeReverse_ne line 417
48. theorem OAI.Release075.TriangleFilling.active_planar line 421
49. theorem OAI.Release075.TriangleFilling.active_components line 424
50. theorem OAI.Release075.TriangleFilling.active_componentCount line 435
51. theorem OAI.Release075.TriangleFilling.active_color_step line 446
52. def OAI.Release075.TriangleFilling.activeColor line 450
53. theorem OAI.Release075.TriangleFilling.active_boundary_iff line 453
54. def OAI.Release075.TriangleFilling.ribbon line 460

    Source documentation

    A nonempty labeled filling has its connected boundary component as an actual Euler-characteristic-one triangle ribbon. No geometric embedding is postulated.

    noncomputable def ribbon (q : V ≃ Fin 3)
        (hf : ∀ a b c, face a b c → color a ≠ color b ∧ color b ≠ color c ∧ color c ≠ color a)
        (b : D.Dart) (hb : b ∈ D.boundary) : TriangleRibbon where
    …

    Mentions: OAI.Release075.TriangleRibbon

55. def OAI.Release075.SequenceWalk.walk line 497
56. theorem OAI.Release075.SequenceWalk.length_walk line 501
57. theorem OAI.Release075.SequenceWalk.getVert_walk line 506
58. theorem OAI.Release075.SequenceWalk.reduced_walk line 517
59. theorem OAI.Release075.PermCycles.class_filter line 531
60. theorem OAI.Release075.PermCycles.pow_card_orbit line 536
61. theorem OAI.Release075.PermCycles.pow_ne_of_lt_card_orbit line 540
62. def OAI.Release075.TriangleRibbon.IsOuter line 557
63. def OAI.Release075.TriangleRibbon.outerCorners line 559
64. def OAI.Release075.TriangleRibbon.innerCorners line 561
65. theorem OAI.Release075.TriangleRibbon.visits_cl line 564
66. theorem OAI.Release075.TriangleRibbon.angles_cl line 571
67. theorem OAI.Release075.TriangleRibbon.corner_count line 584
68. theorem OAI.Release075.TriangleRibbon.no_outer_of_visits_zero line 590
69. theorem OAI.Release075.TriangleRibbon.unique_outer_of_visits_one line 598
70. theorem OAI.Release075.TriangleRibbon.interior_angle_lower line 617

    Source documentation

    The full corner orbit at a vertex disjoint from the exterior is a genuinely reduced nonempty closed link walk.

    theorem interior_angle_lower (M : ℝ)
        (hclosed : ∀ a (p : L.Walk (label a) (label a)), 0 < p.length → ReducedWalk p →
          M ≤ weight (R.color (cl R.vertexPerm a)) * p.length)
        (v : R.Vertex) (hv : R.visits v = 0) : M ≤ R.angles v := by
    …

    Mentions: OAI.Release075.ReducedWalk, OAI.Release075.TriangleRibbon.weight

71. theorem OAI.Release075.TriangleRibbon.boundary_angle_lower line 656

    Source documentation

    A vertex with exactly one exterior corner has a reduced interior-sector path from the outgoing boundary direction back to the incoming one.

    theorem boundary_angle_lower
        (hboundary : ∀ a, R.IsOuter a →
          ∀ p : L.Walk (label (R.vertexPerm a)) (label a), ReducedWalk p →
            5 ≤ weight (R.color (cl R.vertexPerm a)) * p.length)
        (v : R.Vertex) (hv : R.visits v = 1) : 5 ≤ R.angles v := by
    …

    Mentions: OAI.Release075.ReducedWalk, OAI.Release075.TriangleRibbon.weight

72. theorem OAI.Release075.TriangleRibbon.not_all_turns_geodesic line 707

    Source documentation

    Gauss--Bonnet on the actual permutation ribbon now rules out a filling whose boundary turns are all separated by angle at least π in their target links.

    theorem not_all_turns_geodesic
        (hclosed : ∀ a (p : L.Walk (label a) (label a)), 0 < p.length → ReducedWalk p →
          10 ≤ weight (R.color (cl R.vertexPerm a)) * p.length)
        (hboundary : ∀ a, R.IsOuter a →
          ∀ p : L.Walk (label (R.vertexPerm a)) (label a), ReducedWalk p →
            5 ≤ weight (R.color (cl R.vertexPerm a)) * p.length) : False :=
    …

    Mentions: OAI.Release075.ReducedWalk, OAI.Release075.TriangleRibbon.weight