OAI/AlgebraicGeometry/CharacterVarieties/Cutting/Grafting.lean

GitHub source file

140 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror line 17

   Source documentation

   The orientation reverse is again one of the literal allowed vertices.

   def Kind.mirror : Kind → Kind
     | .passage m t => .passage m t
     | .splitting a b c r => .splitting a b c (!r)

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.passage

2. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_mirror line 21
3. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirrorPort line 26
4. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirrorChild line 31
5. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirrorEnd line 37
6. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_endpoint line 42
7. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Passage.permutation_symm line 48
8. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_mate line 55

   Source documentation

   Reversal preserves every paired child occurrence, including repetitions.

   lemma Kind.mirror_mate (k : Kind) (x : (p : k.table.Port) × Option (k.table.Child p)) :
       k.mirrorEnd (k.table.mate x) = k.mirror.table.mate (k.mirrorEnd x) := by
   …

   Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind

9. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_arity line 70
10. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_childEnumeration line 76
11. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.mirror line 84

    Source documentation

    The mirror uses the same color on the same literal occurrence.

    def Decoration.mirror {F : Type} {k : Kind} (d : Decoration k F) : Decoration k.mirror F where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration

12. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.mirror_color line 92
13. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.mirrorKind line 104
14. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.mirrorPortAt line 106
15. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.mirrorPortAt_arity line 120
16. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.sumKind line 126
17. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.sumPortAt line 129

    Source documentation

    A disjoint union of vertex sets retains every whole ordered port.

    def sumPortAt (b : Bool) : PortAt kind b ⊕ PortAt other b ≃ PortAt (sumKind kind other) b where
    …

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

18. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.mirror line 143

    Source documentation

    Mirror all internal sewing, without losing any transverse branch port.

    def mirror : PortPatch (mirrorKind kind) I B A where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch, OAI.IntegralCharacterVarieties.OccurrenceIncidence.mirrorKind

19. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.markInterface line 156

    Source documentation

    Split off ONE genuine short-end from an exhaustive interface; all other ports remain explicitly enumerated, never silently thrown away.

    noncomputable def markInterface {T : Type} (t : T) : Unit ⊕ {u : T // u ≠ t} ≃ T where
    …

20. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.DoubleInternal line 168

    Source documentation

    Index bookkeeping for the literal doubled patch. The first two summands are the two longitudinal sewings; the last two are ALL transverse branches.

    abbrev DoubleInternal (I A B : Type) := (I ⊕ I) ⊕ (A ⊕ B)

21. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.doublePlusIndex line 170
22. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.doubleMinusIndex line 189
23. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double line 211

    Source documentation

    Double an open band and sew every non-short-end interface across the two copies. Exactly four short ends remain. This is an exhaustive whole-port construction, not merely a list of proposed endpoints.

    noncomputable def double (a₀ : A) (b₀ : B) :
        PortPatch (sumKind kind (mirrorKind kind))
          (DoubleInternal I {a : A // a ≠ a₀} {b : B // b ≠ b₀}) Bool Bool := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch, OAI.IntegralCharacterVarieties.OccurrenceIncidence.sumKind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.mirrorKind, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.DoubleInternal

24. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_plus_short line 237
25. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_minus_short line 243
26. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.doubledWiring line 251

    Source documentation

    Identifying matching short ends supplies an honest closed occurrence assembly; the external matching is itself equal-arity, as required.

    noncomputable def doubledWiring (a₀ : A) (b₀ : B) : PortWiring (sumKind kind (mirrorKind kind)) :=
    …

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

27. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.ColorMatch line 269

    Source documentation

    Literal ordered color matching for a whole seam. Repeated names retain separate coordinates; child reindexing is forced by the seam's arity equality.

    def PortWiring.ColorMatch : Prop := ∀ (p : W.Seam) (i : Option (Fin (W.seamArity p))),
    …

28. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.seamColor line 274
29. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.portColor_some_congr line 277
30. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.val_transport line 286
31. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.seamColor_atPort line 289
32. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.seamColor_sideOf line 336
33. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.colored line 342

    Source documentation

    Local decorations with proved complete seam matching produce an actual allowed occurrence assembly, not only rank/port endpoint lists.

    noncomputable def PortWiring.colored (h : W.ColorMatch d) : PortAssembly F W.Seam V W.seamArity :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly

34. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.signature line 353
35. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.mirror_portColor line 356
36. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.mirror_signature line 364
37. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.portSignature line 377
38. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.colorMatch_of_signature line 380
39. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.SignatureMatch line 392

    Source documentation

    Complete ordered names on each internal whole seam, before closing the four short-end interfaces.

    def PortPatch.SignatureMatch : Prop := ∀ i,
    …

40. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.complete_colorMatch line 395
41. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.doubleDecoration line 408
42. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.doubleSignature_left line 412
43. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.doubleSignature_right line 414
44. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_signatureMatch line 418
45. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.doubledWiring_colorMatch line 432
46. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.signature_eq_of_colors line 446
47. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.patch_signatureMatch line 465
48. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.shortFirst line 471
49. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.shortLast line 474
50. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doublePatch line 478
51. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleWiring line 479
52. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.double_colorMatch line 481
53. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly line 488

    Source documentation

    All longitudinal and transverse whole seams are present, with precisely matching original ordered color occurrences. No independent child-germ matching is used. Short ends here are closed against their mirror copies; splicing them into the old exterior remains a separate necessary operation.

    noncomputable def doubleAssembly : PortAssembly F B.doubleWiring.Seam
        (Fin (B.length+1) ⊕ Fin (B.length+1)) B.doubleWiring.seamArity :=
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly

54. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly_color line 492
55. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.portAt line 507

    Source documentation

    Enumerate the genuine ends of the old whole seams.

    def portAt (b : Bool) : S ≃ PortAt A.kind b where
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAt

56. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.attach_portAt line 519
57. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.portAt_arity line 522
58. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.decoration line 529

    Source documentation

    Decoration extracted from the actual old incidence, not chosen colors.

    noncomputable def decoration (v : V) : Decoration (A.kind v) F where
    …

59. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.decoration_portColor line 533
60. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.seamSignature line 545
61. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.decoration_signature line 548
62. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.portAt_signature line 557
63. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.arity_of_signature line 566
64. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftDecoration line 580
65. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftPlus line 584
66. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftMinus line 586
67. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftCycle line 592

    Source documentation

    The SAME seam handle cut has exactly this three-cycle, not identity closure: the outer ends lengthen its old boundary, and the mirror gallery self-closes as the new inner boundary.

    noncomputable def graftCycle (q : S) : Equiv.Perm (S ⊕ (I ⊕ Bool)) :=
    …

68. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftCycle_q line 595
69. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftCycle_false line 597
70. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftCycle_true line 599
71. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftCycle_internal line 601
72. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftCycle_old line 604
73. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graft_signature line 607
74. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftWiring line 633

    Source documentation

    Literal whole-port inverse-band wiring on the disjoint union of the old vertices and ALL band vertices.

    noncomputable def graftWiring (q : S) (hi : P.SignatureMatch d)
        (hp : ∀ b,portSignature d (P.plus (.inr b)).val=A.seamSignature q)
        (hm : ∀ b,portSignature d (P.minus (.inr b)).val=A.seamSignature q) :
        PortWiring (sumKind A.kind kind) where
    …

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

75. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftWiring_colorMatch line 646
76. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.graftAssembly line 657
77. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.map_portColor line 668
78. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.map_children line 671
79. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.map line 679
80. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.first_signature line 690
81. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.last_signature line 692
82. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.double_signature_plus line 695
83. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.double_signature_minus line 701
84. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.mapFacet line 716
85. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.seamChildren line 724
86. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.graftBand line 729

    Source documentation

    A actual gallery at the two old ends, including genuine transverse seams, is spliced by the same-q inverse-cut three-cycle. The endpoint lists are those of the OLD seam, so each original child occurrence survives in its own slot.

    noncomputable def graftBand (q : S)
        (B : RealizedBand (A.facet ⟨q,none⟩) (A.seamChildren q) (A.seamChildren q)) :=
    …

87. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.BandFacet line 744
88. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandColor line 749

    Source documentation

    Old row and column grades attach to their own ordered old occurrence; only common-graded cells are new facets. Equal old facet names are allowed.

    def bandColor : Option (Secondary (arity q) (arity q)) → A.BandFacet q
      | none => .inl (A.facet ⟨q,none⟩)
      | some (.row i) => .inl (A.facet ⟨q,some i⟩)
      | some (.col j) => .inl (A.facet ⟨q,some j⟩)
      | some (.cell i j) => .inr (i,j)

89. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.bandColor_parent_iff line 755
90. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.namedAtomicBand line 770

    Source documentation

    This is the very same obtained weighted atomic gallery, not a replacement chosen from its endpoints or ranks.

    noncomputable def namedAtomicBand : RealizedBand
        ((A.mapFacet (Sum.inl : F → A.BandFacet q)).facet ⟨q,none⟩)
        ((A.mapFacet (Sum.inl : F → A.BandFacet q)).seamChildren q)
        ((A.mapFacet (Sum.inl : F → A.BandFacet q)).seamChildren q) := by
    …

    Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.seamChildren

91. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.atomicBandGraft line 786
92. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.namedAtomicBand_parent_germs line 789
93. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_positive_parent line 809
94. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_negative_parent line 818
95. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.parent_next line 828
96. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graft_wire_plus line 844
97. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.graft_wire_symm line 850
98. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_plus_original line 857
99. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_minus_original line 860
100. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_plus_mirror line 863
101. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_minus_mirror line 866
102. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.kind line 878
103. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring line 879
104. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldPort line 884
105. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalPort line 886
106. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorInput line 891
107. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorOutput line 895
108. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.original_corner line 900
109. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirror_corner line 908
110. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_original line 918
111. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_mirror line 929
112. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_first line 940
113. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_last line 948
114. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_mirror_wrap line 957
115. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wire_old line 966
116. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.decoration line 983
117. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.colorMatch line 984
118. abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next line 988
119. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldSide line 989
120. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalSide line 991
121. def OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorSide line 993
122. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_original line 996
123. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_original_last line 1004
124. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_mirror line 1011
125. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_mirror_zero line 1018
126. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.realize_portAt_parent line 1027
127. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.parent_corner_of_next line 1034
128. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.old_corner line 1057
129. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_old_not_cut line 1065
130. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.next_old_cut line 1073
131. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.positive_side_exists line 1089

     Source documentation

     Every side has its literal representative at a positive WHOLE port.

     lemma positive_side_exists (a : Side W.Seam W.seamArity) :
         ∃ x : LocalEnd V kind, (kind x.1).table.endpoint x.2.1=true ∧ W.sideOf x=a := by
     …

     Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd

132. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.parent_input line 1110
133. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.parent_output line 1116
134. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldSide_color line 1126
135. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalSide_color line 1131
136. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorSide_color line 1133
137. lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.no_child_parent_local line 1143
138. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.parent_exhaustive line 1165

     Source documentation

     Exhaustion for the ACTUAL graft, derived from local tables. This does not infer a band witness from its endpoint lists. Every old parent occurrence and every original/mirror principal corner is retained as its literal side.

     theorem parent_exhaustive
         (hold : ∀ s i,A.facet ⟨s,some i⟩≠A.facet ⟨q,none⟩)
         (hband : ∀ v z,(B.decoration v).color z=A.facet ⟨q,none⟩ ↔
           z=⟨(B.kind v).input,none⟩ ∨ z=⟨(B.kind v).output,none⟩)
         (a : Side (wiring A q B).Seam (wiring A q B).seamArity)
         (ha : (A.graftBand q B).facet a=A.facet ⟨q,none⟩) :
         (∃ s,A.facet ⟨s,none⟩=A.facet ⟨q,none⟩ ∧ a=oldSide A q B s) ∨
         (∃ v,a=originalSide A q B v) ∨ (∃ v,a=mirrorSide A q B v) := by
     …

     Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldSide, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalSide, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorSide

139. theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.atomicBandGraft_parent_exhaustive line 1228

     Source documentation

     Parent exhaustion for the SAME produced named atomic graft. Both hypotheses of the general assembly theorem are discharged from the actual old incidence and actual weighted gallery; no independent cyclic template is substituted.

     theorem atomicBandGraft_parent_exhaustive
         (hold : ∀ s i,A.facet ⟨s,some i⟩≠A.facet ⟨q,none⟩)
         (a : Side (BandGraft.wiring (A.mapFacet (Sum.inl : F → A.BandFacet q)) q (A.namedAtomicBand q d)).Seam
           (BandGraft.wiring (A.mapFacet (Sum.inl : F → A.BandFacet q)) q (A.namedAtomicBand q d)).seamArity)
         (ha : (A.atomicBandGraft q d).facet a=.inl (A.facet ⟨q,none⟩)) :
         (∃ s,A.facet ⟨s,none⟩=A.facet ⟨q,none⟩ ∧
           a=BandGraft.oldSide (A.mapFacet (Sum.inl : F → A.BandFacet q)) q (A.namedAtomicBand q d) s) ∨
         (∃ v,a=BandGraft.originalSide (A.mapFacet (Sum.inl : F → A.BandFacet q)) q (A.namedAtomicBand q d) v) ∨
         (∃ v,a=BandGraft.mirrorSide (A.mapFacet (Sum.inl : F → A.BandFacet q)) q (A.namedAtomicBand q d) v) := by
     …

     Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldSide, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalSide, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorSide

140. theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.maximal_no_child_parent line 1257

     Source documentation

     The global no-parent-child fact used above follows from the exact normalized maximal-rank hypotheses of the manuscript reduction.

     theorem maximal_no_child_parent (h : D.Proper)
         (hn : ∀ f,D.rank f≤D.rank (D.ports.facet ⟨q,none⟩)) :
         ∀ s i,D.ports.facet ⟨s,some i⟩≠D.ports.facet ⟨q,none⟩ := by
     …