OAI/Geometry/HyperbolicGroups/WeightedCoincidence.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.Coincidence.rankOn line 17

   Source documentation

   Coincidence rank on an actual subset of field positions.

   def rankOn (c : V → C) (s : Finset V) : ℕ := s.card - (s.image c).card

2. def OAI.HyperbolicObstruction.Coincidence.maxRepresentative line 20

   Source documentation

   A maximum-weight representative of each nonempty unsigned class.

   def maxRepresentative (c : V → C) (w : V → ℕ) (v : V) : V :=
   …

3. lemma OAI.HyperbolicObstruction.Coincidence.maxRepresentative_mem line 24
4. lemma OAI.HyperbolicObstruction.Coincidence.le_maxRepresentative line 30
5. lemma OAI.HyperbolicObstruction.Coincidence.maxRepresentative_eq line 35
6. lemma OAI.HyperbolicObstruction.Coincidence.maxRepresentative_idem line 43
7. lemma OAI.HyperbolicObstruction.Coincidence.rank_level line 51

   Source documentation

   The representative/nonrepresentative partition computes rank at every level. A maximal position remains selected whenever any class member does.

   lemma rank_level (c : V → C) (w : V → ℕ) (j : ℕ) :
       rankOn c (Finset.univ.filter (fun v => j < w v)) =
         (Finset.univ.filter (fun v => j < w v ∧ v ≠ maxRepresentative c w v)).card := by
   …

   Mentions: OAI.HyperbolicObstruction.Coincidence.rankOn, OAI.HyperbolicObstruction.Coincidence.maxRepresentative

8. lemma OAI.HyperbolicObstruction.Coincidence.layer_cake line 85
9. theorem OAI.HyperbolicObstruction.Coincidence.sum_rank_levels line 100

   Source documentation

   Exact integer layer-cake identity.

   theorem sum_rank_levels (c : V → C) (w : V → ℕ) (K : ℕ) (hK : ∀ v, w v ≤ K) :
       ∑ j ∈ Finset.range K, rankOn c (Finset.univ.filter (fun v => j < w v)) =
         ∑ v ∈ Finset.univ.filter (fun v => v ≠ maxRepresentative c w v), w v := by
   …

   Mentions: OAI.HyperbolicObstruction.Coincidence.rankOn, OAI.HyperbolicObstruction.Coincidence.maxRepresentative

10. def OAI.HyperbolicObstruction.Coincidence.contactCharge line 113

    Source documentation

    Each letter contact is charged to an endpoint other than the class maximum. This uses actual side capacities, not a forest assumption on the contact graph.

    def contactCharge (c : V → C) (w : V → ℕ) (l r : E → V) (e : E) : V :=
    …

11. lemma OAI.HyperbolicObstruction.Coincidence.contactCharge_endpoint line 116
12. lemma OAI.HyperbolicObstruction.Coincidence.contactCharge_not_max line 121
13. theorem OAI.HyperbolicObstruction.Coincidence.contacts_le_weighted_rank line 135

    Source documentation

    The contact bound, valid for arbitrary cycles, multiple edges and repeats of cell copies. Normality is precisely the inequality of the two field indices.

    theorem contacts_le_weighted_rank (c : V → C) (w : V → ℕ) (l r : E → V)
        (hneq : ∀ e, l e ≠ r e) (hc : ∀ e, c (l e) = c (r e))
        (hcap : ∀ v, (Finset.univ.filter (fun e => l e = v ∨ r e = v)).card ≤ w v)
        (K : ℕ) (hK : ∀ v, w v ≤ K) :
        Fintype.card E ≤ ∑ j ∈ Finset.range K,
          rankOn c (Finset.univ.filter (fun v => j < w v)) := by
    …

    Mentions: OAI.HyperbolicObstruction.Coincidence.rankOn