spectralGap_ratio
plain-language theorem explainer
The ratio of spectral gaps between successive k-core levels equals 1/φ under the phi-ladder definition. Network theorists modeling the second eigenvalue of the normalized Laplacian on AS-level Internet graphs would cite this to confirm geometric decay of the Cheeger bound. The proof unfolds the exponential definition of the gap and reduces the ratio by rewriting the exponent difference and applying field simplification with positivity of φ.
Claim. For every natural number $k$, the ratio of the spectral gap at depth $k+1$ to the gap at depth $k$ equals $1/φ$, where the gap at depth $k$ is defined by $φ^{-k}$.
background
The module places the second eigenvalue λ₂ of the normalized graph Laplacian on the phi-ladder for k-core decompositions of the Internet AS graph. The definition spectralGap(k) := φ^(-(k : ℤ)) encodes the structural claim that λ₂(k) = 1/φ^k, with the observed value ≈0.382 for k=2 matching 1/φ². This rests on the phi_ne_zero lemma (φ ≠ 0) from Constants and the phi-ladder constructions imported from PhiLadderLattice and PhiSupport.Lemmas.
proof idea
The tactic proof unfolds spectralGap to expose the ratio of consecutive negative powers. It rewrites the exponent -(k+1) as -k + (-1) via ring, applies zpow_add₀ using phi_ne_zero, casts the natural-number increment, invokes zpow_pos for positivity of the remaining power, and finishes with field_simp to cancel the common factor.
why it matters
The result supplies the ratio field required by the internetSpectralGapCert structure, which bundles positivity, strict monotonicity, the ratio, and the core-gap positivity into a single certificate for the Internet topology model. It realizes the module's explicit prediction that successive k-core gaps stand in ratio 1/φ, linking the phi fixed-point construction to an observable network invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.