InternetSpectralGapCert
InternetSpectralGapCert packages the positivity and exact phi-inverse ratio of the k-core spectral gap under the phi-ladder definition. Network theorists modeling scale-free graphs or testing RS-derived decay predictions would cite it to certify the geometric ratio property. The declaration is a bare structure definition that directly encodes the two forall statements with no additional lemmas or tactics.
claimA certificate structure asserting that the spectral gap satisfies $0 < λ_2(k)$ for every natural number $k$ and $λ_2(k+1)/λ_2(k) = φ^{-1}$ for every $k$, where $λ_2(k) = φ^{-k}$.
background
The module treats the Internet AS-level graph via k-core decomposition and defines the spectral gap at depth $k$ by the explicit formula $λ_2(k) = (φ^k)^{-1}$. This implements the RS prediction that the gap decays geometrically with ratio $φ^{-1}$ on the phi-ladder. The upstream gap_pos theorem from LDPCCodeRateFromPhi shows positivity of analogous capacity gaps by unfolding to one_div_pos and mul_pos with phi_pos. The sibling spectralGap definition in the same module supplies the closed-form expression used by both fields.
proof idea
The declaration is a structure definition whose body consists solely of the two field declarations gap_pos and phi_inv_ratio. No tactics, reductions, or upstream lemmas are invoked; it functions as a typed container for the two properties.
why it matters in Recognition Science
The structure is instantiated by internetSpectralGapCert in the same module and supplies the gap_pos and ratio components to the fuller InternetSpectralGapCert in the parent NetworkScience.InternetSpectralGap module. It directly encodes the phi-ladder decay prediction stated in the module doc, linking the spectral-gap observable to the self-similar fixed point phi and the eight-tick octave of the forcing chain. No open scaffolding questions are addressed.
scope and limits
- Does not derive the spectral-gap formula from any graph-theoretic axioms.
- Does not produce numerical evaluations or bounds for concrete k.
- Does not incorporate empirical AS-graph measurements.
- Does not extend to other invariants such as higher eigenvalues or clustering.
formal statement (Lean)
36structure InternetSpectralGapCert where
37 gap_pos : ∀ k, 0 < spectralGap k
38 phi_inv_ratio : ∀ k, spectralGap (k + 1) / spectralGap k = phi⁻¹
39