StripFacets.lean`

78 declarations, 0 contain sorry, 0 declared as axioms

Connected-strip facet labels and the refined atomic graft.

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

def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.boundaryPerm line 17
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.boundaryPerm_local line 19
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.cornerColor_of_boundary line 24
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.assembleBoundary line 38
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.rewireFacets line 45
Source documentation
Carry a cycle-constant facet assignment through the actual whole-port surgery. The two invariances are finite combinatorial checks, not a solution, coverage, or chart hypothesis.
```
noncomputable def rewireFacets (C : Equiv.Perm W.Seam)
    (hC : ∀ s,W.seamArity (C s)=W.seamArity s)
    (f : Side W.Seam W.seamArity → F)
    (hn : ∀ a,f (W.boundaryPerm a)=f a)
    (hq : ∀ a,f (W.cutAction C hC a)=f a) :
    PortAssembly F W.Seam V W.seamArity :=
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot line 68
Source documentation
Root of the literal doubled strip containing this side, if any. Parent sides receive none. Selection is unique by strip disjointness.
```
noncomputable def sideStripRoot (s : Side B.doubleWiring.Seam B.doubleWiring.seamArity) :
    Option B.StripRoot :=
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot_eq_some_iff line 72
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot_of_orig line 88
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot_of_mirror line 91
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot_next line 95
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.rootFacet line 109
Source documentation
Every contacted strip inherits precisely its old ordered-child facet; every other strip is a separate new disk, even when ranks/colors coincide.
```
noncomputable def rootFacet (h : List.Disjoint a b) (contact : B.ShortChild → G) :
    B.StripRoot → G ⊕ B.FreshStrip := fun r =>
…
```
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet line 115
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet_next line 122
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripDecomposition_inl line 128
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.stripDecomposition_inr line 130
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.rootFacet_contact line 133
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.rootFacet_fresh line 137
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet_input line 142
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet_output line 147
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origPrincipal_ne_origStrip line 157
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.origPrincipal_ne_mirrorStrip line 173
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorPrincipal_ne_origStrip line 182
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.mirrorPrincipal_ne_mirrorStrip line 198
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot_origPrincipal line 217
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.sideStripRoot_mirrorPrincipal line 225
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet_origPrincipal line 234
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet_mirrorPrincipal line 238
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly_origStrip line 243
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly_mirrorStrip line 249
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.input_parent_all line 257
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.output_parent_all line 266
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly_origPrincipal line 272
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleAssembly_mirrorPrincipal line 277
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedFacetRank line 287
Source documentation
Rank of a fresh connected strip, not a rank-only grouping of disks.
```
def refinedFacetRank (old : G → ℕ) (raw : F → ℕ) : G ⊕ B.FreshStrip → ℕ
  | .inl g => old g
  | .inr r => raw (B.stripColor r.val.val)
