OAI/Algebra/GroupRing/FramedLoopIdentities.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TorsionFreeZeroDivisors.FramedLoopIdentities.frames line 22
2. lemma OAI.TorsionFreeZeroDivisors.FramedLoopIdentities.frames_labels line 24
3. lemma OAI.TorsionFreeZeroDivisors.FramedLoopIdentities.frames_closed line 31
4. def OAI.TorsionFreeZeroDivisors.FramedLoopIdentities.area line 36
5. theorem OAI.TorsionFreeZeroDivisors.FramedLoopIdentities.identity_area_zero line 42

   Source documentation

   A free identity among conjugated closed relators has exactly zero lifted edge area whenever sharp arrangement exclusion reduces all its actual spherical pictures. The frames are not erased or existentially replaced.

   theorem identity_area_zero
       (he : FreeGroup.mk (AlgebraicPictures.word (relWords Γ label rel) ts)=1)
       (ht : ∀t∈ts,value v (t.word (relWords Γ label rel))=1)
       (hred : ∀{O : Type}[Fintype O](a : SphericalPicture.Data (O:=O) Γ label WordPairing.inverseLetter),
   …

   Mentions: OAI.TorsionFreeZeroDivisors.AlgebraicPictures.word, OAI.TorsionFreeZeroDivisors.SphericalPicture.Data, OAI.TorsionFreeZeroDivisors.WordPairing.inverseLetter