Heavy-degree census lemmas

Two elementary set-counting facts used by the exact Moore argument on 48 ≤ n ≤ 122. They were first proved inside the former island-band development; this neutral module keeps the active proof independent of that historical assembly.

theorem ACMax.heavy_class_ledger {n : ℕ} (G : SimpleGraph (Fin n)) (hn : 48 ≤ n) : {v : Fin n | 5 ≤ G.degree v}.card + {h ∈ hubSet G | 6 ≤ G.degree h ∧ ¬n + 15 < 9 * G.degree h}.card + 3 * {h ∈ hubSet G | n + 15 < 9 * G.degree h}.card ≤ excessX n G

The total degree excess dominates the heavy vertices, with additional weights for non-giant degree-6 hubs and giant hubs.

theorem ACMax.heavy_class_disjoint {n : ℕ} (G : SimpleGraph (Fin n)) (hn : 48 ≤ n) : {h ∈ hubSet G | 6 ≤ G.degree h ∧ ¬n + 15 < 9 * G.degree h}.card + {h ∈ hubSet G | n + 15 < 9 * G.degree h}.card ≤ {v : Fin n | 5 ≤ G.degree v}.card

The non-giant degree-6 hubs and giant hubs are disjoint subsets of the heavy vertices.