OAI/Algebra/GroupRing/ClosedWords.lean

GitHub source file

662 declarations, 0 contain sorry, 0 declared as axioms

Finite rotation systems. The Euler inequality here is explicitly an input from a planar realization; no PL realization or planar separator theorem is asserted by this file. The face cycles and bad-gap count, however, are computed from the actual boundary and pairing permutations.

  1. def OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.root line 14
  2. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.piece_eq line 16
  3. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.root_eq_some line 29
  4. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.cyclic_iff line 45
  5. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.cyclic line 48
  6. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.root_start line 59
  7. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.rootA line 63
  8. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.rootB line 71
  9. lemma OAI.TorsionFreeZeroDivisors.SingleException.cardinal_charge line 83
  10. lemma OAI.TorsionFreeZeroDivisors.SingleException.two_mass line 98
  11. lemma OAI.TorsionFreeZeroDivisors.SingleException.divide_cast line 102
  12. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.cap_pos line 119
  13. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.H₀ line 120
  14. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.H₀_ge line 122
  15. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.old_lower line 126
  16. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.piece_charge line 138
  17. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.lower_word line 147
  18. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.root_mass line 152
  19. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.added_real line 165
  20. abbrev OAI.TorsionFreeZeroDivisors.PermutationCycles.Cycle line 182
  21. instance OAI.TorsionFreeZeroDivisors.PermutationCycles.(instance at line 183) line 183
  22. def OAI.TorsionFreeZeroDivisors.PermutationCycles.cycle line 184
  23. def OAI.TorsionFreeZeroDivisors.PermutationCycles.members line 185
  24. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.mem_members line 186
  25. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.cycle_eq line 188
  26. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.cycle_apply line 190
  27. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.cycle_surjective line 194
  28. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.members_nonempty line 195
  29. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.mem_of_mem line 198
  30. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.card_one_fixed line 200
  31. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.card_le_two_square line 206
  32. def OAI.TorsionFreeZeroDivisors.PermutationCycles.fixed line 223
  33. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.fixed_le_cycles line 224
  34. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.singleton_cycles_le_fixed line 230
  35. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.sum_card line 245
  36. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.large_count line 249
  37. lemma OAI.TorsionFreeZeroDivisors.PlanarRotation.excess_identity line 263
  38. lemma OAI.TorsionFreeZeroDivisors.PlanarRotation.large_sum_le line 274
  39. def OAI.TorsionFreeZeroDivisors.PlanarRotation.opposite line 282
  40. def OAI.TorsionFreeZeroDivisors.PlanarRotation.Good line 284

    Source documentation

    An actual distinct-arc digon gap, read solely from the two permutations.

    def Good (x : O) : Prop :=
…
  41. def OAI.TorsionFreeZeroDivisors.PlanarRotation.bad line 286
  42. lemma OAI.TorsionFreeZeroDivisors.PlanarRotation.bad_card_bound line 287
  43. theorem OAI.TorsionFreeZeroDivisors.PlanarRotation.bad_gaps_le line 309

    Source documentation

    The exact 8N estimate. The planar input is only its explicit Euler inequality; no comparison-count estimate is assumed.

    theorem bad_gaps_le
    (heuler : Fintype.card O+4≤2*Fintype.card (Cycle σ)+2*Fintype.card (Cycle (opposite σ α)))
    (hmono : (fixed (opposite σ α)).card≤1) :
    (bad σ α).card≤8*Fintype.card (Cycle σ) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarRotation.opposite, OAI.TorsionFreeZeroDivisors.PlanarRotation.bad

  44. lemma OAI.TorsionFreeZeroDivisors.PlanarRotation.good_opposite line 334
  45. def OAI.TorsionFreeZeroDivisors.PlanarRotation.cuts line 349

    Source documentation

    Cut every bad gap and every prescribed marking together with its opposite.

    def cuts (marks : Finset O) : Finset O := bad σ α∪marks∪marks.image (opposite σ α)

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarRotation.bad, OAI.TorsionFreeZeroDivisors.PlanarRotation.opposite

  46. lemma OAI.TorsionFreeZeroDivisors.PlanarRotation.cardinal_cuts line 350
  47. lemma OAI.TorsionFreeZeroDivisors.PlanarRotation.cut_stable line 355
  48. theorem OAI.TorsionFreeZeroDivisors.PlanarRotation.cuts_le_twelve line 372

    Source documentation

    The source's J ≤ 12N', retaining the exact boundary and splitting count.

    theorem cuts_le_twelve (marks : Finset O) (pieces : ℕ)
    (heuler : Fintype.card O+4≤2*Fintype.card (Cycle σ)+2*Fintype.card (Cycle (opposite σ α)))
    (hmono : (fixed (opposite σ α)).card≤1)
    (hpieces : Fintype.card (Cycle σ)≤pieces)
    (hmarks : marks.card≤Fintype.card (Cycle σ)+pieces) :
    (cuts σ α marks).card≤12*pieces := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarRotation.opposite, OAI.TorsionFreeZeroDivisors.PlanarRotation.cuts

  49. structure OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem line 388

    Source documentation

    A finite circular boundary cut at least once in each boundary component.

    structure CutSystem (σ : Equiv.Perm O) where
…
  50. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.distance line 394
  51. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.finish line 395
  52. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.finish_mem line 396
  53. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.before line 397
  54. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.distance_zero line 399
  55. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.finish_cut line 402
  56. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.zero_iff line 404
  57. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.distance_next line 409
  58. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.finish_next line 419
  59. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.finish_surjective line 421
  60. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.distance_iterate line 425
  61. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.finish_iterate line 437
  62. structure OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired line 445

    Source documentation

    Every uncut adjacency is a distinct-arc digon, and cuts are stable under its opposite gap. These are precisely the hypotheses obtained by cutting bad and marked gaps in PlanarRotation.

    structure Paired (α : Equiv.Perm O) : Prop where
