spectralGap_pos
Network theorists modeling Internet topology via k-core decompositions cite this result to guarantee that the spectral gap remains positive at every depth. It confirms the phi-ladder construction where the gap equals phi to the power of negative k. The proof reduces immediately to the positivity of real powers with positive base.
claimFor every natural number $k$, if the spectral gap at depth $k$ is defined by $spectralGap(k) := phi^{-k}$ with $phi > 0$ the constant from the CPM bundle, then $0 < spectralGap(k)$.
background
In the InternetSpectralGap module the spectral gap is defined by spectralGap k := phi ^ (-(k : ℤ)), where phi is taken from the Constants structure in LawOfExistence. This encodes the structural prediction that the second eigenvalue of the normalised Laplacian on the k-core equals 1/phi^k, with successive cores differing by the factor 1/phi. The module doc records the empirical anchor λ₂ ≈ 0.382 ≈ 1/phi² on CAIDA AS graphs. Upstream, Constants supplies the positivity of phi and the sibling definition spectralGap supplies the explicit power expression.
proof idea
The proof is a one-line wrapper that applies zpow_pos to Constants.phi_pos. The negative integer exponent is immaterial once the base is known to be positive.
why it matters in Recognition Science
The theorem is invoked directly by asCoreGap_pos (which specialises to the 2-core) and by internetSpectralGapCert to assemble the full certificate containing gap positivity, strict decrease and ratio properties. It supplies the positivity step required by the phi-ladder model for network spectral gaps, consistent with the Recognition framework's use of phi as the self-similar fixed point. The claim is fully proved with no remaining scaffolding.
scope and limits
- Does not verify numerical agreement with CAIDA AS-graph measurements.
- Does not prove the strictly decreasing property of the gap sequence.
- Does not derive the gap from an explicit Laplacian eigenvalue computation.
- Does not extend the positivity claim beyond the phi-ladder definition.
Lean usage
theorem asCoreGap_pos : 0 < asCoreGap := spectralGap_pos 2formal statement (Lean)
32theorem spectralGap_pos (k : ℕ) : 0 < spectralGap k :=
proof body
One-line wrapper that applies zpow_pos.
33 zpow_pos Constants.phi_pos _
34