CornerHolonomy.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerBasis_start line 16
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryCornerBasis line 26
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerFinish_boundary line 32
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryEdge_cornerGauge line 42

lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryWord_cornerGauge line 67

Source documentation

Based boundary holonomy telescopes at every interior corner; only the independent chosen base corner remains.

lemma boundaryWord_cornerGauge (f : F) (b : Fin (D.boundaryCount f)) :
    (D.boundaryWord f b).eval φ (D.cornerGaugeGenerators G g)=
      (D.boundaryCornerBasis G f b ⟨0,D.boundaryPositive f b⟩).toUnit*
        (D.boundaryWord f b).eval φ g*
          (D.boundaryCornerBasis G f b ⟨0,D.boundaryPositive f b⟩).toUnit⁻¹ := by
…

def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.CornerBases.Based line 80
Source documentation
Fix the selected base corner of every boundary. These are coordinate gauges, not extra equations on an old local system.
```
def CornerBases.Based (G : D.CornerBases (R:=A)) : Prop :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedCorner_boundaryWord line 83
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedCorner_surfaceWord line 94
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.basedCornerSolution line 111
Source documentation
Arbitrary independent internal corner gauges act on the full solution, not just on boundary holonomies or its regular seam equations. The original scalar punctures and handles are unchanged.
```
def basedCornerSolution (P : D.Punctures R) (x : D.Solution P A) : D.Solution P A := by
…
```
abbrev OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.BoundaryBases line 132
def OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerBasesOfBoundary line 137
Source documentation
Transport the exhaustively indexed boundary bases to the side occurrences, including every repeated facet and every cyclic base position.
```
def cornerBasesOfBoundary (B : D.BoundaryBases (A:=A)) : D.CornerBases (R:=A) := fun a =>
…
```
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.boundaryBasis_ofBoundary line 143
lemma OAI.IntegralCharacterVarieties.SurfacePresentation.Diagram.cornerBasesOfBoundary_based line 158
def OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixProduct line 169
Source documentation
Chronological prefix products: the first edge acts first.
```
def prefixProduct (e : ℕ → G) : ℕ → G
  | 0 => 1
  | n+1 => e n*prefixProduct e n
```
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixProduct_zero line 173
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixProduct_succ line 174
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixProduct_eq_reverse line 177
def OAI.IntegralCharacterVarieties.SurfaceSurgery.cycleEdge line 187
Source documentation
Extension by 1 is solely for evaluating the finite prefix; no selected path ever encounters an extended edge.
```
def cycleEdge {n : ℕ} (e : Fin n → G) (i : ℕ) : G :=
…
```
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.cycleEdge_at line 190
def OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixBasis line 193
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixBasis_zero line 196
lemma OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixProduct_cycle line 199
theorem OAI.IntegralCharacterVarieties.SurfaceSurgery.prefix_gauge line 206
Source documentation
All interior edges become 1; the FINAL side retains precisely the original based holonomy, not a merely conjugate matrix.
```
theorem prefix_gauge {n : ℕ} (hn : 0<n) (e : Fin n → G) (i : Fin n) :
    prefixBasis e ⟨(i.val+1)%n,Nat.mod_lt _ hn⟩*e i*(prefixBasis e i)⁻¹=
      if i.val+1<n then 1 else (List.ofFn e).reverse.prod := by
…
```
Mentions: OAI.IntegralCharacterVarieties.SurfaceSurgery.prefixBasis