…
  63. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.opposite_next line 455
  64. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.opposite_uncut line 460
  65. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.finish_opposite line 462
  66. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.finish_pair line 466
  67. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.pair line 477
  68. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.pair_involutive line 478
  69. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.reverse_steps line 484
  70. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.pair_fixed_free line 506
  71. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.predecessor_cut line 525
  72. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.first line 533

    Source documentation

    Each cut is the last occurrence of its run; the first occurrence is the partner of the final occurrence of the opposite run.

    def first (c : {x // x∈S.cut}) : O := α (P.pair c).val
  73. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.finish_first line 534
  74. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.before_first_cut line 536
  75. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.distance_le_first line 539
  76. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.run_coordinates line 557
  77. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.run line 564
  78. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.mem_run line 566
  79. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.run_nonempty line 576
  80. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.run_nodup line 578
  81. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.belongs_opposite line 586
  82. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.distinct_runs line 593
  83. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.first_pair line 601
  84. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.distance_reverse line 604
  85. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.distance_first_pair line 619
  86. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.reverse_coordinate line 626
  87. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.run_reverse line 633
  88. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.PairOrbit.relation line 646
  89. abbrev OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.PairOrbit.Orbit line 657
  90. instance OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.PairOrbit.(instance at line 659) line 659
  91. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.PairOrbit.project line 660
  92. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.PairOrbit.fiber_two line 661
  93. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.PairOrbit.card_twice line 680
  94. abbrev OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.IntervalPair line 688
  95. instance OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.(instance at line 689) line 689
  96. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.twice_interval_pairs line 690
  97. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.Paired.interval_pairs_le line 692
  98. def OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.ofMarks line 700

    Source documentation

    The literal source cut construction has at least one cut per boundary, using one chosen indexing mark there.

    def ofMarks [Fintype O] (α : Equiv.Perm O) (marks : Finset O)
    (hmark : ∀ x,∃ y∈marks,σ.SameCycle x y) : CutSystem σ where
…

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem

  99. lemma OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.ofMarks_paired line 709
  100. theorem OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.source_interval_bound line 725

    Source documentation

    Exact 6N' interval-pair count for the finite rotation data of the manuscript. Euler planarity and the at-most-one exceptional monogon remain explicit geometric inputs; the resulting intervals and their reversal are constructed, not presumed.

    theorem source_interval_bound [Fintype O] (α : Equiv.Perm O) (marks : Finset O)
    (hmark : ∀ x,∃ y∈marks,σ.SameCycle x y)
    (hr : Function.Involutive α) (hf : ∀ x,α x≠x) (pieces : ℕ)
    (heuler : Fintype.card O+4≤2*Fintype.card (PermutationCycles.Cycle σ)+
      2*Fintype.card (PermutationCycles.Cycle (opposite σ α)))
    (hmono : (PermutationCycles.fixed (opposite σ α)).card≤1)
    (hpieces : Fintype.card (PermutationCycles.Cycle σ)≤pieces)
    (hmarks : marks.card≤Fintype.card (PermutationCycles.Cycle σ)+pieces) :
    Fintype.card (ofMarks_paired α marks hmark hr hf).IntervalPair≤6*pieces := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PermutationCycles.Cycle, OAI.TorsionFreeZeroDivisors.PermutationCycles.fixed, OAI.TorsionFreeZeroDivisors.PlanarRuns.CutSystem.ofMarks_paired

  101. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.position_ext line 747
  102. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.coordinate_iterate line 755
  103. def OAI.TorsionFreeZeroDivisors.PlanarIntervals.lower line 769
  104. def OAI.TorsionFreeZeroDivisors.PlanarIntervals.upper line 770
  105. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.finish_coordinates line 771
  106. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.bounds line 777
  107. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.finish_iff line 794
  108. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.finish_real_iff line 819
  109. lemma OAI.TorsionFreeZeroDivisors.PlanarIntervals.partner_coordinate line 836
  110. def OAI.TorsionFreeZeroDivisors.PlanarIntervals.comparisons line 855

    Source documentation

    Every actual maximal run yields a literal integer comparison side. No real-grid or arbitrary interval compatibility is postulated.

    def comparisons : Comparisons (E:={x // x∈S.cut}) len where
…
  111. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.positions_mono line 906
  112. def OAI.TorsionFreeZeroDivisors.ExtendComparisons.embed line 910
  113. abbrev OAI.TorsionFreeZeroDivisors.ExtendComparisons.Old line 912
  114. def OAI.TorsionFreeZeroDivisors.ExtendComparisons.project line 913
  115. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.old_embed line 914
  116. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.project_embed line 915
  117. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.embed_project line 916
  118. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.embed_injective line 917
  119. def OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner line 923
  120. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner_embed line 925
  121. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner_new line 927
  122. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner_inv line 929
  123. def OAI.TorsionFreeZeroDivisors.ExtendComparisons.side line 934
  124. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.side_embed line 936
  125. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.side_some_old line 938
  126. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.side_none line 942
  127. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.side_iff line 950
  128. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner_side line 967
  129. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner_source line 973
  130. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.partner_coordinate line 978
  131. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.target_range line 987
  132. def OAI.TorsionFreeZeroDivisors.ExtendComparisons.comparisons line 994
  133. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.old_card line 1014
  134. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.fixed_old_card line 1026
  135. lemma OAI.TorsionFreeZeroDivisors.ExtendComparisons.fixed_card line 1040
  136. lemma OAI.TorsionFreeZeroDivisors.WordPositions.bounds line 1064
  137. def OAI.TorsionFreeZeroDivisors.WordPositions.fin line 1067
  138. lemma OAI.TorsionFreeZeroDivisors.WordPositions.fin_val line 1083
  139. lemma OAI.TorsionFreeZeroDivisors.WordPositions.fin_symm_val line 1084
  140. lemma OAI.TorsionFreeZeroDivisors.WordPositions.dart_fin line 1086
  141. lemma OAI.TorsionFreeZeroDivisors.WordPositions.dart_prefix line 1090
  142. def OAI.TorsionFreeZeroDivisors.WordPositions.joinFin line 1099
  143. def OAI.TorsionFreeZeroDivisors.WordPositions.join line 1104
  144. lemma OAI.TorsionFreeZeroDivisors.WordPositions.join_first line 1106
  145. lemma OAI.TorsionFreeZeroDivisors.WordPositions.join_value line 1107
  146. def OAI.TorsionFreeZeroDivisors.WordPositions.segments line 1119
  147. lemma OAI.TorsionFreeZeroDivisors.WordPositions.segments_dart line 1122
  148. lemma OAI.TorsionFreeZeroDivisors.WordPositions.cardinal line 1133
  149. abbrev OAI.TorsionFreeZeroDivisors.WordPositions.prefix_bound line 1137
  150. lemma OAI.TorsionFreeZeroDivisors.WordPositions.new_card line 1140
  151. lemma OAI.TorsionFreeZeroDivisors.WordPositions.fixed_card line 1150
  152. lemma OAI.TorsionFreeZeroDivisors.WordPositions.nonfixed_old line 1160
  153. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.grow line 1183
  154. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.upper_real line 1186
  155. def OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.system line 1192

    Source documentation

    Appending the actual short closures changes neither original comparison nor its underlying graph lifts. Every newly added position is unpaired.

    def system : PathSystem rep r x y where
…

    Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem

  156. def OAI.TorsionFreeZeroDivisors.BoundaryRotation.perm line 1243
  157. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.apply_fin line 1245
  158. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.pow_fin line 1249
  159. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.first line 1254
  160. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.finRotate_same line 1257
  161. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.same_first line 1266
  162. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.next line 1280
  163. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.cycles_le line 1303
  164. def OAI.TorsionFreeZeroDivisors.BoundaryRotation.ends line 1312
  165. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.ends_le line 1313
  166. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.hits line 1325
  167. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.fixed_root_end line 1344
  168. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.monogons_le line 1357
  169. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.last_next line 1374
  170. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.step_nonlast line 1393
  171. lemma OAI.TorsionFreeZeroDivisors.BoundaryRotation.step_last line 1403
  172. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.step_label line 1420
  173. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.boundary_reduced line 1426
  174. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.pow_apply line 1444
  175. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.sameCycle line 1448
  176. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.involutive line 1451
  177. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.fixed_free line 1455
  178. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.mul line 1459
  179. abbrev OAI.TorsionFreeZeroDivisors.BalancedRotation.len line 1468
  180. abbrev OAI.TorsionFreeZeroDivisors.BalancedRotation.e line 1469
  181. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.source line 1471
  182. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.value line 1473
  183. def OAI.TorsionFreeZeroDivisors.BalancedRotation.perm line 1476
  184. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.transport line 1479
  185. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.same_source line 1482
  186. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.step line 1488
  187. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.hits line 1513
  188. lemma OAI.TorsionFreeZeroDivisors.BalancedRotation.cycles_le line 1523
  189. structure OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing line 1543

    Source documentation

    The full inverse-letter pairing of the original boundary words, retaining actual graph lifts. Planarity is additional data, not asserted here.

    structure FullPairing (s : PathSystem rep r x y) where
…

    Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem

  190. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.α line 1553
  191. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.α_involutive line 1554
  192. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.α_fixed_free line 1556
  193. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.transport line 1558
  194. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.cuts line 1560
  195. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.paired line 1563
  196. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.step line 1566
  197. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.Side line 1579
  198. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.comparisons line 1580
  199. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.lower line 1582
  200. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.upper line 1583
  201. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.bounds line 1584
  202. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.lower_eq line 1589
  203. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.upper_eq line 1592
  204. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.lower_le line 1595
  205. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.upper_le line 1599
  206. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.dart line 1601
  207. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.balanced_reduced line 1603
  208. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.balanced_compatible line 1608
  209. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.sameCycle_iff line 1618
  210. def OAI.TorsionFreeZeroDivisors.PermutationTransport.cycles line 1626
  211. lemma OAI.TorsionFreeZeroDivisors.PermutationTransport.card_cycles line 1627
  212. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.opposite_eq line 1638
  213. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.opposite_transport line 1642
  214. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.monogons line 1648
  215. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.Euler line 1663

    Source documentation

    Only Euler planarity is needed in the interval-count argument. This file proves neither Euler planarity for an abstract pairing nor its PL realization.

    def Euler : Prop := Fintype.card (Position (fun t=>(s.paths t).length))+4≤
…
  216. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.balanced_euler line 1666
  217. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.sides_le line 1674
  218. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.closed line 1691

    Source documentation

    The actual balanced and short-closed system, with all cut comparisons and all closure positions left unpaired.

    def closed : PathSystem rep r x y := ClosedWords.system s cap hc hL hd (a.comparisons cap hc)
…

    Mentions: OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem, OAI.TorsionFreeZeroDivisors.SampleGraph.ClosedWords.system

  219. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.closed_fixed line 1695
  220. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.closed_old line 1699
  221. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Small line 1717

    Source documentation

    Every retained vertex lies in a small set closed under all retained edges.

    def Small (S : Finset V) (K : ℕ) : Prop :=
…
  222. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.small_of_card line 1722
  223. structure OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split line 1727

    Source documentation

    A genuine one-step separator, including its actual components/blocks.

    structure Split (S : Finset V) where
…
  224. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.subset line 1739
  225. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.mass line 1743
  226. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.smaller line 1749
  227. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.q line 1754
  228. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.a line 1755
  229. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Csep line 1756
  230. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.q_pos line 1757
  231. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.q_lt_one line 1758
  232. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.a_pos line 1762
  233. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Csep_pos line 1763
  234. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Csep_identity line 1764
  235. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.sqrt_size line 1766
  236. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.child_charge line 1774

    Source documentation

    Charge bound for one recursive child, including leaves that incur no cost.

    lemma child_charge {K s b : ℕ} (hK : 0<K) (hs : K<s) (hb : 3*b≤2*s)
    {d : ℝ} (hd : if b≤K then d=0 else d≤Csep*b/Real.sqrt K-Csep*q*Real.sqrt b) :
    d≤Csep*b/Real.sqrt K-Csep*b/Real.sqrt s := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Csep, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.q

  237. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.parent_charge line 1796
  238. def OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.combined line 1823
  239. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.child_deleted line 1824
  240. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.combined_subset line 1827
  241. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.combined_small line 1833
  242. lemma OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split.combined_card line 1852
  243. theorem OAI.TorsionFreeZeroDivisors.RecursiveSeparator.recursive line 1857

    Source documentation

    Exact recursive deletion, with a stronger potential bound used internally.

    theorem recursive (K : ℕ) (hK : 0<K)
    (oneStep : ∀ S : Finset V,K<S.card → Nonempty (Split R S)) (S : Finset V) :
    ∃ D : Finset V,D⊆S ∧ Small R (S\D) K ∧
      (if S.card≤K then D=∅ else
        (D.card:ℝ)≤Csep*S.card/Real.sqrt K-Csep*q*Real.sqrt S.card) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Small, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Csep, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.q

  244. theorem OAI.TorsionFreeZeroDivisors.RecursiveSeparator.separator line 1918

    Source documentation

    Source recursive planar-separation bound, once the actual one-step planar separator is supplied for every induced subgraph.

    theorem separator (K : ℕ) (hK : 1≤K)
    (oneStep : ∀ S : Finset V,K<S.card → Nonempty (Split R S)) (S : Finset V) :
    ∃ D : Finset V,D⊆S ∧ Small R (S\D) K ∧ (D.card:ℝ)≤Csep*S.card/Real.sqrt K := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Split, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Small, OAI.TorsionFreeZeroDivisors.RecursiveSeparator.Csep

  245. def OAI.TorsionFreeZeroDivisors.PlanarParameters.U line 1933
  246. def OAI.TorsionFreeZeroDivisors.PlanarParameters.η line 1934
  247. def OAI.TorsionFreeZeroDivisors.PlanarParameters.K line 1935
  248. def OAI.TorsionFreeZeroDivisors.PlanarParameters.C line 1936
  249. def OAI.TorsionFreeZeroDivisors.PlanarParameters.C₂ line 1937
  250. def OAI.TorsionFreeZeroDivisors.PlanarParameters.sides line 1939

    Source documentation

    Oriented interval sides; the manuscript's I counts pairs.

    def sides : ℕ := 2*C₂*C ε D

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarParameters.C₂, OAI.TorsionFreeZeroDivisors.PlanarParameters.C

  251. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.U_ge line 1940
  252. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.U_pos line 1941
  253. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.η_pos line 1942
  254. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.K_pos line 1945
  255. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.C_pos line 1946
  256. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.sides_pos line 1947
  257. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.closure_loss line 1951
  258. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.deletion_loss line 1958
  259. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.unpaired_loss line 1964
  260. lemma OAI.TorsionFreeZeroDivisors.PlanarParameters.separator_factor line 1970
  261. theorem OAI.TorsionFreeZeroDivisors.PlanarParameters.delete line 1985

    Source documentation

    No planar theorem is hidden here: this uses the actual one-step Split objects and constructs a literal deletion set, with the fixed source K.

    theorem delete {V : Type} [Fintype V] (R : V → V → Prop) (hε : 0<ε)
    (oneStep : ∀ S : Finset V,K ε D<S.card → Nonempty (Split R S)) :
    ∃ A : Finset V,Small R (Finset.univ\A) (K ε D) ∧
      (A.card:ℝ)≤η ε D*Fintype.card V := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarParameters.K, OAI.TorsionFreeZeroDivisors.PlanarParameters.η

  262. def OAI.TorsionFreeZeroDivisors.LocalizationCounts.deletedMap line 2003
  263. lemma OAI.TorsionFreeZeroDivisors.LocalizationCounts.deleted_injective line 2007
  264. lemma OAI.TorsionFreeZeroDivisors.LocalizationCounts.deleted_nonfixed_le line 2020

    Source documentation

    Only deleted ORIGINAL occurrences, not closures, can destroy a partner.

    lemma deleted_nonfixed_le :
    (Finset.univ.filter (fun p : Position len=>¬keep p.1 ∧ C.pairing.partner p≠p)).card≤
      ∑t∈Finset.univ.filter (fun t=>¬keep t),old t := by
…
  265. lemma OAI.TorsionFreeZeroDivisors.LocalizationCounts.deleted_mass line 2030

    Source documentation

    The exact removed-original-position bound, from the actual deletion set.

    lemma deleted_mass {U L : ℕ} {η H₀ : ℝ}
    (hcap : ∀ t,old t≤U*L) (hη : 0≤η)
    (hcount : ((Finset.univ.filter (fun t=>¬keep t)).card:ℝ)≤η*Fintype.card T)
    (hpieces : (Fintype.card T:ℝ)*L≤2*H₀) :
    (∑t∈Finset.univ.filter (fun t=>¬keep t),(old t:ℝ))≤2*η*U*H₀ := by
…
  266. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε line 2051
  267. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε_pos line 2052
  268. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.excluded_of_separator line 2061

    Source documentation

    The complete deterministic separator-to-forbidden-system implication. The one-step separator is explicitly the still-missing planar geometry input; the deletion set, losses, clusters, and realized forbidden words are constructed.

    theorem excluded_of_separator (D : ℕ) (H₀ : ℝ) (old : s.P → ℕ)
    (hH₀ : 0<H₀) (hL : 0<L (size rep))
    (ho : ∀ t,old t≤(s.paths t).length)
    (hcapOld : ∀ t,old t≤PlanarParameters.U ε D*L (size rep))
    (hcap : ∀ t,(s.paths t).length≤(PlanarParameters.U ε D+D)*L (size rep))
    (hbase : H₀≤∑t,(old t:ℝ))
    (hpieces : (Fintype.card s.P:ℝ)*L (size rep)≤2*H₀)
    (hadded : ((Finset.univ.filter (fun p=>s.comparisons.pairing.partner p=p)).card:ℝ)≤
      3*(D:ℝ)/PlanarParameters.U ε D*H₀)
    (hprefix : ∀ p : Position (fun t=>(s.paths t).length),s.comparisons.pairing.partner p≠p →
      p.2.val∈BlockAlignment.positions 0 (old p.1))
    (hcompare : Fintype.card s.E≤12*Fintype.card s.P)
…

    Mentions: OAI.TorsionFreeZeroDivisors.PlanarParameters.U, OAI.TorsionFreeZeroDivisors.SampleGraph.PathSystem.ε, OAI.TorsionFreeZeroDivisors.BlockAlignment.positions

  269. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.U₀ line 2155
  270. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.U₀_ge line 2156
  271. lemma OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.cap_lower line 2157
  272. abbrev OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.cap_positive line 2160
  273. def OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.prepared line 2166
  274. theorem OAI.TorsionFreeZeroDivisors.SampleGraph.FullPairing.excluded line 2170

    Source documentation

    Literal full-pairing exclusion. Euler planarity and the one-step separator are the two remaining geometric inputs, not extra source hypotheses on the main theorem. No claim of their unconditional existence is made here.

    theorem excluded (hr : r∈samples rep) (hordinary : ∃t,s.root≠some t) (heuler : a.Euler)
    (oneStep : ∀ S : Finset (a.prepared hL hd).P,PlanarParameters.K PathSystem.ε ClosedWords.D<S.card →
      Nonempty (RecursiveSeparator.Split
        (PairingClusters.Rel (fun p : Position (fun t=>((a.prepared hL hd).paths t).length)=>p.1)
          (a.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 := by
…

    Mentions: 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

  275. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.invariant_pow line 2215
  276. def OAI.TorsionFreeZeroDivisors.PermutationCycles.lift line 2220
  277. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.lift_cycle line 2226
  278. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.lift_surjective line 2228
  279. def OAI.TorsionFreeZeroDivisors.InsertedRotation.rotation line 2240
  280. def OAI.TorsionFreeZeroDivisors.InsertedRotation.pairing line 2243
  281. def OAI.TorsionFreeZeroDivisors.InsertedRotation.face line 2244
  282. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.rotation_left line 2245
  283. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.rotation_p line 2247
  284. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.rotation_false line 2249
  285. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.rotation_true line 2251
  286. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.face_left line 2253
  287. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.face_p line 2255
  288. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.face_false line 2257
  289. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.face_true line 2259
  290. def OAI.TorsionFreeZeroDivisors.InsertedRotation.classify line 2262
  291. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.classify_invariant line 2266
  292. lemma OAI.TorsionFreeZeroDivisors.InsertedRotation.classify_surjective line 2274
  293. theorem OAI.TorsionFreeZeroDivisors.InsertedRotation.face_count line 2283

    Source documentation

    Inserting an ear creates a new face and retains all old face cycles.

    theorem face_count : Fintype.card (Cycle (α*σ))+1≤Fintype.card (Cycle (face σ α p)) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.InsertedRotation.face

  294. abbrev OAI.TorsionFreeZeroDivisors.SwapCycles.Away line 2296
  295. def OAI.TorsionFreeZeroDivisors.SwapCycles.classify line 2297
  296. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.classify_apply line 2299
  297. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.classify_p line 2301
  298. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.classify_q line 2302
  299. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.classify_swap line 2303
  300. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.invariant line 2309
  301. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.surjective line 2311
  302. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.lower line 2322
  303. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.away_count line 2326
  304. theorem OAI.TorsionFreeZeroDivisors.SwapCycles.count_le line 2341

    Source documentation

    A two-endpoint switch loses at most one permutation cycle.

    theorem count_le : Fintype.card (Cycle f)≤Fintype.card (Cycle (Equiv.swap p q*f))+1 := by
…
  305. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.cycle_swap line 2352
  306. def OAI.TorsionFreeZeroDivisors.SwapCycles.adjacentClass line 2360
  307. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.adjacent_fixed line 2361
  308. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.adjacentClass_invariant line 2362
  309. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.adjacentClass_surjective line 2372
  310. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.count_reverse line 2384
  311. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.adjacent_count line 2388

    Source documentation

    Switching the two arrows adjacent to a nonfixed point splits off that point as one new actual cycle.

    lemma adjacent_count (hp : f p≠p) :
    Fintype.card (Cycle (Equiv.swap p (f p)*f))=Fintype.card (Cycle f)+1 := by
…
  312. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.adjacent_support line 2394
  313. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.away_same line 2410
  314. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.same_monotone line 2421
  315. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.identity_count line 2431
  316. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.sign_formula line 2437

    Source documentation

    The ordinary permutation sign in terms of all cycles, including fixed points.

    lemma sign_formula (f : Equiv.Perm O) :
    Equiv.Perm.sign f=(-1 : ℤˣ)^(Fintype.card O+Fintype.card (Cycle f)) := by
…
  317. theorem OAI.TorsionFreeZeroDivisors.SwapCycles.split_count line 2461

    Source documentation

    A switch between distinct positions of one cycle splits it in two.

    theorem split_count (f : Equiv.Perm O) (p q : O) (hpq : p≠q)
    (h : cycle f p=cycle f q) :
    Fintype.card (Cycle (Equiv.swap p q*f))=Fintype.card (Cycle f)+1 := by
…
  318. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.face_switch line 2482
  319. theorem OAI.TorsionFreeZeroDivisors.SwapCycles.split_euler line 2490

    Source documentation

    The global sphere Euler lower bound is preserved when one boundary cycle is split at two distinct positions. This finite statement does not identify which realized component contains the outer disk in a self-band surgery.

    theorem split_euler (hpq : p≠q) (h : cycle σ p=cycle σ q)
    (he : Fintype.card O+4≤2*Fintype.card (Cycle σ)+2*Fintype.card (Cycle (α*σ))) :
    Fintype.card O+4≤2*Fintype.card (Cycle (Equiv.swap p q*σ))+
      2*Fintype.card (Cycle (α*(Equiv.swap p q*σ))) := by
…
  320. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.merge_same line 2505

    Source documentation

    Switching two distinct cycles joins the two selected positions in one actual new cycle. The witness follows the old cycle up to its first return.

    lemma merge_same (h : cycle f p≠cycle f q) :
    (Equiv.swap p q*f).SameCycle p q := by
…
  321. lemma OAI.TorsionFreeZeroDivisors.SwapCycles.merge_count line 2535
  322. def OAI.TorsionFreeZeroDivisors.ComponentEuler.Refines line 2547
  323. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.refines_of_invariant line 2548
  324. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.merge_refines line 2552
  325. def OAI.TorsionFreeZeroDivisors.ComponentEuler.merge line 2563
  326. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.merge_refines' line 2565
  327. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.merge_pair line 2569
  328. def OAI.TorsionFreeZeroDivisors.ComponentEuler.forest line 2574
  329. def OAI.TorsionFreeZeroDivisors.ComponentEuler.face line 2577
  330. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.face_invariant line 2580
  331. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.face_refines line 2588
  332. theorem OAI.TorsionFreeZeroDivisors.ComponentEuler.upper line 2593

    Source documentation

    Euler's upper bound for the actual component partition formed by gluing listed bands. The forest permutation is a computed partition, not a planar input.

    theorem upper (σ : Equiv.Perm O) (l : List (O×O)) :
    Nat.card (Cycle σ)+Nat.card (Cycle (face σ l))≤
      l.length+2*Nat.card (Cycle (forest σ l)) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.ComponentEuler.face, OAI.TorsionFreeZeroDivisors.ComponentEuler.forest

  333. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.forest_refines line 2610
  334. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.forest_pair line 2614
  335. def OAI.TorsionFreeZeroDivisors.ComponentEuler.Edge line 2623
  336. abbrev OAI.TorsionFreeZeroDivisors.ComponentEuler.Component line 2625
  337. def OAI.TorsionFreeZeroDivisors.ComponentEuler.component line 2626
  338. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.forest_of_component line 2627
  339. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.invariant_forest line 2641
  340. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.component_invariant line 2663
  341. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.component_of_forest line 2670
  342. def OAI.TorsionFreeZeroDivisors.ComponentEuler.componentEquiv line 2674
  343. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.upper_components line 2681
  344. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.connected_upper line 2686
  345. def OAI.TorsionFreeZeroDivisors.PairingFactors.strip line 2702
  346. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_p line 2704
  347. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_q line 2707
  348. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_away line 2710
  349. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_involutive line 2716
  350. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_support line 2727
  351. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_card line 2738
  352. theorem OAI.TorsionFreeZeroDivisors.PairingFactors.factorization line 2759

    Source documentation

    Every finite involution is literally a product of its own nontrivial paired-edge swaps, with exactly one factor for each pair.

    theorem factorization : ∃l : List (O×O),
    (l.map (fun e=>Equiv.swap e.1 e.2)).prod=α ∧
      2*l.length=α.support.card ∧ ∀e∈l,e.1≠e.2 ∧ α e.1=e.2 := by
…
  353. lemma OAI.TorsionFreeZeroDivisors.MapEuler.product_invariant line 2799
  354. lemma OAI.TorsionFreeZeroDivisors.MapEuler.face_product line 2817
  355. def OAI.TorsionFreeZeroDivisors.MapEuler.Edge line 2823
  356. abbrev OAI.TorsionFreeZeroDivisors.MapEuler.Component line 2824
  357. def OAI.TorsionFreeZeroDivisors.MapEuler.component line 2825
  358. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_forest line 2831
  359. lemma OAI.TorsionFreeZeroDivisors.MapEuler.forest_alpha line 2838
  360. lemma OAI.TorsionFreeZeroDivisors.MapEuler.forest_component line 2842
  361. def OAI.TorsionFreeZeroDivisors.MapEuler.componentEquiv line 2855
  362. lemma OAI.TorsionFreeZeroDivisors.MapEuler.upper_factors line 2863
  363. theorem OAI.TorsionFreeZeroDivisors.MapEuler.upper line 2871

    Source documentation

    Every finite orientable permutation map obeys the Euler upper bound. This uses only its actual involution and actual connected-component equivalence; no topological realization or Euler inequality is assumed.

    theorem upper (hi : Function.Involutive α) :
    2*Nat.card (Cycle σ)+2*Nat.card (Cycle (α*σ))≤α.support.card+4*Nat.card (Component σ α) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.Component

  364. lemma OAI.TorsionFreeZeroDivisors.MapEuler.fixedFree_upper line 2876
  365. lemma OAI.TorsionFreeZeroDivisors.MapEuler.connected_upper line 2881
  366. def OAI.TorsionFreeZeroDivisors.ComponentEuler.handles line 2899

    Source documentation

    A handle is precisely an edge whose endpoints are already in one component but which merges two distinct face cycles when glued.

    def handles (σ : Equiv.Perm O) : List (O×O) → ℕ
  | []=>0
  | e::l=>handles σ l+if cycle (forest σ l) e.1=cycle (forest σ l) e.2 ∧
      cycle (face σ l) e.1≠cycle (face σ l) e.2 then 1 else 0
omit [Fintype O] in

    Mentions: OAI.TorsionFreeZeroDivisors.ComponentEuler.forest, OAI.TorsionFreeZeroDivisors.ComponentEuler.face

  367. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.handles_tail line 2904
  368. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.handles_exact line 2906
  369. lemma OAI.TorsionFreeZeroDivisors.ComponentEuler.zero_handles line 2934
  370. def OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero line 2947

    Source documentation

    Combinatorial genus zero, including disconnected maps and isolated darts. This is a definition in permutation data, not an asserted sphere embedding.

    def GenusZero : Prop :=
…
  371. lemma OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_of_lower line 2949
  372. lemma OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_iff_handles line 2952
  373. lemma OAI.TorsionFreeZeroDivisors.PairingFactors.strip_edge line 2965
  374. lemma OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_strip line 2982

    Source documentation

    Deleting an actual paired edge cannot create a handle in any component.

    lemma genusZero_strip (hz : GenusZero σ α) (p : O) (hp : α p≠p) : GenusZero σ (strip α p) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero

  375. lemma OAI.TorsionFreeZeroDivisors.MapEuler.dual_rel line 3001
  376. lemma OAI.TorsionFreeZeroDivisors.MapEuler.dual_twice line 3015
  377. def OAI.TorsionFreeZeroDivisors.MapEuler.dualEquiv line 3018
  378. lemma OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_dual line 3023
  379. theorem OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_band line 3031

    Source documentation

    The actual band splice preserves componentwise combinatorial genus zero, prior to bypassing its two now-unpaired occurrences. Both the merge and the split vertex cases are covered by dual edge deletion.

    theorem genusZero_band (hz : GenusZero σ α) (p : O) (hp : α p≠p) :
    GenusZero (Equiv.swap p (α p)*σ) (strip α p) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero

  380. abbrev OAI.TorsionFreeZeroDivisors.DeleteCycle.Rest line 3047
  381. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.invariant line 3048
  382. def OAI.TorsionFreeZeroDivisors.DeleteCycle.restrict line 3052
  383. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.restrict_pow line 3053
  384. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.restrict_same line 3057
  385. def OAI.TorsionFreeZeroDivisors.DeleteCycle.classify line 3072
  386. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.classify_apply line 3075
  387. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.classify_surjective line 3083
  388. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.classify_eq line 3090
  389. def OAI.TorsionFreeZeroDivisors.DeleteCycle.cycleEquiv line 3102
  390. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.fixed_count line 3109
  391. def OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass line 3114

    Source documentation

    Delete an occurrence by bypassing it in its boundary cycle.

    def bypass : Equiv.Perm (Rest p) := restrict (Equiv.swap p (f p)*f) p (SwapCycles.adjacent_fixed f p)

    Mentions: OAI.TorsionFreeZeroDivisors.DeleteCycle.Rest, OAI.TorsionFreeZeroDivisors.DeleteCycle.restrict, OAI.TorsionFreeZeroDivisors.SwapCycles.adjacent_fixed

  392. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass_count line 3115
  393. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass_apply line 3124
  394. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass_mul line 3127

    Source documentation

    Bypassing a point commutes with a left permutation fixing that point.

    lemma bypass_mul [Fintype O] (a : Equiv.Perm O) (ha : a p=p) :
    bypass (a*f) p=restrict a p ha*bypass f p := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass, OAI.TorsionFreeZeroDivisors.DeleteCycle.restrict

  395. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass_nonfixed line 3134
  396. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.card_rest line 3146
  397. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_rotation line 3157
  398. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_partner line 3159
  399. def OAI.TorsionFreeZeroDivisors.MapEuler.lift line 3161
  400. lemma OAI.TorsionFreeZeroDivisors.MapEuler.lift_component line 3172
  401. lemma OAI.TorsionFreeZeroDivisors.MapEuler.swap_invariant line 3174
  402. abbrev OAI.TorsionFreeZeroDivisors.MapDeletion.rotation line 3187
  403. abbrev OAI.TorsionFreeZeroDivisors.MapDeletion.partner line 3188
  404. def OAI.TorsionFreeZeroDivisors.MapDeletion.push line 3189
  405. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.push_p line 3191
  406. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.push_val line 3193
  407. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.push_rotation line 3194
  408. def OAI.TorsionFreeZeroDivisors.MapDeletion.projectRaw line 3201
  409. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.project_rotation line 3203
  410. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.project_partner line 3214
  411. def OAI.TorsionFreeZeroDivisors.MapDeletion.project line 3221
  412. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.include_rotation line 3223
  413. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.include_partner line 3227
  414. def OAI.TorsionFreeZeroDivisors.MapDeletion.inclusion line 3229
  415. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.component_push line 3232
  416. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.left_inverse line 3236
  417. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.project_surjective line 3240
  418. def OAI.TorsionFreeZeroDivisors.MapDeletion.componentEquiv line 3246
  419. def OAI.TorsionFreeZeroDivisors.MapDeletion.support_equiv line 3252
  420. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.support_count line 3265
  421. lemma OAI.TorsionFreeZeroDivisors.MapDeletion.face_nonfixed line 3269
  422. theorem OAI.TorsionFreeZeroDivisors.MapDeletion.genusZero_delete line 3274

    Source documentation

    Removing a dart fixed by the partner involution preserves all actual map components and the Euler equality when its vertex is not a singleton.

    theorem genusZero_delete (hs : σ p≠p) (hz : GenusZero σ α) :
    GenusZero (rotation σ p) (partner α p ha) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapDeletion.rotation, OAI.TorsionFreeZeroDivisors.MapDeletion.partner

  423. abbrev OAI.TorsionFreeZeroDivisors.BandEuler.q' line 3303
  424. abbrev OAI.TorsionFreeZeroDivisors.BandEuler.Residual line 3304
  425. def OAI.TorsionFreeZeroDivisors.BandEuler.adjusted line 3305
  426. lemma OAI.TorsionFreeZeroDivisors.BandEuler.adjusted_p line 3308
  427. lemma OAI.TorsionFreeZeroDivisors.BandEuler.adjusted_q line 3313
  428. def OAI.TorsionFreeZeroDivisors.BandEuler.α₁ line 3315
  429. lemma OAI.TorsionFreeZeroDivisors.BandEuler.α₁_q line 3317
  430. def OAI.TorsionFreeZeroDivisors.BandEuler.partner line 3321
  431. def OAI.TorsionFreeZeroDivisors.BandEuler.switched line 3323
  432. def OAI.TorsionFreeZeroDivisors.BandEuler.rotation line 3324
  433. def OAI.TorsionFreeZeroDivisors.BandEuler.face line 3325
  434. def OAI.TorsionFreeZeroDivisors.BandEuler.val line 3327
  435. lemma OAI.TorsionFreeZeroDivisors.BandEuler.val_ne_p line 3329
  436. lemma OAI.TorsionFreeZeroDivisors.BandEuler.val_ne_q line 3331
  437. lemma OAI.TorsionFreeZeroDivisors.BandEuler.val_injective line 3335
  438. lemma OAI.TorsionFreeZeroDivisors.BandEuler.partner_val line 3339
  439. lemma OAI.TorsionFreeZeroDivisors.BandEuler.partner_involutive line 3344
  440. lemma OAI.TorsionFreeZeroDivisors.BandEuler.partner_distinct line 3350
  441. lemma OAI.TorsionFreeZeroDivisors.BandEuler.face_eq line 3355
  442. lemma OAI.TorsionFreeZeroDivisors.BandEuler.switched_p line 3368
  443. lemma OAI.TorsionFreeZeroDivisors.BandEuler.switched_q line 3377
  444. lemma OAI.TorsionFreeZeroDivisors.BandEuler.switched_p_ne_q line 3386
  445. lemma OAI.TorsionFreeZeroDivisors.BandEuler.face_p_ne_q line 3393
  446. lemma OAI.TorsionFreeZeroDivisors.BandEuler.rotation_count line 3397
  447. lemma OAI.TorsionFreeZeroDivisors.BandEuler.face_count line 3406
  448. lemma OAI.TorsionFreeZeroDivisors.BandEuler.two_fewer line 3414
  449. theorem OAI.TorsionFreeZeroDivisors.BandEuler.euler line 3423

    Source documentation

    The literal removal of a paired band preserves the global sphere Euler lower bound. No componentwise planarity or essentiality is concluded here.

    theorem euler (he : Fintype.card O+4≤2*Fintype.card (Cycle σ)+2*Fintype.card (Cycle (face σ α))) :
    Fintype.card (Residual p q hpq)+4≤2*Fintype.card (Cycle (rotation σ p q hpq))+
      2*Fintype.card (Cycle (partner α hi p q hpq hpair*rotation σ p q hpq)) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BandEuler.face, OAI.TorsionFreeZeroDivisors.BandEuler.Residual, OAI.TorsionFreeZeroDivisors.BandEuler.rotation, OAI.TorsionFreeZeroDivisors.BandEuler.partner

  450. lemma OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_fintype line 3433
  451. lemma OAI.TorsionFreeZeroDivisors.BandEuler.adjusted_strip line 3445
  452. lemma OAI.TorsionFreeZeroDivisors.BandEuler.switched_genusZero line 3451
  453. theorem OAI.TorsionFreeZeroDivisors.BandEuler.genusZero line 3461

    Source documentation

    The genuine remaining map after deleting a paired band has genus zero in all its actual components. This strengthens the global Euler estimate and uses no assumed planar embedding. Local degenerate faces are explicitly excluded.

    theorem genusZero (hz : GenusZero σ α) (hs : σ p≠p)
    (hfp : face σ α p≠p) (hfq : face σ α q≠q) :
    GenusZero (rotation σ p q hpq) (partner α hi p q hpq hpair) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BandEuler.face, OAI.TorsionFreeZeroDivisors.BandEuler.rotation, OAI.TorsionFreeZeroDivisors.BandEuler.partner

  454. structure OAI.TorsionFreeZeroDivisors.WordPairing.Data line 3485
  455. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.raise line 3494
  456. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.raise_lt line 3496
  457. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.raise_injective line 3499
  458. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.raise_avoid line 3505
  459. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.insert line 3509
  460. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.insert_injective line 3513
  461. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.insert_surjective line 3532
  462. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.equiv line 3548
  463. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.equiv_left line 3550
  464. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.equiv_false line 3551
  465. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.equiv_true line 3552
  466. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.sumPartner line 3555
  467. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.partner line 3557
  468. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.partner_apply line 3559
  469. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.involutive line 3563
  470. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.distinct line 3571
  471. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.noncrossing line 3580
  472. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Data.reindex_apply line 3621
  473. def OAI.TorsionFreeZeroDivisors.WordPairing.Data.reindex line 3625
  474. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.labels line 3654
  475. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.labels_left line 3656
  476. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.labels_false line 3659
  477. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.labels_true line 3662
  478. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.data line 3666
  479. lemma OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.get_old line 3691
  480. lemma OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.get_first line 3699
  481. lemma OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.get_second line 3702
  482. lemma OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.length_eq line 3712
  483. def OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.orderIso line 3716
  484. lemma OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.labels_eq line 3719
  485. def OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.data line 3742
  486. def OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter line 3748
  487. lemma OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter_involutive line 3749
  488. def OAI.TorsionFreeZeroDivisors.WordPairing.emptyData line 3754
  489. theorem OAI.TorsionFreeZeroDivisors.WordPairing.of_reduction line 3761
  490. theorem OAI.TorsionFreeZeroDivisors.WordPairing.of_identity line 3771
  491. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.rotate_val line 3785
  492. def OAI.TorsionFreeZeroDivisors.WordPairing.Ear.previous line 3793
  493. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.previous_rotate line 3796
  494. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.rotate_old line 3802
  495. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.rotate_false line 3810
  496. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.rotate_true line 3815
  497. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.rotation_transport line 3823
  498. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.rotation_eq line 3839
  499. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.face_eq line 3848
  500. theorem OAI.TorsionFreeZeroDivisors.WordPairing.Ear.face_count line 3855
  501. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.card_identity line 3865
  502. def OAI.TorsionFreeZeroDivisors.WordPairing.DiskEuler line 3880

    Source documentation

    The disk Euler estimate for the actual circle rotation and word matching. The empty word is distinguished, since it has no boundary occurrences.

    def DiskEuler (d : Data inv label) : Prop :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordPairing.Data

  503. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Data.reindex_euler line 3883
  504. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.empty_rotation line 3891
  505. lemma OAI.TorsionFreeZeroDivisors.WordPairing.Ear.euler line 3903
  506. lemma OAI.TorsionFreeZeroDivisors.WordPairing.ListInsert.data_euler line 3922
  507. theorem OAI.TorsionFreeZeroDivisors.WordPairing.of_reduction_euler line 3931

    Source documentation

    The face-count input is now proved for the matching constructed from literal free cancellation. This does not yet claim a multi-disk PL realization.

    theorem of_reduction_euler {w : List (A×Bool)} (h : FreeGroup.Red w []) :
    ∃ d : Data inverseLetter w.get,DiskEuler d := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordPairing.Data, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter, OAI.TorsionFreeZeroDivisors.WordPairing.DiskEuler

  508. theorem OAI.TorsionFreeZeroDivisors.WordPairing.of_identity_euler line 3942
  509. theorem OAI.TorsionFreeZeroDivisors.WordPairing.adjacent_ear line 3955

    Source documentation

    Every nonempty finite noncrossing perfect matching has a literal adjacent ear, obtained by minimizing the positive distance between matched positions.

    theorem adjacent_ear (d : Data inv label) (hn : 0 < n) :
    ∃i : Fin n,(d.partner i).val=i.val+1 := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordPairing.Data

  510. lemma OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.back line 4004
  511. lemma OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.remains line 4007
  512. def OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.lower line 4022
  513. lemma OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.lower_spec line 4023
  514. lemma OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.lower_involutive line 4025
  515. def OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.data line 4030
  516. lemma OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.recover line 4050
  517. lemma OAI.TorsionFreeZeroDivisors.WordPairing.EraseEar.euler line 4062
  518. theorem OAI.TorsionFreeZeroDivisors.WordPairing.Data.diskEuler line 4072

    Source documentation

    Every literal finite noncrossing inverse-letter matching has the disk Euler estimate, independently of its choice as a free cancellation witness.

    theorem Data.diskEuler {n : ℕ} {label : Fin n → A} (d : Data inv label) : DiskEuler d := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.WordPairing.Data, OAI.TorsionFreeZeroDivisors.WordPairing.DiskEuler

  519. lemma OAI.TorsionFreeZeroDivisors.MapEuler.component_sameCycle line 4095
  520. lemma OAI.TorsionFreeZeroDivisors.WordPairing.rotate_sameCycle line 4106
  521. theorem OAI.TorsionFreeZeroDivisors.WordPairing.Data.genusZero line 4113

    Source documentation

    The noncrossing cancellation matching has actual combinatorial genus zero, not just a scalar disk face estimate. Nonempty words (necessarily of length at least two) have a single map component; the empty case is separate.

    theorem Data.genusZero : GenusZero (finRotate n) d.partner := by
…
  522. lemma OAI.TorsionFreeZeroDivisors.DeleteCycle.bypass_fixed line 4154
  523. def OAI.TorsionFreeZeroDivisors.IsolatedDeletion.classify line 4164
  524. lemma OAI.TorsionFreeZeroDivisors.IsolatedDeletion.classify_rotation line 4166
  525. lemma OAI.TorsionFreeZeroDivisors.IsolatedDeletion.classify_partner line 4171
  526. def OAI.TorsionFreeZeroDivisors.IsolatedDeletion.project line 4176
  527. def OAI.TorsionFreeZeroDivisors.IsolatedDeletion.inclusion line 4178
  528. lemma OAI.TorsionFreeZeroDivisors.IsolatedDeletion.project_injective line 4181
  529. lemma OAI.TorsionFreeZeroDivisors.IsolatedDeletion.project_surjective line 4196
  530. def OAI.TorsionFreeZeroDivisors.IsolatedDeletion.componentEquiv line 4205
  531. lemma OAI.TorsionFreeZeroDivisors.IsolatedDeletion.component_count line 4208
  532. theorem OAI.TorsionFreeZeroDivisors.IsolatedDeletion.genusZero line 4213

    Source documentation

    Deleting an isolated unpaired occurrence removes one vertex, one face and one actual connected component; genus zero is preserved also in the empty case.

    theorem genusZero (hz : GenusZero σ α) :
    GenusZero (bypass σ p) (restrict α p ha) := by
…
  533. theorem OAI.TorsionFreeZeroDivisors.MapDeletion.genusZero_delete_all line 4247

    Source documentation

    Unconditional deletion of an unpaired occurrence, including isolated vertices/components.

    theorem genusZero_delete_all (hz : GenusZero σ α) : GenusZero (bypass σ p) (restrict α p ha) := by
…
  534. theorem OAI.TorsionFreeZeroDivisors.BandEuler.genusZero_all line 4263

    Source documentation

    Paired-band deletion preserves genus zero without any degree or face nondegeneracy assumptions. Empty residual maps, isolated disks, monogons, digons, and split components are all included. This is purely a permutation-map result, not an assertion that an essential sphere survives the surgery.

    theorem genusZero_all (hz : GenusZero σ α) :
    GenusZero (rotation σ p q hpq) (partner α hi p q hpq hpair) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BandEuler.rotation, OAI.TorsionFreeZeroDivisors.BandEuler.partner

  535. theorem OAI.TorsionFreeZeroDivisors.MapEuler.euler_of_genusZero line 4279

    Source documentation

    Exact Euler lower bound used by the source interval estimate, extracted from actual combinatorial genus zero. No connectivity is assumed: one actual occurrence suffices to make the component count positive.

    theorem euler_of_genusZero [Nonempty O] (hz : GenusZero σ α) (hf : ∀x,α x≠x) :
    Fintype.card O+4≤2*Fintype.card (Cycle σ)+2*Fintype.card (Cycle (α*σ)) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero

  536. def OAI.TorsionFreeZeroDivisors.BoundarySurgery.Consistent line 4297

    Source documentation

    Consecutive edge endpoint agreement. A marked exterior break can be encoded by one extra formal item with distinct prescribed before/after endpoints.

    def Consistent : Prop := ∀ x,after x=before (σ x)
…
  537. lemma OAI.TorsionFreeZeroDivisors.BoundarySurgery.bypass_consistent line 4299
  538. def OAI.TorsionFreeZeroDivisors.BoundarySurgery.swappedBefore line 4306
  539. lemma OAI.TorsionFreeZeroDivisors.BoundarySurgery.switched_consistent line 4308
  540. theorem OAI.TorsionFreeZeroDivisors.BoundarySurgery.consistent line 4318

    Source documentation

    The literal band-spliced boundary preserves the graph endpoint equations. The two crossed endpoints are exactly those forced by an edge and its reverse. No statement about homotopy or essentiality is hidden in this combinatorial lemma, and neither distinct-boundary nor same-boundary cases are excluded.

    theorem consistent (h : Consistent σ before after)
    (hp : after p=before q) (hq : after q=before p) :
    Consistent (rotation σ p q hpq) (fun x=>before (val p q hpq x))
      (fun x=>after (val p q hpq x)) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BoundarySurgery.Consistent

  541. lemma OAI.TorsionFreeZeroDivisors.BoundarySurgery.marker_nonfixed line 4336

    Source documentation

    A surviving exterior marker keeps its prescribed distinct endpoints, so its new boundary contains at least one actual edge after the deletion.

    lemma marker_nonfixed (h : Consistent σ before after)
    (hp : after p=before q) (hq : after q=before p)
    (m : Residual p q hpq) (hm : after (val p q hpq m)≠before (val p q hpq m)) :
    rotation σ p q hpq m≠m := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BoundarySurgery.Consistent

  542. lemma OAI.TorsionFreeZeroDivisors.VertexSplit.forest_partner line 4357
  543. lemma OAI.TorsionFreeZeroDivisors.VertexSplit.forest_join line 4362
  544. lemma OAI.TorsionFreeZeroDivisors.VertexSplit.forest_rotation line 4368
  545. lemma OAI.TorsionFreeZeroDivisors.VertexSplit.original_invariant line 4374
  546. def OAI.TorsionFreeZeroDivisors.VertexSplit.toOriginal line 4390
  547. def OAI.TorsionFreeZeroDivisors.VertexSplit.toForest line 4392
  548. def OAI.TorsionFreeZeroDivisors.VertexSplit.componentEquiv line 4394
  549. lemma OAI.TorsionFreeZeroDivisors.VertexSplit.face_eq line 4403
  550. theorem OAI.TorsionFreeZeroDivisors.MapEuler.genusZero_vertexSplit line 4418

    Source documentation

    Splitting a vertex along two gaps preserves combinatorial genus zero. This permits empty/isolated components and needs no topological embedding assumption. The two gaps must be on the same actual vertex cycle.

    theorem genusZero_vertexSplit (hz : GenusZero σ α) (p q : O) (hpq : p≠q)
    (hc : cycle σ p=cycle σ q) : GenusZero (Equiv.swap p q*σ) α := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero

  551. def OAI.TorsionFreeZeroDivisors.MapConjugation.forward line 4454
  552. def OAI.TorsionFreeZeroDivisors.MapConjugation.backward line 4458
  553. def OAI.TorsionFreeZeroDivisors.MapConjugation.components line 4462
  554. def OAI.TorsionFreeZeroDivisors.MapConjugation.supports line 4474
  555. lemma OAI.TorsionFreeZeroDivisors.MapConjugation.support_count line 4489
  556. theorem OAI.TorsionFreeZeroDivisors.MapConjugation.genusZero line 4492

    Source documentation

    Changing the actual finite occurrence coordinates does not change genus.

    theorem genusZero (h : GenusZero σ α) : GenusZero σ' α' := by
…
  557. abbrev OAI.TorsionFreeZeroDivisors.MatchingSurgery.Remaining line 4513
  558. def OAI.TorsionFreeZeroDivisors.MatchingSurgery.splice line 4514
  559. lemma OAI.TorsionFreeZeroDivisors.MatchingSurgery.splice_avoids line 4517
  560. def OAI.TorsionFreeZeroDivisors.MatchingSurgery.apply line 4537
  561. lemma OAI.TorsionFreeZeroDivisors.MatchingSurgery.involutive line 4540
  562. lemma OAI.TorsionFreeZeroDivisors.MatchingSurgery.distinct line 4558
  563. def OAI.TorsionFreeZeroDivisors.MatchingSurgery.partner line 4572
  564. lemma OAI.TorsionFreeZeroDivisors.MatchingSurgery.compatible line 4577
  565. lemma OAI.TorsionFreeZeroDivisors.Smoothing.rotation_invariant line 4597
  566. def OAI.TorsionFreeZeroDivisors.Smoothing.rotation line 4603
  567. abbrev OAI.TorsionFreeZeroDivisors.Smoothing.r line 4606
  568. lemma OAI.TorsionFreeZeroDivisors.Smoothing.pr line 4608
  569. lemma OAI.TorsionFreeZeroDivisors.Smoothing.rename_invariant line 4610
  570. def OAI.TorsionFreeZeroDivisors.Smoothing.flatten line 4620
  571. def OAI.TorsionFreeZeroDivisors.Smoothing.rename line 4626
  572. def OAI.TorsionFreeZeroDivisors.Smoothing.coordinates line 4628
  573. lemma OAI.TorsionFreeZeroDivisors.Smoothing.coordinates_val line 4630
  574. lemma OAI.TorsionFreeZeroDivisors.Smoothing.partner_commutes line 4633
  575. lemma OAI.TorsionFreeZeroDivisors.Smoothing.bypass_value line 4656
  576. lemma OAI.TorsionFreeZeroDivisors.Smoothing.rotation_value line 4662
  577. lemma OAI.TorsionFreeZeroDivisors.Smoothing.smoothing_value line 4684
  578. lemma OAI.TorsionFreeZeroDivisors.Smoothing.rotation_commutes line 4730
  579. theorem OAI.TorsionFreeZeroDivisors.Smoothing.genusZero line 4742

    Source documentation

    Suppressing an actual two-occurrence boundary splices its matching partners, including the already-paired case, and preserves combinatorial genus zero.

    theorem genusZero (hz : MapEuler.GenusZero σ α) :
    MapEuler.GenusZero (rotation σ p q hsp hsq)
      (MatchingSurgery.partner α hi hf p q hpq) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.Smoothing.rotation, OAI.TorsionFreeZeroDivisors.MatchingSurgery.partner

  580. def OAI.TorsionFreeZeroDivisors.Tightening.isolate line 4770
  581. lemma OAI.TorsionFreeZeroDivisors.Tightening.q_ne_next line 4772
  582. lemma OAI.TorsionFreeZeroDivisors.Tightening.isolate_p line 4774
  583. lemma OAI.TorsionFreeZeroDivisors.Tightening.isolate_q line 4777
  584. def OAI.TorsionFreeZeroDivisors.Tightening.rotation line 4778
  585. lemma OAI.TorsionFreeZeroDivisors.Tightening.isolate_genusZero line 4783
  586. theorem OAI.TorsionFreeZeroDivisors.Tightening.genusZero line 4792

    Source documentation

    Deleting an actual adjacent backtracking pair from its boundary, with the forced partner splice, preserves genus zero even if the two occurrences were not paired. This supplies the finite-map part of cyclic tightening.

    theorem genusZero (hz : MapEuler.GenusZero σ α) :
    MapEuler.GenusZero (rotation σ p q hpq hsp) (MatchingSurgery.partner α hi hf p q hpq) :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.Tightening.rotation, OAI.TorsionFreeZeroDivisors.MatchingSurgery.partner

  587. theorem OAI.TorsionFreeZeroDivisors.Tightening.consistent line 4802

    Source documentation

    The graph endpoint conditions, not just the rose labels, survive the backtracking deletion. The second occurrence really returns to the first occurrence's starting vertex.

    theorem consistent (h : BoundarySurgery.Consistent σ before after) (hq : after q=before p) :
    BoundarySurgery.Consistent (rotation σ p q hpq hsp)
      (fun x=>before x) (fun x=>after x) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.BoundarySurgery.Consistent, OAI.TorsionFreeZeroDivisors.Tightening.rotation

  588. lemma OAI.TorsionFreeZeroDivisors.Tightening.marker_nonfixed line 4811
  589. abbrev OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.Remaining line 4830
  590. def OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.splice line 4831
  591. lemma OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.splice_avoids line 4834
  592. def OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.apply line 4854
  593. lemma OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.involutive line 4857
  594. lemma OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.distinct line 4875
  595. def OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.partner line 4889
  596. lemma OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.compatible line 4894
  597. lemma OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.fixed line 4905
  598. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.rotation_invariant line 4919
  599. def OAI.TorsionFreeZeroDivisors.PartialSmoothing.rotation line 4925
  600. abbrev OAI.TorsionFreeZeroDivisors.PartialSmoothing.r line 4928
  601. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.pr line 4930
  602. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.rename_invariant line 4932
  603. def OAI.TorsionFreeZeroDivisors.PartialSmoothing.flatten line 4942
  604. def OAI.TorsionFreeZeroDivisors.PartialSmoothing.rename line 4948
  605. def OAI.TorsionFreeZeroDivisors.PartialSmoothing.coordinates line 4950
  606. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.coordinates_val line 4952
  607. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.partner_commutes line 4955
  608. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.bypass_value line 4978
  609. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.rotation_value line 4984
  610. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.smoothing_value line 5006
  611. lemma OAI.TorsionFreeZeroDivisors.PartialSmoothing.rotation_commutes line 5052
  612. theorem OAI.TorsionFreeZeroDivisors.PartialSmoothing.genusZero line 5064

    Source documentation

    Suppressing an actual two-occurrence boundary splices its matching partners, including the already-paired case, and preserves combinatorial genus zero.

    theorem genusZero (hz : MapEuler.GenusZero σ α) :
    MapEuler.GenusZero (rotation σ p q hsp hsq)
      (PartialMatchingSurgery.partner α hi p q hpq hfp hfq) := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.PartialSmoothing.rotation, OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.partner

  613. theorem OAI.TorsionFreeZeroDivisors.Tightening.partial_genusZero line 5094

    Source documentation

    The tightening operation also allows unrelated unpaired markers. Only the actual two deleted letter occurrences are required to be nonfixed.

    theorem partial_genusZero (hz : MapEuler.GenusZero σ α) :
    MapEuler.GenusZero (rotation σ p q hpq hsp)
      (PartialMatchingSurgery.partner α hi p q hpq hfp hfq) :=
…

    Mentions: OAI.TorsionFreeZeroDivisors.MapEuler.GenusZero, OAI.TorsionFreeZeroDivisors.Tightening.rotation, OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.partner

  614. structure OAI.TorsionFreeZeroDivisors.FinitePicture.Data line 5107

    Source documentation

    A purely finite lifted boundary certificate. The single unpaired marker records the break from the exterior endpoint y back to the prescribed root x. No surface map, cone filling, essentiality, or CW realization is asserted.

    structure Data where
…
  615. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.nonfixed line 5127
  616. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.partner_ne_marker line 5128
  617. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.swap_endpoints line 5130
  618. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.marker_not_fixed_rotation line 5140
  619. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.reindex line 5147
  620. abbrev OAI.TorsionFreeZeroDivisors.FinitePicture.Data.bandMarker line 5178
  621. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.band line 5179
  622. abbrev OAI.TorsionFreeZeroDivisors.FinitePicture.Data.tightMarker line 5211
  623. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.option_inverse line 5212
  624. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.option_compatible line 5217
  625. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.option_backtrack line 5221
  626. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.tighten line 5229

    Source documentation

    The actual adjacent reverse-edge deletion with the forced partner splice. In contrast to the paired band move, p and q need not be partners.

    def tighten (hinv : Function.Involutive inv)
    (hlabel : ∀d,label (Γ.reverse d)=inv (label d))
    (hsp : a.rotation p=q) (he : a.dart q=(a.dart p).map Γ.reverse) :
    Data (O:=PartialMatchingSurgery.Remaining p q) Γ label inv x y where
…

    Mentions: OAI.TorsionFreeZeroDivisors.FinitePicture.Data, OAI.TorsionFreeZeroDivisors.PartialMatchingSurgery.Remaining

  627. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.unequal_backtrack line 5265
  628. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.Reduced line 5274

    Source documentation

    Both kinds of shortening forbidden in a least marked finite certificate.

    def Reduced : Prop :=
…
  629. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.deletionCoordinates line 5277
  630. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.remaining_two_fewer line 5283
  631. theorem OAI.TorsionFreeZeroDivisors.FinitePicture.Data.reduced_of_minimum line 5286
  632. theorem OAI.TorsionFreeZeroDivisors.FinitePicture.Data.exists_reduced line 5312

    Source documentation

    From an actual finite marked certificate obtain one with the same distinct endpoints and with no same-lift paired band or adjacent backtracking. This is a finite combinatorial reduction, not existence of a certificate for a null word.

    theorem exists_reduced (hinv : Function.Involutive inv)
    (hlabel : ∀d,label (Γ.reverse d)=inv (label d)) :
    ∃n,n≤Fintype.card O ∧ ∃b : Data (O:=Fin n) Γ label inv x y,b.Reduced := by
…

    Mentions: OAI.TorsionFreeZeroDivisors.FinitePicture.Data

  633. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.excess_identity line 5330
  634. lemma OAI.TorsionFreeZeroDivisors.PermutationCycles.twice_cycles_le line 5341
  635. abbrev OAI.TorsionFreeZeroDivisors.FinitePicture.Data.Occ line 5353
  636. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.closedRotation line 5354
  637. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.fullPartner line 5355
  638. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.fullPartner_val line 5356
  639. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.fullPartner_involutive line 5357
  640. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.fullPartner_nonfixed line 5361
  641. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.dart_isSome line 5364
  642. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge line 5367
  643. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.some_edge line 5368
  644. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_begins line 5369
  645. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_ends line 5370
  646. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_compatible line 5371
  647. def OAI.TorsionFreeZeroDivisors.FinitePicture.Data.first line 5377
  648. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.first_start line 5378
  649. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.closedRotation_at_first line 5381
  650. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.closedRotation_val line 5392
  651. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_consistent line 5399

    Source documentation

    All joins other than the unique root break are actual graph joins.

    lemma edge_consistent (i : a.Occ) (hi : a.closedRotation i≠a.first hxy) :
    Γ.origin (Γ.reverse (a.edge i))=Γ.origin (a.edge (a.closedRotation i)) := by
…
  652. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.last_end line 5403
  653. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.closedRotation_genusZero line 5407
  654. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.closedRotation_euler line 5413

    Source documentation

    The unmarked pairing is nonempty and has the literal sphere Euler bound. This proves the scalar input needed by interval cutting, not a PL realization.

    lemma closedRotation_euler : Fintype.card a.Occ+4≤2*Fintype.card (Cycle a.closedRotation)+
    2*Fintype.card (Cycle (a.fullPartner*a.closedRotation)) := by
…
  655. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_partner_not_reverse line 5419
  656. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_partner_not_same line 5424
  657. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_reduced line 5431
  658. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.edge_no_backtrack line 5440
  659. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.face_fixed_break line 5449
  660. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.face_monogons_le line 5462
  661. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.at_least_two_boundaries line 5475

    Source documentation

    A reduced distinct-endpoint certificate necessarily contains an ordinary boundary, not just the exceptional root cycle. This includes singleton cycles.

    lemma at_least_two_boundaries : 2≤Fintype.card (Cycle a.closedRotation) := by
…
  662. lemma OAI.TorsionFreeZeroDivisors.FinitePicture.Data.ordinary_boundary line 5481