OAI/GroupTheory/Kervaire/RibbonRigidity.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KervaireRibbon.orbitWeight_coboundary line 43
2. lemma OAI.KervaireRibbon.list_prod_single_difference line 51
3. lemma OAI.KervaireRibbon.orbitWeight_as_list line 70
4. lemma OAI.KervaireRibbon.rotate_orbit_list line 79
5. lemma OAI.KervaireRibbon.orbitWeight_single_difference line 86
6. lemma OAI.KervaireRibbon.one_defect_of_holonomy line 97

   Source documentation

   A connection which is a pure gauge away from one directed corner is a pure gauge everywhere as soon as its exceptional face has trivial holonomy.

   lemma one_defect_of_holonomy [Fintype D] (σ : Equiv.Perm D) (b u : D → A) (p : D)
       {Z : Type*} (n : Z → ℕ) (e : (Σ z, Fin (n z+1)) ≃ D)
       (he : ∀ z i, σ (e ⟨z,i⟩) = e ⟨z,finRotate (n z+1) i⟩)
       (hu : ∀ d, d ≠ p → b d = u (σ d) * (u d)⁻¹)
       (hm : ∀ z, orbitWeight (finRotate (n z+1)) (fun i ↦ b (e ⟨z,i⟩)) (n z+1) 0 = 1) :
       b p = u (σ p) * (u p)⁻¹ := by
   …

7. lemma OAI.KervaireRibbon.holonomy_of_coboundary line 115
8. lemma OAI.KervaireRibbon.successor_pow_inl line 134
9. lemma OAI.KervaireRibbon.successor_pow_inr line 141
10. lemma OAI.KervaireRibbon.successor_cycles line 147
11. lemma OAI.KervaireRibbon.numCycles_successor line 170
12. lemma OAI.KervaireRibbon.traversal_ne_zero line 177
13. theorem OAI.KervaireRibbon.planar_corner_rigidity line 184

    Source documentation

    A single deviating corner on a connected planar assembly of literal word disks cannot carry a nontrivial defect. This is the analytic boundary theorem, with all other circuit products discharged by gauge telescoping.

    theorem planar_corner_rigidity [Nonempty I] [Nonempty K]
        (ρ : Perm I) (hρ : ∀ i j, ρ.SameCycle i j) (a : I → A)
        (s : I → ℤ) (hs : ∀ i, s i = 1 ∨ s i = -1) (hsum : (∑ i, s i) = 1 ∨ (∑ i, s i) = -1)
        (θ : Perm (Slot I K)) (hθ : ∀ d, θ (θ d) = d)
        (hop : ∀ d, traversalSign s (θ d) = - traversalSign s d)
        (hconn : components (successor ρ) θ = ⊤) (hp : planar (successor ρ) θ)
        (u : Slot I K → A) (p : Slot I K)
        (hu : ∀ d, d ≠ p → (labels ρ a d)⁻¹ = u (θ d) * (u (successor ρ d))⁻¹) :
        (labels ρ a p)⁻¹ = u (θ p) * (u (successor ρ p))⁻¹ := by
    …

    Mentions: OAI.KervaireRibbon.components, OAI.KervaireRibbon.planar