spectralGap
plain-language theorem explainer
The definition sets the k-core spectral gap λ₂(k) to φ^{-k} for the Internet AS graph under the phi-ladder decay model. Network theorists testing Recognition Science predictions on empirical graphs cite this for its explicit tie to the ratio 1/φ and the k=2 value near 0.382. It is realized as a direct one-line assignment equating the gap to the reciprocal of phi to the power k.
Claim. The k-core spectral gap satisfies λ₂(k) = φ^{-k}.
background
The module models the spectral gap of the Internet AS-level graph via k-core decomposition on the phi-ladder. Upstream, the sibling definition states spectralGap (k : ℕ) : ℝ := phi ^ (-(k : ℤ)). This variant supplies the equivalent reciprocal form to support downstream ratio and positivity results. The module doc states the RS prediction that λ₂(k+1)/λ₂(k) = φ^{-1} with λ₂(2) ≈ 0.382.
proof idea
This is a one-line definition that directly assigns (phi ^ k)^{-1} to spectralGap k.
why it matters
It supplies the explicit form consumed by asCoreGap for the k=2 case and by InternetSpectralGapCert for the structure holding positivity, strict decrease, and ratio properties. This fills the phi-ladder prediction in the network science application, linking to the self-similar fixed point. The supplied results flag no open questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.