OAI/Geometry/HyperbolicGroups/GraphAction.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.MasterGraph.Step.value line 18
2. lemma OAI.HyperbolicObstruction.MasterGraph.Step.value_symm line 21
3. def OAI.HyperbolicObstruction.MasterGraph.Path.eval line 28
4. lemma OAI.HyperbolicObstruction.MasterGraph.Path.eval_append line 32
5. lemma OAI.HyperbolicObstruction.MasterGraph.Path.eval_symm line 38
6. def OAI.HyperbolicObstruction.MasterGraph.Path.Compatible line 45

   Source documentation

   A field-sign map is compatible with each actual edge traversal.

   def Compatible (σ : Field → Bool) : {a b : Vertex} → Path a b → Prop
     | _, _, .nil _ => True
     | _, _, .cons s p => σ s.field = s.forward ∧ p.Compatible σ

   Mentions: OAI.HyperbolicObstruction.MasterGraph.Vertex, OAI.HyperbolicObstruction.MasterGraph.Path

7. lemma OAI.HyperbolicObstruction.MasterGraph.Path.compatible_congr line 49
8. lemma OAI.HyperbolicObstruction.MasterGraph.Path.exists_compatible line 57
9. def OAI.HyperbolicObstruction.MasterGraph.Path.read line 71
10. lemma OAI.HyperbolicObstruction.MasterGraph.Path.eval_word line 74
11. lemma OAI.HyperbolicObstruction.MasterGraph.Path.bound line 85
12. structure OAI.HyperbolicObstruction.MasterGraph.Potential line 103

    Source documentation

    Actual consistency of the labelled graph in a group, not a metric configuration or a conclusion of the sampling argument.

    structure Potential {L G : Type*} [Group G] (label : Field → L) (letter : L → G) where
    …

13. lemma OAI.HyperbolicObstruction.MasterGraph.Potential.step line 112
14. lemma OAI.HyperbolicObstruction.MasterGraph.Potential.path line 123
15. lemma OAI.HyperbolicObstruction.MasterGraph.Potential.route line 128
16. lemma OAI.HyperbolicObstruction.MasterGraph.Potential.orbit_path line 131
17. def OAI.HyperbolicObstruction.MasterGraph.Potential.of_relators line 138

    Source documentation

    Rooted potentials are provided by the actual cycle relators on fixed routes.

    def of_relators (label : Field → L) (letter : L → G)
        (hroot : (MasterGraph.route root).eval label letter = 1)
        (hloop : ∀ f, ((MasterGraph.route (source f)).append
          (.cons (Step.pos f) (MasterGraph.route (target f)).symm)).eval label letter = 1) :
        Potential label letter where
    …

    Mentions: OAI.HyperbolicObstruction.MasterGraph.route, OAI.HyperbolicObstruction.MasterGraph.root, OAI.HyperbolicObstruction.MasterGraph.source, OAI.HyperbolicObstruction.MasterGraph.Step.pos, OAI.HyperbolicObstruction.MasterGraph.target, OAI.HyperbolicObstruction.MasterGraph.Potential