The residual-core interface lemmas

Generic (n-free where possible) glue lemmas mediating between the residual-core open Classical in structure and the counting/covering layers. Here M = G[D] is the subgraph induced on the degree-3 set D, and iso twins are the M-isolated degree-3 vertices.

Main results

• each_iso_three_hubs_general — an M-isolated degree-3 vertex meets exactly the three hubs (4 ≤ deg).
• hub_iso_sum_general — the two-hub selection engine's core count ∑_{a∈Hub} |N(a) ∩ Iso| = 3·|Iso|.
• dist_le_three_of_mem_closeSet — the metric half of the compact-ball interface: every membership certificate for the radius-3 combinatorial ball closeSet G u₀ is a walk of length ≤ 3, so closeSet sits inside the graph-distance ball.
• s0_of_no_medge, deg3_eq_isoTwins_of_s0, twin_incidence_total — the e(M) = 0 normalization: with no degree-3–degree-3 edge, D is the iso-twin set and the twin incidence total is 3·|Iso|.

theorem ACMax.each_iso_three_hubs_general {V : Type u_1} [Fintype V] (G : SimpleGraph V) (D Hub : Finset V) (hmemD : ∀ (v : V), v ∈ D ↔ G.degree v = 3) (hmemHub : ∀ (v : V), v ∈ Hub ↔ 4 ≤ G.degree v) (h3 : ∀ (v : V), 3 ≤ G.degree v) (t : V) (htD : t ∈ D) (htiso : (G.neighborFinset t ∩ D).card = 0) : (G.neighborFinset t ∩ Hub).card = 3

B3 — Each M-isolated twin meets exactly three hubs. An M-isolated degree-3 twin t ((N t ∩ D).card = 0) has all three of its neighbours in Hub, so (N t ∩ Hub).card = 3.

The two-hub selection engine

Abstract Finset counting over given sets Hub, Iso: hub_iso_sum_general records ∑_{a∈Hub} |N(a) ∩ Iso| = 3·|Iso|, since each iso twin meets exactly three hubs.

theorem ACMax.hub_iso_sum_general {V : Type u_1} [Fintype V] (G : SimpleGraph V) (Hub Iso : Finset V) (hiso3 : ∀ t ∈ Iso, (G.neighborFinset t ∩ Hub).card = 3) : ∑ a ∈ Hub, (G.neighborFinset a ∩ Iso).card = 3 * Iso.card

Total iso-degree is 3·|Iso|. Each M-isolated twin meets exactly three hubs.

The closeSet → dist bound

The metric half of the compact-ball interface: every membership certificate for the radius-3 combinatorial ball closeSet G u₀ is a walk of length ≤ 3, so closeSet sits inside the graph-distance ball of radius 3 around u₀.

theorem ACMax.dist_le_three_of_mem_closeSet {n : ℕ} (G : SimpleGraph (Fin n)) (u₀ v : Fin n) (hv : v ∈ closeSet G u₀) : G.dist u₀ v ≤ 3

A closeSet member is within distance 3. Every vertex of the radius-3 combinatorial ball closeSet G u₀ is at graph distance ≤ 3 from u₀; each membership certificate is a walk of length ≤ 3. No connectivity is needed.

The e(M) = 0 normalization

The normalization leaves for the e(M) = 0 case: s0_of_no_medge pushes the absence of a degree-3–degree-3 edge into the pointwise hs0 form, deg3_eq_isoTwins_of_s0 shows the degree-3 set then coincides with the iso-twin set, and twin_incidence_total records the resulting incidence total ∑_{h∈Hub} |N(h) ∩ Iso| = 3·|Iso|.

theorem ACMax.s0_of_no_medge {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h : ¬∃ (v : V) (w : V), G.degree v = 3 ∧ G.degree w = 3 ∧ G.Adj v w) (v w : V) : G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w

B-0a (push). The negation of a degree-3–degree-3 edge, in the pointwise hs0 form the downstream e(M) = 0 fight consumes.

theorem ACMax.deg3_eq_isoTwins_of_s0 {V : Type u_1} [Fintype V] (G : SimpleGraph V) (hs0 : ∀ (v w : V), G.degree v = 3 → G.degree w = 3 → ¬G.Adj v w) : deg3Set G = isoTwins G

B-0a (identification). Under hs0 (no degree-3–degree-3 adjacency) every degree-3 vertex is M-isolated, so the degree-3 set coincides with the M-isolated twin set: deg3Set G = isoTwins G. The forward inclusion is the (a)-step hsub of xmz_pigeonhole_input; the reverse is the definitional isoTwins ⊆ deg3Set.

theorem ACMax.twin_incidence_total {V : Type u_1} [Fintype V] (G : SimpleGraph V) (h3 : ∀ (v : V), 3 ≤ G.degree v) : ∑ h ∈ hubSet G, (G.neighborFinset h ∩ isoTwins G).card = 3 * (isoTwins G).card

B-0c. The twin-incidence total. Under hs0 (e(M) = 0) and minimum degree 3 each M-isolated twin meets exactly three hubs (each_iso_three_hubs_general), so the hub-to-twin incidence sum is 3·|Iso| (hub_iso_sum_general): ∑_{h∈Hub} |N(h) ∩ Iso| = 3·|Iso|. This is the exact shape the B1 residue fights (e.g. the single-heavy budget xmz_single5_budget) consume; the banked hub_iso_sum_general already carries this statement for given Hub, Iso, and this leaf supplies its per-twin hypothesis directly from the definition of isoTwins (whose members are intrinsically M-isolated), so only minimum degree 3 is needed here — the hs0 e(M) = 0 hypothesis of the surrounding node is what identifies |Iso| = n₃ upstream (deg3_eq_isoTwins_of_s0), not this incidence identity.