InternetSpectralGapCert
plain-language theorem explainer
InternetSpectralGapCert collects the four properties required to certify that the spectral gap on the phi-ladder matches the predicted scaling for Internet AS graphs. Network scientists studying scale-free topologies cite the certificate when asserting that successive k-core gaps decrease by the factor phi inverse. The structure is assembled directly from the positivity, monotonicity, ratio, and core-gap lemmas already established for spectralGap.
Claim. Let $g(k) := phi^{-k}$. 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 develops the spectral-gap layer for Internet topology on the phi-ladder. spectralGap k is defined as phi raised to the power minus k. asCoreGap is set to spectralGap 2, identified with the empirical CAIDA AS-graph value approximately 0.382 or one over phi squared. The module documentation states that the structural prediction is that the spectral gap for the k-core decomposition at depth k equals 1 over phi to the k, with ratios between successive cores equal to one over phi. Upstream results include the gap definitions from Gap45.Derivation and the anchor gap functions, but the local spectralGap and asCoreGap supply the concrete expressions.
proof idea
The structure is populated by supplying the four field values gap_pos, strictly_decreasing, ratio, and as_core_pos. These are taken directly from the lemmas spectralGap_pos, spectralGap_strictly_decreasing, spectralGap_ratio, and asCoreGap_pos.
why it matters
This certificate is instantiated by internetSpectralGapCert in the same module and by the parallel construction in InternetSpectralGapFromPhiLadder. It supplies the formal statement that the second eigenvalue of the normalized Laplacian on the AS-level graph follows the phi-ladder scaling, consistent with the Recognition Science forcing chain that derives phi as the self-similar fixed point. The declaration closes the gap between the abstract phi-ladder and the concrete network-science prediction for spectral gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.