OAI/Geometry/HyperbolicGroups/LinkApex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.FanLink.T line 16
2. def OAI.HyperbolicObstruction.FanLink.allDominant line 18
3. lemma OAI.HyperbolicObstruction.FanLink.turn_eq line 22
4. lemma OAI.HyperbolicObstruction.FanLink.T_eq line 23
5. lemma OAI.HyperbolicObstruction.FanLink.D_allDominant line 25
6. lemma OAI.HyperbolicObstruction.FanLink.N_allDominant line 30
7. lemma OAI.HyperbolicObstruction.FanLink.Q_allDominant line 35
8. lemma OAI.HyperbolicObstruction.FanLink.P_allDominant line 40
9. lemma OAI.HyperbolicObstruction.FanLink.active_allDominant line 46
10. lemma OAI.HyperbolicObstruction.FanLink.two_turns_le line 49
11. lemma OAI.HyperbolicObstruction.FanLink.triangle_only_four line 60

    Source documentation

    A full triangle-only normalized fan link has at least four steps. The normality condition rules out immediate reversal of the same indexed triangle; the fan's bipartition rules out odd circuits.

    lemma triangle_only_four (next : Equiv.Perm V) (line : V → Bool) [Nonempty V]
        (hbip : ∀ i, line i ≠ line (next i))
        (hback : ∀ i, next (next i) ≠ i) : 4 ≤ Fintype.card V := by
    …

12. theorem OAI.HyperbolicObstruction.FanLink.full_instance_bound line 86

    Source documentation

    The full-link inequality in the r-dominant case. The assumptions are only the ordinary indexed-side normality and the fan's bipartition, not a pre-assumed apex or isoperimetric inequality.

    theorem full_instance_bound (next : Equiv.Perm V) (s : V → State) (line : V → Bool)
        [Nonempty V] (hfull : ∀ i, (s i).active = true)
        (hfix : ∀ i, next i ≠ i)
        (hbip : ∀ i, s i = triangle → line i ≠ line (next i))
        (hback : ∀ i, s i = triangle → s (next i) = triangle → next (next i) ≠ i) :
        (4 : ℝ) - 2 * T s ≤ (Q s : ℝ) + P next s line := by
    …

    Mentions: OAI.HyperbolicObstruction.FanLink.State, OAI.HyperbolicObstruction.FanLink.T, OAI.HyperbolicObstruction.FanLink.Q, OAI.HyperbolicObstruction.FanLink.P