asCoreGap
plain-language theorem explainer
asCoreGap defines the spectral gap of the AS-level 2-core as phi to the power of negative two. Network theorists matching CAIDA AS-graph data to the phi-ladder prediction would cite this constant when instantiating the k=2 case. The definition is realized as a direct one-line abbreviation of the general spectralGap function evaluated at depth 2.
Claim. The AS-level spectral gap at k-core depth 2 is defined by $λ_2(2) := φ^{-2}$.
background
The module develops the spectral-gap layer for Internet topology on the phi-ladder. The spectral gap at k-core decomposition depth k is defined as phi to the power of negative k. This follows the structural prediction that successive k-cores have gaps in ratio 1/phi, matching the empirical CAIDA value of approximately 0.382 at k=2.
proof idea
This declaration is a one-line definition that applies the spectralGap function at argument 2.
why it matters
This definition supplies the concrete value for the AS-level core used in the positivity theorem asCoreGap_pos and the certificate structure InternetSpectralGapCert. It instantiates the k=2 case of the module prediction that the spectral gap equals 1/phi^k. The result extends the Recognition Science phi-ladder into the network-science layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.