AllSeams.lean`

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Framed flags at every seam of a marked cut

The first, last, reflected, internal, and inherited seams satisfy their framed flag equations.

lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.allSeams_of_families line 22
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.allSeams_of_eightFamilies line 43
Source documentation
The eight seam families exhaust the marked band graft.
```
lemma allSeams_of_eightFamilies (P : (wiring A q B).Seam → Prop)
    (hselected : P (oldPort A q B q true))
    (hinherited : ∀ s,s≠q → P (oldPort A q B s true))
    (hfirst : P (originalPort A q B 0 true))
    (horiginal : ∀ j : Fin B.length,P (originalPort A q B j.succ true))
    (hlastMirror : P (mirrorOutput A q B (Fin.last B.length)))
    (hmirror : ∀ j : Fin B.length,P (mirrorOutput A q B j.castSucc))
    (hpositive : ∀ a,P (branchPlus A q B a))
    (hnegative : ∀ a,P (branchNegPlus A q B a)) : ∀ s,P s := by
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldPort, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalPort, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorOutput, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchPlus, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchNegPlus
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.allSeams_of_eightFamilies_forall line 66
Source documentation
A parameterized family of flags satisfies every seam equation if it satisfies each seam family.
```
lemma allSeams_of_eightFamilies_forall {H : Type} {Q : Prop}
    (P : H → (wiring A q B).Seam → Prop)
    (hselected : ∀ h,Q → P h (oldPort A q B q true))
    (hinherited : ∀ h,Q → ∀ s,s≠q → P h (oldPort A q B s true))
    (hfirst : ∀ h,P h (originalPort A q B 0 true))
    (horiginal : ∀ h (j : Fin B.length),P h (originalPort A q B j.succ true))
    (hlastMirror : ∀ h,P h (mirrorOutput A q B (Fin.last B.length)))
    (hmirror : ∀ h (j : Fin B.length),P h (mirrorOutput A q B j.castSucc))
    (hpositive : ∀ h a,P h (branchPlus A q B a))
    (hnegative : ∀ h a,P h (branchNegPlus A q B a)) : ∀ h,Q → ∀ s,P h s := by
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.oldPort, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.originalPort, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.mirrorOutput, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchPlus, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.branchNegPlus
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCutOriginalSideValues line 103
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCutInnerTransport line 107
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.FramedSeamEquation line 114
Source documentation
The framed flag equation at a seam of a diagram.
```
def FramedSeamEquation (s : S) : Prop :=
…
```
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutSeamFlag line 120
Source documentation
The framed flag equation at a seam of the marked cut.
```
abbrev MarkedCutSeamFlag (handle : (C).HandleValues (R:=K))
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.HandleValues
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutSelectedSeam line 127
Source documentation
The selected old seam satisfies its framed flag equation.
```
def MarkedCutSelectedSeam : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_selectedSeam line 134
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutInheritedSeams line 140
Source documentation
Inherited old seams satisfy their framed flag equations.
```
def MarkedCutInheritedSeams : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_inheritedSeams line 148
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutFirstSeam line 154
Source documentation
The first marked original seam satisfies its framed flag equation.
```
def MarkedCutFirstSeam : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_firstSeam line 159
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutOriginalInternalSeams line 165
Source documentation
The internal marked original seams satisfy their framed flag equations.
```
def MarkedCutOriginalInternalSeams : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_originalInternalSeams line 170
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutLastMirrorSeam line 178
Source documentation
The last marked mirror seam satisfies its framed flag equation.
```
def MarkedCutLastMirrorSeam : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_lastMirrorSeam line 183
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutMirrorInternalSeams line 189
Source documentation
The internal marked mirror seams satisfy their framed flag equations.
```
def MarkedCutMirrorInternalSeams : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_mirrorInternalSeams line 194
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutPositiveSeams line 202
Source documentation
The positive seam family satisfies its framed flag equations.
```
def MarkedCutPositiveSeams : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_positiveSeams line 206
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutNegativeSeams line 213
Source documentation
The negative seam family satisfies its framed flag equations.
```
def MarkedCutNegativeSeams : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_negativeSeams line 217
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.MarkedCutSeamEquations line 224
Source documentation
All seam equations of a marked cut follow from the original named seam flags.
```
def MarkedCutSeamEquations : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.markedCut_allSeams line 231