spectralGapRatio
plain-language theorem explainer
The theorem establishes that the ratio of spectral gaps at successive k-core levels equals the inverse of the golden ratio. Researchers modeling the Internet's AS-level topology with Recognition Science's phi-ladder would cite this to verify the predicted self-similarity. The proof is a short sequence of rewrites that unfolds the power definition and simplifies the ratio using the non-zero property of phi.
Claim. For each natural number $k$, if the spectral gap satisfies $λ_2(k) = φ^{-k}$, then $λ_2(k+1)/λ_2(k) = φ^{-1}$.
background
The module defines the spectral gap at k-core level k by $λ_2(k) = φ^{-k}$. This encodes the phi-ladder decay for the Internet AS graph as described in the module documentation. The upstream lemma from Constants states that phi is nonzero, enabling the division in the ratio expression. The theoretical setting is the F5 depth analysis where the Recognition Science prediction asserts that adjacent gaps on the ladder satisfy the ratio one over phi, with the concrete value at k equals two being approximately one over phi squared.
proof idea
The proof unfolds the spectralGap definition to expose the powers of phi. It invokes the positivity of phi to produce a non-zero witness for the k-th power. The successor is expanded via pow_succ, the inverse is rewritten as a product, and field_simp cancels terms with the non-zero lemma to yield phi inverse.
why it matters
This theorem provides the phi-inverse ratio that the internetSpectralGapCert certificate in the same module requires. It directly encodes the RS prediction from the module doc-comment that the adjacent k-core spectral gap ratio equals one over phi. The result ties the phi-ladder structure to network spectral properties, supporting the self-similar fixed point at the scale of the Internet graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.