```
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.rootFacet_rank line 291
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleFacet_rank line 301
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration line 325
Source documentation
Replace coarse atom colors by the actual connected strip roots on the SAME band. Contacted strips inherit old facets; untouched strips are separate disks.
```
noncomputable def refinedDecoration (h : List.Disjoint a b) (parent : G)
    (contact : B.ShortChild → G) (v : Fin (B.length+1)) :
    Decoration (B.kind v) (G ⊕ B.FreshStrip) where
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration_input_parent line 332
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration_output_parent line 336
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration_chain line 343
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration_input_child line 364
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration_output_child line 375
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedInput line 384
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedOutput line 387
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedBand line 392
theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedBand_same_wiring line 412
Source documentation
The construction changes ONLY facet names; no chosen topology, ports, transverse seam, or successor is replaced by a cyclic template.
```
theorem refinedBand_same_wiring (h : List.Disjoint a b) (parent : G) (contact : B.ShortChild → G) :
    (B.refinedBand h parent contact).doubleWiring=B.doubleWiring := rfl
…
```
Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.doubleWiring
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedDecoration_rank line 418
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.RealizedBand.refinedBand_conservative line 429
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomic_input_arity line 446
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomic_output_arity line 449
def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.inputIndex line 454
def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.outputIndex line 456
def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.stripContact line 462
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomic_refinedInput line 466
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.atomic_refinedOutput line 471
def OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.refinedAtomicBand line 479
Source documentation
This named-root recoloring is obtained from the exact common-atom gallery, not existentially chosen from its rank and endpoint signature.
```
noncomputable def refinedAtomicBand (parent : G) :
    RealizedBand (Sum.inl parent : G ⊕ d.atomicBand.FreshStrip)
      ((List.ofFn row).map Sum.inl) ((List.ofFn col).map Sum.inl) :=
…
```
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.inputIndex_color line 494
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.outputIndex_color line 506
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.stripColor_ne_parent line 521
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.secondaryRank_lt line 532
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.stripRank_lt line 546
Source documentation
The actual connected strips produced by the common-array algorithm are proper lower-rank facets, including its branch parents. Rank conservation alone would not prove this; it follows from the retained fresh labels.
```
lemma stripRank_lt (hr : ∀ i,d.secondaryRank (.row i)<r)
    (hc : ∀ j,d.secondaryRank (.col j)<r) (x : d.atomicBand.StripNode) :
    freshRank r d.secondaryRank (d.atomicBand.stripColor x)<r := by
…
```
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.stripContact_rank line 554
lemma OAI.IntegralCharacterVarieties.TwoFlagBand.RankShape.refinedAtomicBand_conservative line 571
abbrev OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.RefinedBandFacet line 587
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedBandForSeam line 590
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedAtomicGraft line 602
Source documentation
Complete occurrence assembly, with every untouched component of the literal band double a DISTINCT fresh strip disk. No new incidence is guessed.
```
noncomputable def refinedAtomicGraft :=
…
```
def OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedRank line 612
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedBandForSeam_rank line 615
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedBandForSeam_parent_germs line 628

theorem OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedAtomicGraft_parent_exhaustive line 661

Source documentation

This exhausts parent germs of the connected-strip refinement, not merely of a coarsely labeled band with possibly merged disconnected child components.

theorem refinedAtomicGraft_parent_exhaustive
    (hp : rank (A.facet ⟨q,none⟩)=r)
    (hc : ∀ i,rank (A.facet ⟨q,some i⟩)=d.secondaryRank (.row i))
    (hc' : ∀ i,rank (A.facet ⟨q,some i⟩)=d.secondaryRank (.col i))
    (hlt : ∀ i,rank (A.facet ⟨q,some i⟩)<r)
    (hold : ∀ s i,A.facet ⟨s,some i⟩≠A.facet ⟨q,none⟩)
    (a : Side (BandGraft.wiring (A.mapFacet (Sum.inl : F → A.RefinedBandFacet q d)) q
      (A.refinedBandForSeam q d)).Seam
      (BandGraft.wiring (A.mapFacet (Sum.inl : F → A.RefinedBandFacet q d)) q
      (A.refinedBandForSeam q d)).seamArity)
    (ha : (A.refinedAtomicGraft q d).facet a=.inl (A.facet ⟨q,none⟩)) :
    (∃ s,A.facet ⟨s,none⟩=A.facet ⟨q,none⟩ ∧
…

Mentions: OAI.IntegralCharacterVarieties.OccurrenceIncidence.Side, OAI.IntegralCharacterVarieties.OccurrenceIncidence.BandGraft.wiring

lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedRank_fresh_lt line 687
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.decoration_conservative line 698
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.VertexTable.Decoration.mirror_conservative line 712
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortWiring.colored_seamRank line 726
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.graftBand_seamRank line 735
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedBandForSeam_shortRoot_injective line 756
Source documentation
Injection is proved from the uncoloured atomic row/column topology. The actual two endpoint lists can be identical; no false disjointness assumption on their old facet colours is used.
```
lemma refinedBandForSeam_shortRoot_injective :
    Function.Injective (A.refinedBandForSeam q d).shortRoot := by
…
```
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedBandForSeam_shortRoot_eq line 778
lemma OAI.IntegralCharacterVarieties.OccurrenceIncidence.PortAssembly.refinedBandForSeam_fresh_eq line 785