Compact-cell counting ledgers

The counting infrastructure of the compact cell: a family of double-counting inequalities that bound the population of usable / suppressed degree-3 vertices by the total degree excess X = excessX plus explicit constants. These ledgers turn the compact cell into a search bounded in n for each fixed excess.

Main results

• sfb_forces_sharing, no_two_saturated_deg6 — on the SeaFatBoundary, a pair of clean same-count hubs is forced to share ≥ 3 twins, and two saturated degree-6 hubs would build a forbidden good K_{2,3}.
• mIncidence_le_two, medge_endpoint_card_le — the global cap on the degree-3–degree-3 adjacency mass.
• anchored_sharing_count, class_cap_with_adj — the anchored twin-sharing double count σ₀·(|T| − 1) ≤ 2a and the class cap |T| ≤ 1 + i₀ + 2a.
• w1_of_unblocked_eq_twins, w1_of_unblocked_pad_supply — the far-pad supply discharging the W1 firing bridge.
• The suppressed-vertex ledgers 3·#S ≤ Σ_{deg ≥ 4} |hubTwins| etc., weighted_heavy_ledger (3/2)·#S ≤ Σ_{deg ≥ 5} σ·|hubTwins|, and their absorption suppressed_card_le (3/2)·#S ≤ (4/3)·X + 5703.
• usable_deg3_pair_coverage — the pair-coverage inequality on the usable degree-3 set.
• mid_leaves_card_le / mid_leaves_card_le_sharp (|L₈| ≤ 143, sharpened to 108), mid_usable5_card_le, and the splits usable_deg3_split_mid, w5_card_split isolating the big-neighbour cloud classes.

The Sea-Fat-Boundary sharing law and the K₂,₃ bridge

On the SeaFatBoundary (every hub pair DS-blocked, dsValue ≥ 5), a pair of same-count hubs with zero internal degree, zero mCross and no adjacency shares ≥ 3 twins (sfb_forces_sharing); two saturated degree-6 hubs with independent shared twins would assemble a good K_{2,3} (Σ₅deg = 21), contradicting no_good_K23 (no_two_saturated_deg6).

theorem ACMax.card_hubTwins_add_intDeg {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g : V) : (hubTwins G g).card + intDeg G g = G.degree g

Partition of N(g) by deg3Set-membership: |D3(g)| + i(g) = deg g.

theorem ACMax.privTwins_card_eq {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) : (privTwins G g h).card + (sharedTwins G g h).card = (hubTwins G g).card

Partition of D3(g) by D3(h)-membership: p(g,h) + s(g,h) = |D3(g)|.

A global cap on the M-incidence count

In the residual core the degree-3–degree-3 adjacency mass is globally bounded by a constant: mIncidence_le_two (mIncidence G ≤ 2 under the block-law matching), medge_endpoint_card_le_two (at most 2 degree-3 M-edge endpoints) and medge_endpoint_hub_card_le_four (at most 4 hubs own an M-endpoint twin). The constants are deliberately crude; only their existence matters downstream.

theorem ACMax.mIncidence_eq (n : ℕ) (G : SimpleGraph (Fin n)) : mIncidence G = ∑ v ∈ deg3Set G, (G.neighborFinset v ∩ deg3Set G).card

mIncidence written with the ambient decidability instances of Fin n (bridging the Classical instances baked into the definition over an abstract vertex type).

theorem ACMax.mem_hubTwins_adj {V : Type u_1} [Fintype V] {G : SimpleGraph V} {g v : V} : v ∈ hubTwins G g ↔ G.Adj g v ∧ G.degree v = 3

Membership in hubTwins, stated over a general vertex type so that the classical decidability instances inside the definition match those synthesised in the proof.

theorem ACMax.mIncidence_le_two (n : ℕ) (G : SimpleGraph (Fin n)) (huniq : ∀ (t₁ t₂ t₃ t₄ : Fin n), G.Adj t₁ t₂ → G.Adj t₃ t₄ → G.degree t₁ = 3 → G.degree t₂ = 3 → G.degree t₃ = 3 → G.degree t₄ = 3 → {t₁, t₂} = {t₃, t₄}) : mIncidence G ≤ 2

The incidence collapse: when all M-edges coincide, the incidence count is at most 2 — the two endpoints of the single edge.

