OAI/AlgebraicGeometry/CharacterVarieties/Cutting/PortSurgery.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.toWiring line 18

   Source documentation

   The old assembly's actual whole-port wiring, not an abstract end matching.

   def toWiring : PortWiring A.kind where
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring

2. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.toWiring_endOf line 26
3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.wiringSides line 39
4. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.wiringSides_number line 42
5. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.realize_number line 47
6. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.toWiring_sideOf line 54
7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.boundaryNext_local line 61
8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.toWiring_boundary line 71
9. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum line 88

   Source documentation

   Disjoint whole-port union, before the three-port inverse-band surgery.

   def sum : PortWiring (sumKind k l) where
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.sumKind

10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_wire_left line 101
11. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_wire_right line 106
12. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sumSides line 113

    Source documentation

    This equivalence retains each individual ordered child occurrence.

    def sumSides : Side W.Seam W.seamArity ⊕ Side Z.Seam Z.seamArity ≃
        Side (W.sum Z).Seam (W.sum Z).seamArity where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.Seam, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.seamArity

13. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.leftEnd line 124
14. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.rightEnd line 125
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_endOf_left line 127
16. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_endOf_right line 142
17. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sumSides_number_left line 157
18. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sumSides_number_right line 161
19. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_sideOf_left line 166
20. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_sideOf_right line 175
21. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_boundary_left line 184
22. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sum_boundary_right line 193
23. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.rewire line 211

    Source documentation

    Rewire WHOLE ports of the same ordered arity, never individual children.

    def rewire (C : Equiv.Perm W.Seam) (hC : ∀ s,W.seamArity (C s)=W.seamArity s) : PortWiring kind where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring

24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.inverse_arity line 215
25. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.mapSides line 222
26. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.mapSides_number line 226
27. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.mapSides_isNone line 230
28. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.rewire_sideOf line 237

    Source documentation

    Negative endpoints are the only local ends whose side number changes under the whole-port rewiring. The ordered child NUMBER remains identical.

    lemma rewire_sideOf (C : Equiv.Perm W.Seam) (hC) (x : LocalEnd V kind) :
        (W.rewire C hC).sideOf x =
          if (kind x.1).table.endpoint x.2.1 then W.sideOf x
          else W.mapSides C.symm (W.inverse_arity C hC) (W.sideOf x) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf

29. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideEntries line 265

    Source documentation

    Separate parents from their individual ordered child occurrences.

    def sideEntries : Side W.Seam W.seamArity ≃ W.Seam ⊕ ((s : W.Seam) × Fin (W.seamArity s)) where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side

30. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.entryAction line 275
31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.entryAction_none line 280
32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.entryAction_some line 282
33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.positiveRelabel line 285
34. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.cutAction line 287
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.positiveRelabel_sideOf line 290
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.negativeRelabel_sideOf line 298
37. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.rewire_boundary line 317

    Source documentation

    The literal boundary permutation after rewiring: inverse action on parent occurrences, forward action on EACH ordered child occurrence. This identity is independent of colors, ranks, or any supposed ribbon template.

    theorem rewire_boundary (C : Equiv.Perm W.Seam) (hC) (a : Side W.Seam W.seamArity) :
        ((W.rewire C hC).assemble (fun _ => ()) (fun _ => rfl)).vertexAssembly.corners.boundaryNext
          (W.positiveRelabel C hC a) =
        W.positiveRelabel C hC (W.cutAction C hC
          ((W.assemble (fun _ => ()) (fun _ => rfl)).vertexAssembly.corners.boundaryNext a)) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.assemble

38. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.ext_wire line 334
39. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graft_close_arity line 348
40. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftBase line 353
41. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftBase_wire line 356
42. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm line 371
43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm_apply line 374
44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm_wire line 378
45. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm_arity line 387
46. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftWiring_eq_rewire line 396

    Source documentation

    The actual inverse-band assembly, not a guessed cyclic template, is the three-port surgery of the disjoint old assembly and its closed doubled band.

    theorem graftWiring_eq_rewire :
        graftWiring A P d q hi hp hm=
          (graftBase A P d q hp hm).rewire (graftPerm A P q)
            (graftPerm_arity A P d q hi hp hm) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftWiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftBase, OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm, OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPerm_arity

47. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.splice_pow_lt line 417
48. lemma OAI.IntegralCharacterVarieties.BoundarySurgery.splice_pow_card line 436
49. theorem OAI.IntegralCharacterVarieties.BoundarySurgery.splice_isCycle line 448

    Source documentation

    Splicing two distinct actual boundary circuits at designated entries joins them to ONE circuit and retains every side, including singleton loops.

    theorem splice_isCycle : (Equiv.swap x y*N).IsCycleOn ((s∪t : Finset α) : Set α) := by
    …

50. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.StripRoot line 482
51. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.ShortChild line 483
52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.inputStrip_injective line 486
53. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputStrip_injective line 489
54. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputRoot_injective line 493
55. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.shortRoot line 502
56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.shortRoot_injective line 509

    Source documentation

    Distinct incidence occurrences contact distinct doubled strips. In particular a row and a column may carry the same old facet but they CANNOT be identified before the actual gluing.

    lemma shortRoot_injective (h : List.Disjoint a b) : Function.Injective B.shortRoot := by
    …

57. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.contactEmbedding line 522
58. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.FreshStrip line 526

    Source documentation

    These, and not cell-rank values, label the newly created disk facets.

    abbrev FreshStrip := {r : B.StripRoot // r∉Set.range B.shortRoot}

59. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripDecomposition line 528
60. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.root_root line 533
61. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_mem_orig line 536
62. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_mem_mirror line 538
63. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.inputContact_cycle line 543

    Source documentation

    An actual short-end child occurs on a certified strip circuit, not just in an endpoint list.

    lemma inputContact_cycle (c) : B.mirrorStripSide (B.inputStrip c)∈
        B.stripCycle (B.shortRoot (.inl c)).val := by
    …

64. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.outputContact_cycle line 546
65. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.contact_cycles_disjoint line 549
66. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.fresh_contact_disjoint line 553