OAI/AlgebraicGeometry/CharacterVarieties/Cutting/GraftCircuits.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

The principal and secondary boundary circuits of an inverse-band graft.

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

  1. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base line 18
  2. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding line 19
  3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding line 24
  4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base_old_next line 31
  5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base_band_next line 36
  6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base_old_cycle line 41
  7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base_band_cycle line 45
  8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_band_ne line 50
  9. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_band_disjoint line 55
  10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base_eq line 64
  11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.graft_arity line 68
  12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring_eq_base_rewire line 75
  13. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_base line 82
  14. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripFinset line 98
  15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mem_stripFinset line 101
  16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.coe_stripFinset line 103
  17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripFinset_cycle line 106
  18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripFinset_disjoint line 110
  19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.shortFinsets_disjoint line 116
  20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.inputContact_number line 124
  21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputContact_number line 137
  22. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.cutPort line 159
  23. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortPort line 160
  24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.cutPort_arity line 161
  25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.input_arity line 162
  26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.output_arity line 165
  27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortPort_arity line 168
  28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.cutPort_ne_short line 174
  29. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortChildAt line 178
  30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortChildAt_injective line 184
  31. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortCycle line 191
  32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortCycle_cycle line 193
  33. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortCycles_disjoint line 195
  34. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.tripleNew_mem_shortCycle line 205
  35. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.contacts line 243
  36. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldContact line 244
  37. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.newContact line 245
  38. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.childNext line 247
  39. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.secondaryCircle line 249
  40. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldContact_eq line 251
  41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.childNext_eq_family line 258
  42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldContact_not_shortCycle line 276
  43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldCircle_short_disjoint line 281
  44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.actual_child_circle line 284
  45. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircleOn_all line 314
  46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding_parent line 334
  47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding_input_parent line 340
  48. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding_output_parent line 349
  49. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.graftPerm_away line 359
  50. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.parentSurgery_away line 365
  51. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_parentSurgery_away line 382
  52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.strip_parentSurgery_away line 391
  53. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.secondary_parentSurgery_away line 412
  54. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircleOn_subset line 426
  55. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.actual_secondary_circle line 445

    Source documentation

    Full ACTUAL three-port rewiring, not merely its child-side cyclic template: every old circle away from the cut parent remains one cycle, and its based noncommutative word is unchanged after inserting both strips at every contact.

    theorem actual_secondary_circle {G : Type*} [Group G]
    (s : Finset (Side S arity))
    (hs : A.vertexAssembly.corners.boundaryNext.IsCycleOn (s : Set (Side S arity)))
    (hq : (⟨q,none⟩ : Side S arity)∉s)
    (hinj : Function.Injective B.shortRoot)
    (u : Side (base A q B).Seam (base A q B).seamArity → G)
    (hu : ∀ j,∀ a∈shortCycle A q B j,u a=1) :
    (next A q B).IsCycleOn (secondaryCircle A q B s : Set (Side (base A q B).Seam (base A q B).seamArity)) ∧
    ∀ a∈s,cycleWord (next A q B) u (oldEmbedding A q B a) (secondaryCircle A q B s).card=
      cycleWord A.vertexAssembly.corners.boundaryNext (u ∘ oldEmbedding A q B) a s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortCycle, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.secondaryCircle, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding

  56. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.preSpliceFamily_at_away line 470
  57. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.anyStrip_parentSurgery_away line 487
  58. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.freshStrip_newContact_ne line 508
  59. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_freshStrip line 523
  60. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.freshStrip_actual_circle line 545

    Source documentation

    Each untouched connected strip is STILL its literal single boundary circle after all three-port sewings. No phantom fresh facet or additional boundary component is inferred merely from ranks.

    theorem freshStrip_actual_circle (r : B.FreshStrip) :
    (next A q B).IsCycleOn
      ((B.stripFinset r.val.val).map (bandEmbedding A q B) : Set (Side (base A q B).Seam (base A q B).seamArity)) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding, OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base

  61. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.attachedCircleOn_contact_subset line 559
  62. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortChildAt_surjective line 578
  63. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mem_contacts line 589
  64. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.literal_germ_exhaustion line 595

    Source documentation

    Exhaustion is on literal sides of the actual graft wiring. In particular, an untouched strip is assigned its connected root, not a colour-label guess.

    theorem literal_germ_exhaustion (a : Side (base A q B).Seam (base A q B).seamArity) :
    (∃ x : Side S arity,a=oldEmbedding A q B x) ∨
    (∃ v,a=bandEmbedding A q B (B.origPrincipal v)) ∨
    (∃ v,a=bandEmbedding A q B (B.mirrorPrincipal v)) ∨
    (∃ j,a∈shortCycle A q B j) ∨
    (∃ r : B.FreshStrip,a∈(B.stripFinset r.val.val).map (bandEmbedding A q B)) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.base, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldEmbedding, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.bandEmbedding, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortCycle

  65. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.shortCycle_in_secondary line 625
  66. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.pow_cycleEntry line 639
  67. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.isCycleOn_range line 647
  68. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorEntry line 665

    Source documentation

    Actual positive traversal of the new principal circle of the graft.

    noncomputable def mirrorEntry (i : Fin (B.length+1)) := mirrorSide A q B i.rev

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorSide

  69. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorEntry_next line 667
  70. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorEntry_injective line 676
  71. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirror_isCycle line 684

    Source documentation

    The literal mirror sides form exactly one boundary orbit. No independent cyclic template, no parent germ exhaustion assumption.

    lemma mirror_isCycle : (next A q B).IsCycleOn (Set.range (mirrorEntry A q B)) :=
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorEntry

  72. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_pow_old line 699
  73. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_pow_old_card line 712
  74. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_pow_new line 723
  75. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_pow_full line 731
  76. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_isCycle line 739

    Source documentation

    Full circuit exhaustion for the inserted chain, not just a rank or Euler characteristic count.

    lemma chain_isCycle : Z.IsCycleOn (f '' (s : Set α) ∪ Set.range c) := by
…
  77. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_word_old line 784
  78. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_word_new line 794
  79. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_cycleWord line 808

    Source documentation

    Exact NONCOMMUTATIVE monodromy for inserting a new literal band side into an old boundary circuit. Old coefficients and starting occurrence are retained.

    lemma chain_cycleWord (u : β → G) :
    cycleWord Z u (f q) (s.card+(k+1))=
      (List.ofFn (fun i => u (c i))).reverse.prod*cycleWord N (u ∘ f) q s.card := by
…

    Mentions: OAI.IntegralCharacterVarieties.BoundarySurgery.cycleWord

  80. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.chain_cycleWord_identity line 815
  81. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldPrincipal_parent line 834
  82. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_oldPrincipal line 851
  83. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.principalChain_isCycle line 874

    Source documentation

    The selected actual old circuit acquires precisely the original band side; all its old occurrences remain separate. The mirror circle is a different literal orbit, proved separately by mirror_isCycle.

    lemma principalChain_isCycle : (next A q B).IsCycleOn
    ((fun a : Side S arity => oldSide A q B a.1) '' (s : Set (Side S arity)) ∪
      Set.range (originalSide A q B)) := by
…

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next, OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldSide, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalSide

  84. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.principalChain_word line 889