OAI/Algebra/GroupRing/PictureChains.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.TorsionFreeZeroDivisors.PictureChains.Lift line 20

   Source documentation

   The actual group-coordinate lift of every boundary occurrence. Rotation and paired sides share the prescribed endpoint in the Cayley one-skeleton.

   structure Lift where
   …

2. lemma OAI.TorsionFreeZeroDivisors.PictureChains.reverse_value line 26
3. lemma OAI.TorsionFreeZeroDivisors.PictureChains.inverse_segment line 29
4. def OAI.TorsionFreeZeroDivisors.PictureChains.band line 34
5. def OAI.TorsionFreeZeroDivisors.PictureChains.tighten line 46
6. def OAI.TorsionFreeZeroDivisors.PictureChains.chain line 68
7. lemma OAI.TorsionFreeZeroDivisors.PictureChains.cancel_pair line 70
8. lemma OAI.TorsionFreeZeroDivisors.PictureChains.sum_remaining line 75
9. lemma OAI.TorsionFreeZeroDivisors.PictureChains.band_chain line 95
10. lemma OAI.TorsionFreeZeroDivisors.PictureChains.tighten_chain line 103
11. theorem OAI.TorsionFreeZeroDivisors.PictureChains.chain_eq_zero line 114

    Source documentation

    Every actual lifted genus-zero spherical boundary picture which reduces as proved by the sharp arrangement exclusion has ZERO integral cell-chain charge. Only an antisymmetric physical cone-edge contribution is needed.

    theorem chain_eq_zero (h : ReducesToEmpty Γ label inv a) : chain a l c=0 := by
    …

    Mentions: OAI.TorsionFreeZeroDivisors.PictureChains.chain