OAI/GroupTheory/Hyperbolic/FullGluing.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Release075.FullFilling.wedge line 11
2. abbrev OAI.Release075.FullFilling.reword line 157
3. theorem OAI.Release075.FullFilling.trace_reword line 160
4. theorem OAI.Release075.FullFilling.rotateAppend line 164
5. theorem OAI.Release075.FullFilling.foldHead line 170
6. theorem OAI.Release075.FullFilling.erase line 181
7. theorem OAI.Release075.FullFilling.erase_reverse line 191
8. theorem OAI.Release075.FullFilling.trace_palindrome line 210
9. theorem OAI.Release075.FullFilling.trace_unique line 227

   Source documentation

   The signed triangle chain of a full disk depends only on its typed boundary. This is proved by actual exterior folds, retaining detached components.

   theorem trace_unique
       (hempty : ∀ D : TriangleSphere flip color face, IsEmpty D.Dipole → IsEmpty D.Dart)
       (hi : Function.Involutive flip) (hn : ∀ e, color e ≠ color (flip e))
       (hf : ∀ a b c, face a b c → face (flip a) (flip c) (flip b))
       (F : E → E → E → M)
       (hrot : ∀ a b c, face a b c → F b c a = F a b c)
       (hmir : ∀ a b c, face a b c → F (flip a) (flip c) (flip b) = -F a b c)
       (hdeg : ∀ a b, F a b a = 0)
       {x : V} {w : List E} (hw : WordPath flip color x x w)
       (D D' : FullFilling flip color face w) : D.trace F = D'.trace F := by
   …

   Mentions: OAI.Release075.TriangleSphere, OAI.Release075.WordPath, OAI.Release075.FullFilling

10. theorem OAI.Release075.FullFilling.trace_cyclic line 265

    Source documentation

    Cyclic reindexing of corners of genuine triangles.

    theorem trace_cyclic {w : List E} (D : FullFilling flip color face w)
        (ht : ∀ a, a ∉ D.boundary → (D.next^3) a = a)
        (F : E → E → E → M) : D.trace (fun a b c => F b c a) = D.trace F := by
    …

    Mentions: OAI.Release075.FullFilling

11. theorem OAI.Release075.FullFilling.trace_add line 284
12. theorem OAI.Release075.FullFilling.trace_cyclic_sum line 292
13. theorem OAI.Release075.FullFilling.trace_map line 309
14. theorem OAI.Release075.FullFilling.trace_congr line 318
15. theorem OAI.Release075.FullFilling.trace_edge line 331

    Source documentation

    Integral Stokes accounting for an antisymmetric edge evaluation.

    theorem trace_edge {w : List E} (D : FullFilling flip color face w)
        (F : E → M) (hf : ∀ e, F (flip e) = -F e) :
        D.trace (fun a _ _ => F a) = -(w.map F).sum := by
    …

    Mentions: OAI.Release075.FullFilling

16. theorem OAI.Release075.TriangleFilling.full_triangular line 365