internetSpectralGapCert
plain-language theorem explainer
The definition assembles a certificate asserting positivity, strict decrease by factor 1/φ, and positivity of the 2-core gap for the spectral-gap function on the phi-ladder model of Internet k-core topology. Network theorists working with scale-free graphs and Cheeger bounds would cite it to certify the predicted decay across core decompositions. It is a direct record constructor that packages four sibling theorems into the InternetSpectralGapCert structure.
Claim. Let $g(k)$ denote the spectral gap at k-core depth. The certificate asserts $g(k)>0$ for every natural number $k$, $g(k+1)<g(k)$, $g(k+1)/g(k)=phi^{-1}$, and $g(2)>0$.
background
The module extends the phi-ladder treatment of Internet topology, where the second eigenvalue of the normalized Laplacian on the k-core satisfies $g(k)=phi^{-k}$. This builds on the power-law exponent γ=3 and average path length log_φ N already established in the SmallWorldFromSigma module. Upstream results supply the four required properties: spectralGap_pos proves positivity via zpow_pos on phi, spectralGap_strictly_decreasing and spectralGap_ratio establish the strict decrease and exact ratio 1/φ by algebraic exponent manipulation, and asCoreGap_pos specializes the positivity claim to the 2-core.
proof idea
The definition is a one-line record constructor that directly assigns the four fields of InternetSpectralGapCert to the corresponding sibling theorems: gap_pos to spectralGap_pos, strictly_decreasing to spectralGap_strictly_decreasing, ratio to spectralGap_ratio, and as_core_pos to asCoreGap_pos.
why it matters
This certificate provides the canonical interface for the phi-ladder spectral-gap properties and is consumed by the InternetSpectralGapFromPhiLadder module to build its own certificate. It encodes the structural prediction that successive k-core gaps decrease by the factor 1/φ, matching the empirical observation λ₂ ≈ 1/φ² for the full AS-level graph. Within Recognition Science it supplies the network-science layer that extends the phi-ladder scaling already used for mass formulas and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.