OAI/Geometry/HyperbolicGroups/CyclicLink.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Finite cyclic-link counting used at the literal fan apices. No planarity, normal-form, or diagram conclusions are postulated here.

  1. inductive OAI.HyperbolicObstruction.FanLink.State line 16
  2. def OAI.HyperbolicObstruction.FanLink.State.active line 22
  3. def OAI.HyperbolicObstruction.FanLink.State.d line 26
  4. def OAI.HyperbolicObstruction.FanLink.State.n line 30
  5. def OAI.HyperbolicObstruction.FanLink.State.f line 34
  6. def OAI.HyperbolicObstruction.FanLink.State.turn line 38
  7. def OAI.HyperbolicObstruction.FanLink.State.bit line 42
  8. def OAI.HyperbolicObstruction.FanLink.State.boundary line 44
  9. lemma OAI.HyperbolicObstruction.FanLink.State.endpoint_bound line 46
  10. lemma OAI.HyperbolicObstruction.FanLink.State.fan_partition line 53
  11. def OAI.HyperbolicObstruction.FanLink.D line 63
  12. def OAI.HyperbolicObstruction.FanLink.N line 64
  13. def OAI.HyperbolicObstruction.FanLink.Q line 65
  14. def OAI.HyperbolicObstruction.FanLink.P line 66
  15. def OAI.HyperbolicObstruction.FanLink.B line 68
  16. theorem OAI.HyperbolicObstruction.FanLink.dominant_endpoint_bound line 75

    Source documentation

    Direct endpoint charging proves the dominant-turn bound. A selected triangle has one line endpoint. A nonline endpoint of a top turn incurs its exceptional loose-side payment. No two dominant turns share a radial side. This works even before the five-step bound and allows any selection of steps.

    theorem dominant_endpoint_bound (next : Equiv.Perm V) (s : V → State) (line : V → Bool)
    (hcancel : ∀ i, ¬ (s i = dominant ∧ s (next i) = dominant))
    (hbip : ∀ i, s i = triangle → line i ≠ line (next i)) :
    2 * D s ≤ 2 * N s + Q s + P next s line + B next s := by
…

    Mentions: OAI.HyperbolicObstruction.FanLink.State, OAI.HyperbolicObstruction.FanLink.D, OAI.HyperbolicObstruction.FanLink.N, OAI.HyperbolicObstruction.FanLink.Q, OAI.HyperbolicObstruction.FanLink.P, OAI.HyperbolicObstruction.FanLink.B

  17. def OAI.HyperbolicObstruction.FanLink.IsCyclic line 97

    Source documentation

    One connected cyclic order, including the one-element cycle.

    def IsCyclic (next : Equiv.Perm V) : Prop :=
…
  18. def OAI.HyperbolicObstruction.FanLink.enter line 100
  19. def OAI.HyperbolicObstruction.FanLink.leave line 101
  20. lemma OAI.HyperbolicObstruction.FanLink.transition_balance line 103
  21. lemma OAI.HyperbolicObstruction.FanLink.transition_split line 106
  22. lemma OAI.HyperbolicObstruction.FanLink.total_balance line 110
  23. lemma OAI.HyperbolicObstruction.FanLink.boundary_eq_twice line 118
  24. lemma OAI.HyperbolicObstruction.FanLink.boundary_le_four line 122
  25. lemma OAI.HyperbolicObstruction.FanLink.selected_of_no_leave line 141
  26. lemma OAI.HyperbolicObstruction.FanLink.partial_boundary line 150
  27. theorem OAI.HyperbolicObstruction.FanLink.dominant_partial_bound line 172

    Source documentation

    Source's four-unit error for a represented partial link of at most five steps, derived from endpoint charging and actual cyclic transitions.

    theorem dominant_partial_bound (next : Equiv.Perm V) (s : V → State) (line : V → Bool)
    (hcancel : ∀ i, ¬ (s i = dominant ∧ s (next i) = dominant))
    (hbip : ∀ i, s i = triangle → line i ≠ line (next i))
    (hcard : Fintype.card V ≤ 5) :
    2 * D s ≤ 2 * N s + Q s + P next s line + 4 := by
…

    Mentions: OAI.HyperbolicObstruction.FanLink.State, OAI.HyperbolicObstruction.FanLink.D, OAI.HyperbolicObstruction.FanLink.N, OAI.HyperbolicObstruction.FanLink.Q, OAI.HyperbolicObstruction.FanLink.P

  28. lemma OAI.HyperbolicObstruction.FanLink.boundary_full line 180