OAI/Geometry/HyperbolicGroups/WalkRawPosition.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.isLetter line 18
2. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RawPosition line 22

   Source documentation

   Indexed positions, NOT generator labels. Two fields carrying an equal numerical letter remain distinct positions.

   abbrev RawPosition := Top n w ⊕ (FanTriangle n w ⊕ ((Square n w × Fin 4) ⊕ (Six n d × Fin 6)))

   Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Top, OAI.HyperbolicObstruction.ConeSkeleton.FanTriangle, OAI.HyperbolicObstruction.ConeSkeleton.Square, OAI.HyperbolicObstruction.ConeSkeleton.Six

3. def OAI.HyperbolicObstruction.ConeSkeleton.rawPosition line 24
4. def OAI.HyperbolicObstruction.ConeSkeleton.looseMacro line 30
5. def OAI.HyperbolicObstruction.ConeSkeleton.rawRepresentative line 33
6. lemma OAI.HyperbolicObstruction.ConeSkeleton.macro_letter_cases line 39
7. lemma OAI.HyperbolicObstruction.ConeSkeleton.fan_letter_index line 62
8. lemma OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite_twice line 72
9. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_step_cases line 78
10. lemma OAI.HyperbolicObstruction.ConeSkeleton.rev_ne line 98
11. lemma OAI.HyperbolicObstruction.ConeSkeleton.raw_position_reverse line 105

    Source documentation

    Reversed label sides at the SAME indexed position are literally opposite indexed steps. This excludes indexed loops in the coincidence-contact graph.

    lemma raw_position_reverse {s t : WalkStep n w d}
        (hs : isLetter n w (walkLabel n w d s) = true)
        (ht : isLetter n w (walkLabel n w d t) = true)
        (hp : rawPosition n w d s = rawPosition n w d t)
        (he : walkLabel n w d t = rev n w (walkLabel n w d s)) :
        t = walkOpposite n w d s := by
    …

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.WalkStep, OAI.HyperbolicObstruction.ConeSkeleton.isLetter, OAI.HyperbolicObstruction.ConeSkeleton.walkLabel, OAI.HyperbolicObstruction.ConeSkeleton.rawPosition, OAI.HyperbolicObstruction.ConeSkeleton.rev, OAI.HyperbolicObstruction.ConeSkeleton.walkOpposite

12. lemma OAI.HyperbolicObstruction.ConeSkeleton.contact_different line 128