OAI/AlgebraicGeometry/CharacterVarieties/Cutting/RefinedDiagram.lean

GitHub source file

67 declarations, 0 contain sorry, 0 declared as axioms

Boundary orbits of the refined inverse-band diagram.

This formalizes the band reconstruction for filtered surface local systems in Integral points on character varieties of curves.

  1. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedAtomicGraft_seamRank line 23
  2. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedGenus line 32
  3. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutDiagram line 40

    Source documentation

    Literal inverse-band occurrence diagram with a distinct lower-rank disk for each uncontacted strip. ALL circles are taken from the actual boundary successor; none is supplied as a cyclic-template coverage assumption. The full solution lift is a separate obligation and is not asserted by this constructor.

    noncomputable def refinedCutDiagram [Finite V] :=
…
  4. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutDiagram_rank_inl line 45
  5. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutDiagram_genus_selected line 47
  6. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutDiagram_genus_lt line 51
  7. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutDiagram_fresh_rank_lt line 57
  8. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.refinedCutPunctures line 64
  9. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.PortFrames line 81
  10. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.localFrameUnit line 84
  11. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues line 88
  12. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.frameValues_attach line 94
  13. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.SideValues line 104
  14. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.HandleValues line 106
  15. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.valuesFromPorts line 109
  16. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.portFrame_valuesFromPorts line 116
  17. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.vertexHolds_valuesFromPorts line 124
  18. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEntry line 141
  19. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEntry_injective line 144
  20. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEntry_next line 150
  21. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEntry_pow_lt line 160
  22. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySet line 172
  23. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySet_coe line 175
  24. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySet_card line 180
  25. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySet_isCycle line 184
  26. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCoefficient line 202
  27. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCoefficient_boundary line 206
  28. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.eval_subst_rank line 213
  29. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord_cycleWord line 220
  30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding_any_parent line 248
  31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding_origPrincipal line 254
  32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding_mirrorPrincipal line 266
  33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.principalCircle line 280
  34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.principalCircle_coe line 284
  35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.principalCircle_isCycle line 309
  36. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle line 322
  37. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySet_exhaustive line 327
  38. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.old_mem_graftCircle line 332
  39. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle_isCycle line 341
  40. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_circle_exhaustion line 357

    Source documentation

    Every side of the actual reconstructed diagram belongs to an explicitly identified actual circle: one from an old boundary, the extra principal circle, or a single untouched connected strip. This is an exhaustive geometric sewing statement, not rank conservation or a template enumeration.

    theorem actual_circle_exhaustion
    (hno : ∀ z i,D.ports.facet ⟨z,some i⟩≠D.ports.facet ⟨q,none⟩)
    (a : Side (base D.ports q B).Seam (base D.ports q B).seamArity) :
    (∃ f b,a∈D.oldGraftCircle q B f b) ∨
    (∃ i,a=mirrorEntry D.ports q B i) ∨
    (∃ r : B.FreshStrip,a∈(B.stripFinset r.val.val).map (bandEmbedding D.ports q B)) := by
…
  41. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.mem_attachedCircleOn_iff line 390
  42. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.disjoint_cycles_of_mem_not_mem line 402
  43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_not_shortCycle line 422
  44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_secondaryCircle_iff line 426
  45. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_principalCircle_iff line 430
  46. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorCircle line 440
  47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorCircle_isCycle line 442
  48. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_not_mirrorCircle line 456
  49. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_not_stripCircle line 462
  50. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.old_mem_graftCircle_iff line 473
  51. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundarySet_unique line 480
  52. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle_nonempty line 487
  53. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle_disjoint line 492
  54. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.freshCircle line 511
  55. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.freshCircle_nonempty line 513
  56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorCircle_nonempty line 518
  57. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirror_not_freshCircle line 521
  58. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirror_fresh_disjoint line 532
  59. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.freshCircle_disjoint line 538
  60. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle_mirror_disjoint line 554
  61. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.oldGraftCircle_fresh_disjoint line 564
  62. abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.GraftCircleLabel line 574
  63. def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircle line 575
  64. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircle_nonempty line 580
  65. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircle_isCycle line 585
  66. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircle_disjoint line 594
  67. lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.graftCircle_cover line 609