Proof of `Stable hubbed comb in a critical graph`
groundedproofs/Lax54Proofs/KeyCombLemma.lean · lax-54
What this proof establishes
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Proof of Lemma 3.1. Decompose the prescribed vertex set into the critical layers used in the paper and apply the bipartite comb lemma to each layer. If no layer yields a comb, normalized estimates for the hubs, their neighborhoods, and the covered residual sets contradict the partition identity.