spectralGap_pos
plain-language theorem explainer
Network theorists modeling Internet topology via k-core decompositions cite this result to guarantee that the spectral gap remains positive at every depth. It confirms the phi-ladder construction where the gap equals phi to the power of negative k. The proof reduces immediately to the positivity of real powers with positive base.
Claim. For every natural number $k$, if the spectral gap at depth $k$ is defined by $spectralGap(k) := phi^{-k}$ with $phi > 0$ the constant from the CPM bundle, then $0 < spectralGap(k)$.
background
In the InternetSpectralGap module the spectral gap is defined by spectralGap k := phi ^ (-(k : ℤ)), where phi is taken from the Constants structure in LawOfExistence. This encodes the structural prediction that the second eigenvalue of the normalised Laplacian on the k-core equals 1/phi^k, with successive cores differing by the factor 1/phi. The module doc records the empirical anchor λ₂ ≈ 0.382 ≈ 1/phi² on CAIDA AS graphs. Upstream, Constants supplies the positivity of phi and the sibling definition spectralGap supplies the explicit power expression.
proof idea
The proof is a one-line wrapper that applies zpow_pos to Constants.phi_pos. The negative integer exponent is immaterial once the base is known to be positive.
why it matters
The theorem is invoked directly by asCoreGap_pos (which specialises to the 2-core) and by internetSpectralGapCert to assemble the full certificate containing gap positivity, strict decrease and ratio properties. It supplies the positivity step required by the phi-ladder model for network spectral gaps, consistent with the Recognition framework's use of phi as the self-similar fixed point. The claim is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.