BandCycles.lean`

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

def OAI.IntegralCharacterVarieties.BoundaryBand.orbitList line 14
Source documentation
Unlike Perm.toList, this retains fixed-point boundary circles.
```
def orbitList (σ : Equiv.Perm α) (x : α) : List α :=
…
```
theorem OAI.IntegralCharacterVarieties.BoundaryBand.mem_orbitList line 17
theorem OAI.IntegralCharacterVarieties.BoundaryBand.orbitList_nodup line 25
theorem OAI.IntegralCharacterVarieties.BoundaryBand.orbitList_formPerm line 30
theorem OAI.IntegralCharacterVarieties.BoundaryBand.orbitList_head line 37
structure OAI.IntegralCharacterVarieties.BoundaryBand.Exposure line 53
Source documentation
Every complete orbit is retained. The residual fixes EACH removed occurrence, not merely its facet rank or its boundary-component count.
```
structure Exposure (σ : Equiv.Perm α) (x y : α) where
…
```
theorem OAI.IntegralCharacterVarieties.BoundaryBand.exposure_exists line 66
Source documentation
Produce the canonical cycle exposure for ANY distinct pair of feet.
```
theorem exposure_exists (σ : Equiv.Perm α) (x y : α) (hxy : x≠y) :
    Nonempty (Exposure σ x y) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.Exposure
theorem OAI.IntegralCharacterVarieties.BoundaryBand.Exposure.after line 121
Source documentation
Exact successor, including every untouched edge, for the produced exposure.
```
theorem Exposure.after {σ : Equiv.Perm α} {x y : α} (E : Exposure σ x y) :
    incomingSwitch σ x y=(if E.oneCircle then (x::E.left).formPerm*(y::E.right).formPerm
      else ((x::E.left)++(y::E.right)).formPerm)*E.rest := by
…
```
Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.Exposure, OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch
theorem OAI.IntegralCharacterVarieties.BoundaryBand.sameCycle_iff_list line 137
Source documentation
Agreement on every member of a nodup cyclic list identifies its whole orbit, including a singleton. This excludes hidden fresh-parent or exterior germs.
```
theorem sameCycle_iff_list (σ : Equiv.Perm α) (L : List α) (hn : L.Nodup)
    (x : α) (hx : x∈L) (ha : ∀ z∈L,σ z=L.formPerm z) (z : α) :
    σ.SameCycle x z ↔ z∈L := by
…
```
theorem OAI.IntegralCharacterVarieties.BoundaryBand.Exposure.split_exhaust line 157
Source documentation
The two lists produced in the split case are the COMPLETE new boundary circles, not a compatible but nonexhaustive list of contacts.
```
theorem Exposure.split_exhaust {σ : Equiv.Perm α} {x y : α} (E : Exposure σ x y)
    (he : E.oneCircle=true) (z : α) :
    (incomingSwitch σ x y).SameCycle x z ↔ z∈x::E.left := by
…
```
Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.Exposure, OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch
theorem OAI.IntegralCharacterVarieties.BoundaryBand.Exposure.split_exhaust_right line 170
theorem OAI.IntegralCharacterVarieties.BoundaryBand.Exposure.join_exhaust line 186
Source documentation
The joined cycle retains both old cycles in full, even when one was a single fixed side occurrence.
```
theorem Exposure.join_exhaust {σ : Equiv.Perm α} {x y : α} (E : Exposure σ x y)
    (he : E.oneCircle=false) (z : α) :
    (incomingSwitch σ x y).SameCycle x z ↔ z∈(x::E.left)++(y::E.right) := by
…
```
Mentions: OAI.IntegralCharacterVarieties.BoundaryBand.Exposure, OAI.IntegralCharacterVarieties.BoundaryBand.incomingSwitch
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.sideCircle line 205
Source documentation
The old boundary circle of an occurrence, read from the exhaustive boundarySide equivalence, not inferred from its rank or its facet color.
```
def sideCircle (a : Side S arity) : D.BoundaryCircle :=
…
```
theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.mem_boundarySides_iff line 209
theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundary_sameCycle_iff line 225
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryBandExposure line 237
Source documentation
Universal exposure used by every chronological band step of a whole-port move. Its branch is decided by old occurrence circles, not colors.
```
def boundaryBandExposure (a b : Side S arity) (hab : a≠b) :
    Exposure D.ports.vertexAssembly.corners.boundaryNext a b :=
…
```
theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryBandExposure_one line 241
theorem OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.actual_boundaryBand_exposure line 247
Source documentation
The exact split/join successor and its produced exhaustive witness for ANY band feet of the original finite Diagram. No genus choice is asserted.
```
theorem actual_boundaryBand_exposure (a b : Side S arity) (hab : a≠b) :
    let E := D.boundaryBandExposure a b hab
…
```