theorem ACMax.medge_endpoint_card_le_two (n : ℕ) (G : SimpleGraph (Fin n)) (huniq : ∀ (t₁ t₂ t₃ t₄ : Fin n), G.Adj t₁ t₂ → G.Adj t₃ t₄ → G.degree t₁ = 3 → G.degree t₂ = 3 → G.degree t₃ = 3 → G.degree t₄ = 3 → {t₁, t₂} = {t₃, t₄}) : {t ∈ deg3Set G | ∃ (t' : Fin n), G.Adj t t' ∧ G.degree t' = 3}.card ≤ 2

M-endpoints under the dichotomy: at most 2.

theorem ACMax.medge_endpoint_hub_card_le_four (n : ℕ) (G : SimpleGraph (Fin n)) (_h : ResidualCore n G) (huniq : ∀ (t₁ t₂ t₃ t₄ : Fin n), G.Adj t₁ t₂ → G.Adj t₃ t₄ → G.degree t₁ = 3 → G.degree t₂ = 3 → G.degree t₃ = 3 → G.degree t₄ = 3 → {t₁, t₂} = {t₃, t₄}) : {g : Fin n | 4 ≤ G.degree g ∧ ∃ t ∈ hubTwins G g, ∃ (t' : Fin n), G.Adj t t' ∧ G.degree t' = 3}.card ≤ 4

Endpoint hubs under the dichotomy: at most 4.

The anchored twin-sharing double count

Fix a class T of clean same-count hubs on the SeaFatBoundary. Anchoring at g₀ ∈ T and counting shared-twin incidences I = #{(t, h) : h ∈ T∖{g₀}, t ∈ sharedTwins g₀ h} gives σ₀·(|T| − 1) ≤ I ≤ 2a (anchored_sharing_count), where each pair shares ≥ σ₀ twins (sfb_forces_sharing_of_intDeg_le, with σ₀ = 3 − i₀ under intDeg ≤ i₀) and each twin is adjacent to ≤ 2 members.

theorem ACMax.anchored_sharing_count {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) (g₀ : V) (T : Finset V) (σ₀ a : ℕ) (hshare : ∀ h ∈ T.erase g₀, σ₀ ≤ (sharedTwins G g₀ h).card) (ha : (hubTwins G g₀).card = a) (h3T : ∀ t ∈ hubTwins G g₀, G.degree t = 3) : σ₀ * (T.erase g₀).card ≤ 2 * a

The anchored double count. If every member of T \ {g₀} shares at least σ₀ twins with the anchor g₀, whose twin set has size a and consists of degree-3 vertices, then σ₀·|T \ {g₀}| ≤ 2a: counting incidences (t, h) with t ∈ sharedTwins g₀ h, each h contributes ≥ σ₀, while each twin t has only |N(t)| = 3 slots, one of which is g₀ itself — so t serves at most 2 members.

The saturated class cap (intDeg = 0)

The general interaction version (intDeg ≤ i₀, 2·i₀ < 5)

theorem ACMax.sfb_forces_sharing_of_intDeg_le {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hb : SeaFatBoundary G) (g h : V) (i₀ : ℕ) (hne : g ≠ h) (hg4 : 4 ≤ G.degree g) (hh4 : 4 ≤ G.degree h) (heq : (hubTwins G g).card = (hubTwins G h).card) (hig : intDeg G g ≤ i₀) (hih : intDeg G h ≤ i₀) (hmx : mCross G g h = 0) (hadj : ¬G.Adj g h) : 3 - i₀ ≤ (sharedTwins G g h).card

Forced sharing at internal degree ≤ i₀. On the SeaFatBoundary, a nonadjacent equal-twin-count hub pair with intDeg ≤ i₀ each and mCross = 0 shares at least 3 − i₀ twins: the gap terms of dsValue cancel, so 5 ≤ i(g) + i(h) + 2s ≤ 2i₀ + 2s, and since 5 − 2i₀ is odd, s ≥ ⌈(5 − 2i₀)/2⌉ = 3 − i₀.

Pad supply for the W1 firing bridge

Two ways to discharge the far-pad requirement of w1Config_of_pair: w1_of_unblocked_eq_twins (gap-0: equal private-twin counts, empty pad set) and w1_of_unblocked_pad_supply (pad supply: when the degree-3 supply exceeds the two twin counts by 20, the forbidden pads number at most |D3(g)| + |D3(h')| + 16, leaving ≥ 4 ≥ gap far pads).

theorem ACMax.w1_of_unblocked_eq_twins {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) (hg4 : 4 ≤ G.degree g) (hh4 : 4 ≤ G.degree h) (hne : g ≠ h) (heq : (privTwins G g h).card = (privTwins G h g).card) (hds : dsValue G g h ≤ 4) : W1Config G

Gap-0 firing: a DS-unblocked hub pair with equal private-twin counts is a W1 configuration — the empty pad set closes the count.

The anchor bound and the suppressed ledgers

Anchor bound: on the compact cell every usable vertex lies in the radius-3 ball around a usable degree-3 anchor t, so #{v : deg v = 3, sigS v ≤ 2} ≤ 1 + |hubTwins t| + Σ_{x∈N(t)} |hubTwins x| + Σ_{x∈N(t)} Σ_{y∈N(x)} |hubTwins y|. Suppressed ledgers: a suppressed vertex (deg = 3, sigS > 2) has, by nonusable_deg3_structure, 3 hub neighbours, 2 of degree ≥ 5 and 1 of degree ≥ 6; double-counting gives 3·#S ≤ Σ_{deg ≥ 4} |hubTwins|, 2·#S ≤ Σ_{deg ≥ 5} |hubTwins|, #S ≤ Σ_{deg ≥ 6} |hubTwins|.

hubTwins as a degree filter (generic V, keeping the classical

instances of GeneralDoubleStar stable)

theorem ACMax.mem_hubTwins_iff {V : Type u_1} [Fintype V] {G : SimpleGraph V} {g v : V} : v ∈ hubTwins G g ↔ G.Adj g v ∧ G.degree v = 3

Membership in hubTwins: a hub twin of g is a degree-3 neighbour.

The weighted heavy ledger

A σ-weighted refinement of the suppressed ledgers. A suppressed vertex has at most one degree-4 neighbour (contributing σ(4) = 1/2), so the σ-mass from heavy (degree ≥ 5) neighbours is ≥ 3/2 (heavy_sigma_into_suppressed); summing and swapping the double count gives the weighted heavy ledger (3/2)·#S ≤ Σ_{deg w ≥ 5} σ(deg w)·|hubTwins w|.

The integer-profile sharpening: 3/2 → 32/21

theorem ACMax.sigma_pair_gap {d₁ d₂ : ℕ} (h₁ : 5 ≤ d₁) (h₂ : 5 ≤ d₂) (h : 3 / 2 < sigma d₁ + sigma d₂) : 32 / 21 ≤ sigma d₁ + sigma d₂

The σ-value pair gap. Two heavy σ-values summing strictly above 3/2 sum to at least 32/21: the σ-value set {2/3, 3/4, 4/5, 5/6, 6/7, …} is discrete, so the sum cannot approach 3/2 from above — the minimum is the (5, 9)-profile 2/3 + 6/7 = 32/21.

theorem ACMax.heavy_sigma_into_suppressed_sharp {n : ℕ} (G : SimpleGraph (Fin n)) (t : Fin n) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hd : G.degree t = 3) (hs : 2 < sigS G t) : 32 / 21 ≤ ∑ w ∈ G.neighborFinset t with 5 ≤ G.degree w, sigma (G.degree w)

Sharp heavy σ-inflow (integer profile). A suppressed vertex receives σ-mass at least 32/21 from its heavy neighbours: with a degree-4 neighbour present, the remaining two heavy σ-values sum strictly above 3/2, hence to at least 32/21 by the pair gap; with no degree-4 neighbour the heavy sum already exceeds 2.

theorem ACMax.weighted_heavy_ledger_sharp {n : ℕ} (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) : 32 / 21 * ↑{v : Fin n | G.degree v = 3 ∧ 2 < sigS G v}.card ≤ ∑ w : Fin n with 5 ≤ G.degree w, sigma (G.degree w) * ↑(hubTwins G w).card

The sharp weighted heavy ledger (integer-profile demand):

(32/21)·#suppressed ≤ Σ_{deg w ≥ 5} σ(deg w)·|hubTwins w|.

The D1 summation: the heavy ledger absorbed by the excess

The σ-weighted heavy sum Σ_{deg w ≥ 5} σ(deg w)·|hubTwins w| is at most (4/3)·X + 5703 (X = excessX), via a three-way partition of the heavy set: parts A (a + 3 ≤ d) and B (d ≥ 13) absorb into (4/3)·excessX by the pointwise sigma_mul_le_four_thirds; the capped part C (5 ≤ d ≤ 12) is bounded in cardinality by the adjacency-tolerant class cap class_cap_with_adj (|T| ≤ 1 + i₀ + 2a ≤ 27, anchoring the double count with σ₀ = 1), giving |C| ≤ 528 and Σ_C ≤ 5703. Chaining with weighted_heavy_ledger yields suppressed_card_le : (3/2)·#S ≤ (4/3)·excessX + 5703.

Small vocabulary lemmas

theorem ACMax.hubTwins_card_le_degree {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g : V) : (hubTwins G g).card ≤ G.degree g

The twin count never exceeds the degree: |D3(g)| ≤ deg g.

theorem ACMax.exists_cross_edge_of_mCross_ne_zero {V : Type u_1} [Fintype V] (G : SimpleGraph V) (g h : V) (hmx : mCross G g h ≠ 0) : ∃ t ∈ privTwins G g h, ∃ t' ∈ privTwins G h g, G.Adj t t'

A nonzero mCross produces an explicit cross edge: a private twin t of g against h adjacent to a private twin t' of h against g.

The adjacency-tolerant class cap

theorem ACMax.class_cap_with_adj (n : ℕ) (G : SimpleGraph (Fin n)) (hb : SeaFatBoundary G) (a i₀ : ℕ) (hi : i₀ ≤ 2) (T : Finset (Fin n)) (hT : ∀ g ∈ T, 4 ≤ G.degree g ∧ intDeg G g ≤ i₀ ∧ (hubTwins G g).card = a) (hmx : ∀ g ∈ T, ∀ h ∈ T, g ≠ h → mCross G g h = 0) : T.card ≤ 1 + i₀ + 2 * a

Adjacency-tolerant class cap. On the SeaFatBoundary, a class T of hubs with deg ≥ 4, intDeg ≤ i₀ ≤ 2, the same twin count a, and vanishing pairwise mCross satisfies |T| ≤ 1 + i₀ + 2a: anchored at any g₀ ∈ T, at most i₀ partners are adjacent to g₀ (they are non-degree-3 neighbours) and at most 2a are nonadjacent (each shares ≥ 3 − i₀ ≥ 1 twins with g₀, and each of g₀'s a twins serves at most 2 partners).

The capped-part cardinality bound

The D1 summation

Corollary: the suppressed set is absorbed by the excess

Pair coverage of usable degree-3 vertices

On the compact cell two distinct usable vertices must be adjacent, share a neighbour, or carry an edge between their neighbourhoods (else they form a usable far pair). Double-counting the ordered pairs of U₃ = {v : deg v = 3 ∧ sigS v ≤ 2} by mechanism yields usable_deg3_pair_coverage: |U₃|·(|U₃|−1) ≤ mIncidence G + Σ_w a(w)(a(w)−1) + Σ_w Σ_{w'∈N(w)} a(w)·a(w'), with a(w) = |hubTwins G w|.

theorem ACMax.usable_pair_mechanism {n : ℕ} (G : SimpleGraph (Fin n)) (hcpt : ¬HasUsableFarPair G) (t t' : Fin n) (hne : t ≠ t') (ht : sigS G t ≤ 2) (ht' : sigS G t' ≤ 2) : G.Adj t t' ∨ (∃ (w : Fin n), G.Adj t w ∧ G.Adj t' w) ∨ ∃ (w : Fin n) (w' : Fin n), G.Adj t w ∧ G.Adj t' w' ∧ G.Adj w w'

On the compact cell (¬HasUsableFarPair), two distinct usable vertices are adjacent, share a common neighbour, or carry an edge between their neighbourhoods: the negation of all three would exhibit a usable clean far pair.

The mid-leaves Moore bound (Δ ≤ 8)

On the compact cell the set of mid leaves L₈ = {u : deg u = 3 ∧ sigS u ≤ 2 ∧ every neighbour has deg ≤ 8} has at most 143 elements — the Δ = 8 Moore bound. Fixing one mid leaf u₀, every usable vertex is adjacent to u₀, shares a neighbour, or sits at the far end of an edge out of N(u₀) through a ≤ 8-degree middle vertex, so L₈ sits in a parent-erased radius-2 ball of volume ≤ 1 + 1 + 3·5 + 21·6 = 143. The corollary usable_deg3_split_mid splits the usable degree-3 count into this mid part and the big-neighbour (deg ≥ 9) population, whose partners are degree-≤ 4 by usable_twin_partners_deg_le_four.

The mid-usable Moore bound and the W₅ split

The W₅ class (usable degree-5 hubs with exactly two twins) splits by its heaviest neighbour: the all-neighbours-≤ 8 part is Moore-bounded by 1 + 5 + 5·7 + 5·7·7 = 286 (mid_usable5_card_le), and the remainder is the big-hub cloud class W₅ᵇ. w5_card_split records N₅ ≤ 286 + N₅ᵇ.

theorem ACMax.mid_usable5_card_le (n : ℕ) (G : SimpleGraph (Fin n)) (hcpt : ¬HasUsableFarPair G) : {u : Fin n | G.degree u = 5 ∧ sigS G u ≤ 2 ∧ (hubTwins G u).card = 2 ∧ ∀ x ∈ G.neighborFinset u, G.degree x ≤ 8}.card ≤ 206

Mid-usable Moore bound. On the compact cell, the set of degree-5 usable vertices all of whose neighbours have degree ≤ 8 has at most 286 elements: every member mediates with a fixed member u₀ within the parent-erased ball 1 + 5 + 5·7 + 5·7·7 = 286 around u₀.

theorem ACMax.w5_card_split (n : ℕ) (G : SimpleGraph (Fin n)) (hcpt : ¬HasUsableFarPair G) : ↑{w : Fin n | G.degree w = 5 ∧ sigS G w ≤ 2 ∧ (hubTwins G w).card = 2}.card ≤ 206 + ↑{w : Fin n | G.degree w = 5 ∧ sigS G w ≤ 2 ∧ (hubTwins G w).card = 2 ∧ ∃ x ∈ G.neighborFinset w, 9 ≤ G.degree x}.card

The W₅ split: the usable degree-5 two-twin class is covered by the mid-usable Moore class together with the big-hub cloud class W₅ᵇ:

N₅ ≤ 206 + N₅ᵇ.

The sharpened mid-leaves Moore bound

Sharpens |L₈| ≤ 143 to |L₈| ≤ 108. Since the base mid leaf u₀ is itself usable, Σσ_{u₀} = σ(d₁) + σ(d₂) + σ(d₃) ≤ 2 caps the neighbour-degree sum d₁ + d₂ + d₃ ≤ 19 (maximiser {8,8,3}). As the two expansion layers grow linearly in the neighbour degrees, the ball volume is 1 + 1 + Σ(dᵢ − 3) + Σ 6(dᵢ − 1) = 7·Σdᵢ − 25 ≤ 108 (mid_leaves_card_le_sharp). usable_deg3_split_mid_sharp is the drop-in split (extra min degree ≥ 3 hypothesis, from ResidualCore.min_degree).

theorem ACMax.sigma_deg_triple_sum_le {da db dc : ℕ} (ha3 : 3 ≤ da) (ha8 : da ≤ 8) (hb3 : 3 ≤ db) (hb8 : db ≤ 8) (hc3 : 3 ≤ dc) (hc8 : dc ≤ 8) (hs : sigma da + sigma db + sigma dc ≤ 2) : da + db + dc ≤ 19

The σ integer program. Three neighbour degrees in [3,8] whose slot values sum to ≤ 2 have degree sum ≤ 19 — the {8,8,3} maximiser (σ = 5/6+5/6+0 = 5/3). {8,8,4} already costs 13/6 > 2.

theorem ACMax.nbr_deg_sum_le_nineteen (n : ℕ) (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (u : Fin n) (hdeg : G.degree u = 3) (hsig : sigS G u ≤ 2) (hmid : ∀ x ∈ G.neighborFinset u, G.degree x ≤ 8) : ∑ x ∈ G.neighborFinset u, G.degree x ≤ 19

The neighbour-degree cap. A usable degree-3 vertex u (sigS u ≤ 2) whose neighbours all have degree ≤ 8, in a graph of minimum degree ≥ 3, has neighbour-degree sum ≤ 19.

theorem ACMax.mid_leaves_card_le_sharp (n : ℕ) (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hcpt : ¬HasUsableFarPair G) (hblk : ∀ (w : Fin n), G.degree w ≤ 15 → (hubTwins G w).card + 2 ≤ G.degree w) : {u : Fin n | G.degree u = 3 ∧ sigS G u ≤ 2 ∧ ∀ x ∈ G.neighborFinset u, G.degree x ≤ 8}.card ≤ 108

Sharpened mid-leaves Moore bound. On the compact cell, in a graph of minimum degree ≥ 3, the set of degree-3 usable vertices all of whose neighbours have degree ≤ 8 has at most 108 elements.

theorem ACMax.usable_deg3_split_mid_sharp (n : ℕ) (G : SimpleGraph (Fin n)) (h3 : ∀ (v : Fin n), 3 ≤ G.degree v) (hcpt : ¬HasUsableFarPair G) (hblk : ∀ (w : Fin n), G.degree w ≤ 15 → (hubTwins G w).card + 2 ≤ G.degree w) : {u : Fin n | G.degree u = 3 ∧ sigS G u ≤ 2}.card ≤ 108 + {u : Fin n | G.degree u = 3 ∧ sigS G u ≤ 2 ∧ ∃ x ∈ G.neighborFinset u, 9 ≤ G.degree x}.card

The usable degree-3 set splits into the sharpened mid part (≤ 108 on the compact cell, min degree ≥ 3) and the vertices carrying a big (deg ≥ 9) neighbour. Drop-in replacement for usable_deg3_split_mid with the improved constant.