Draft — mutable and not usable as a dependency; its citation marks the draft state.

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.

Read the Lean proof on GitHub

Description

Proof of Lemma 3.1. Decompose the prescribed vertex set into the critical layers used in the paper and apply the d=1/2d=1/2 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.