OAI/Geometry/HyperbolicGroups/Template.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Edge line 15

   Source documentation

   All incidences except Y_D--CD. Both sides have fixed named positions.

   abbrev Edge := {p : Fin 11 × Fin 7 // Incident (pointOfRepresentative p.1) p.2 ∧ p ≠ (10,4)}

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Incident, OAI.HyperbolicObstruction.IncidenceTemplate.pointOfRepresentative

2. def OAI.HyperbolicObstruction.IncidenceTemplate.isLoose line 17
3. instance OAI.HyperbolicObstruction.IncidenceTemplate.(instance at line 19) line 19
4. def OAI.HyperbolicObstruction.IncidenceTemplate.fan line 21
5. lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_edges line 24
6. lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_fan line 26
7. def OAI.HyperbolicObstruction.IncidenceTemplate.code line 28
8. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.TwoPath line 31

   Source documentation

   One canonical orientation of each unoriented nonbacktracking two-edge path.

   abbrev TwoPath := {p : Edge × Edge // code p.1 < code p.2 ∧
   …

   Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Edge, OAI.HyperbolicObstruction.IncidenceTemplate.code

9. lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_twoPaths line 34
10. abbrev OAI.HyperbolicObstruction.IncidenceTemplate.Field line 36
11. instance OAI.HyperbolicObstruction.IncidenceTemplate.instFieldDecidableEq line 38
12. lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_fields line 40
13. lemma OAI.HyperbolicObstruction.IncidenceTemplate.partition_per_edge line 45

    Source documentation

    The fan membership partition includes the unique loose edge separately.

    lemma partition_per_edge : ∀ e : Edge,
        (if isLoose e then 1 else 0) + (∑ i, if e ∈ fan i then 1 else 0) = (1 : ℕ) := by
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Edge, OAI.HyperbolicObstruction.IncidenceTemplate.isLoose, OAI.HyperbolicObstruction.IncidenceTemplate.fan

14. def OAI.HyperbolicObstruction.IncidenceTemplate.fanCount line 49
15. def OAI.HyperbolicObstruction.IncidenceTemplate.looseCount line 51
16. lemma OAI.HyperbolicObstruction.IncidenceTemplate.count_partition line 53
17. lemma OAI.HyperbolicObstruction.IncidenceTemplate.fanCount_le line 72
18. lemma OAI.HyperbolicObstruction.IncidenceTemplate.fanCount_eq_iff line 75
19. lemma OAI.HyperbolicObstruction.IncidenceTemplate.fan_card_lower line 85
20. def OAI.HyperbolicObstruction.IncidenceTemplate.fanScore line 90

    Source documentation

    Each fan retains two units of critical exponent even when fully charged.

    def fanScore (W : Finset Edge) (i : Fin 7) : ℤ :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Edge

21. lemma OAI.HyperbolicObstruction.IncidenceTemplate.fanScore_lower line 93
22. lemma OAI.HyperbolicObstruction.IncidenceTemplate.fanScore_nonneg line 105
23. def OAI.HyperbolicObstruction.IncidenceTemplate.coreExponent line 108
24. lemma OAI.HyperbolicObstruction.IncidenceTemplate.coreExponent_decompose line 112
25. lemma OAI.HyperbolicObstruction.IncidenceTemplate.coreExponent_univ line 119
26. lemma OAI.HyperbolicObstruction.IncidenceTemplate.min_sum_le_sum_min line 122
27. lemma OAI.HyperbolicObstruction.IncidenceTemplate.coreExponent_lower line 131
28. def OAI.HyperbolicObstruction.IncidenceTemplate.CoreAdmissible line 150

    Source documentation

    Admissibility of core-field sets, retaining the exact three/two quotas.

    def CoreAdmissible (S : Finset Edge) : Prop :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Edge

29. lemma OAI.HyperbolicObstruction.IncidenceTemplate.coreExponent_admissible line 153
30. def OAI.HyperbolicObstruction.IncidenceTemplate.squareSupport line 174

    Source documentation

    The four coordinates of a square row: two core fields and two private ones.

    def squareSupport (τ : TwoPath) : Finset Field :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.TwoPath, OAI.HyperbolicObstruction.IncidenceTemplate.Field

31. def OAI.HyperbolicObstruction.IncidenceTemplate.freshFields line 177
32. def OAI.HyperbolicObstruction.IncidenceTemplate.freshCount line 180
33. lemma OAI.HyperbolicObstruction.IncidenceTemplate.freshCount_le line 182
34. lemma OAI.HyperbolicObstruction.IncidenceTemplate.freshCount_eq_two_iff line 187
35. lemma OAI.HyperbolicObstruction.IncidenceTemplate.card_sum_prod line 195
36. lemma OAI.HyperbolicObstruction.IncidenceTemplate.count_split line 214
37. def OAI.HyperbolicObstruction.IncidenceTemplate.freshScore line 219
38. lemma OAI.HyperbolicObstruction.IncidenceTemplate.freshScore_nonneg line 222
39. lemma OAI.HyperbolicObstruction.IncidenceTemplate.twoPath_ne line 233
40. lemma OAI.HyperbolicObstruction.IncidenceTemplate.no_square_of_small_core line 239
41. lemma OAI.HyperbolicObstruction.IncidenceTemplate.coreExponent_small line 252
42. def OAI.HyperbolicObstruction.IncidenceTemplate.criticalExponent line 267
43. theorem OAI.HyperbolicObstruction.IncidenceTemplate.criticalExponent_lower line 271

    Source documentation

    Source Lemma sample:lem-budget, first inequality, for the actual template.

    theorem criticalExponent_lower (W : Finset Field) :
        ((min 2 W.card : ℕ) : ℤ) ≤ criticalExponent W := by
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.criticalExponent

44. def OAI.HyperbolicObstruction.IncidenceTemplate.Admissible line 290

    Source documentation

    Exact admissibility from Definition 2.3 of the manuscript.

    def Admissible (S : Finset Field) : Prop :=
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field

45. theorem OAI.HyperbolicObstruction.IncidenceTemplate.criticalExponent_admissible line 295

    Source documentation

    Source Lemma sample:lem-budget, the strengthened admissible-set budget.

    theorem criticalExponent_admissible (S W : Finset Field) (hS : Admissible S)
        (hSW : S ⊆ W) : (S.card : ℤ) ≤ criticalExponent W := by
    …

    Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.Admissible, OAI.HyperbolicObstruction.IncidenceTemplate.criticalExponent