DoubledStrips.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

Boundary circuits and germ exhaustion of doubled secondary strips.

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

lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.endOf_positive line 17
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.endOf_negative line 19
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_wired line 24
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_wire_original line 37
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_wire_mirror line 42
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_wire_exposed_plus line 47
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortPatch.double_wire_exposed_minus line 55
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_isNone line 67
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Kind.mirror_negative line 71
abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.DoubleEnd line 79
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origEnd line 80
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorEnd line 81
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStripSide line 83
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorStripSide line 85
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStrip_next line 87
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorStrip_next line 97
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStrip_edge line 107
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorStrip_edge line 126
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.root_plus_port line 148
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.root_minus_port line 157
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.tip_plus_port line 165
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.tip_minus_port line 174
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.double_exposed_side line 188
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStrip_root line 224
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorStrip_tip line 228
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStrip_sameRoot line 237
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorStrip_sameRoot line 249
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle line 262
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_next line 265
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_surj line 279
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_sameRoot line 293
theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_isCycle line 305
Source documentation
Each actual secondary run doubles to EXACTLY one boundary circuit. The successors are those of the literal whole-port double, including every transverse split/merge seam; there is no postulated replacement permutation.
```
theorem stripCycle_isCycle (r : B.StripNode) :
    B.doubleAssembly.vertexAssembly.corners.boundaryNext.IsCycleOn (B.stripCycle r) := by
…
```
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.sideOf_isNone line 318
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.oriented_side_injective line 324
Source documentation
Every actual side has one and only one positively oriented local germ, not merely one endpoint at a positive port.
```
lemma oriented_side_injective (x y : LocalEnd V kind)
    (hx : (kind x.1).table.endpoint x.2.1=x.2.2.isNone)
    (hy : (kind y.1).table.endpoint y.2.1=y.2.2.isNone)
    (h : W.sideOf x=W.sideOf y) : x=y := by
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.LocalEnd
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.oriented_side_exists line 333
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStripSide_injective line 350
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorStripSide_injective line 362
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origStrip_ne_mirror line 373
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripCycle_disjoint line 386
Source documentation
Even when old facet labels repeat, distinct strip roots give disjoint actual boundary circuits. They may therefore be assigned distinct fresh disk facets rather than silently joining unrelated components.
```
lemma stripCycle_disjoint {r t : B.StripNode} (h : r≠t) : Disjoint (B.stripCycle r) (B.stripCycle t) := by
…
```
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origPrincipal line 400
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorPrincipal line 402
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.positive_classification line 404
theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.double_side_exhaustive line 428
Source documentation
Exhaustion of every literal side of the doubled cut band. All facets of lower rank arise from the enumerated secondary strips; transverse seams do not leave hidden boundary germs.
```
theorem double_side_exhaustive (s : Side B.doubleWiring.Seam B.doubleWiring.seamArity) :
    (∃ v,s=B.origPrincipal v) ∨ (∃ v,s=B.mirrorPrincipal v) ∨
    ∃ x : B.StripNode,s=B.origStripSide x ∨ s=B.mirrorStripSide x := by
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side