spectralGap_pos
The theorem establishes that the k-core spectral gap, defined as the reciprocal of the golden ratio raised to k, remains strictly positive for every natural number k. Network theorists working on Internet topology models cite it to guarantee the phi-decay ladder stays positive. The proof reduces directly via the inverse-positivity lemma applied to the positivity of phi to the k.
claimFor every natural number $k$, $0 < (phi^k)^{-1}$, where $phi > 1$ is the golden ratio.
background
The module models the second eigenvalue of the Internet AS graph under k-core decomposition as decaying on the phi ladder: λ₂(k) = φ^{-k}. This follows the Recognition Science prediction that consecutive gaps stand in ratio 1/φ. The local definition sets spectralGap k to the reciprocal of phi to the power k, relying on phi positivity from the Constants module.
proof idea
The term proof invokes inv_pos.mpr on the result of pow_pos phi_pos k. This composes the fact that phi^k > 0 with the preservation of positivity under inversion to conclude the gap is positive.
why it matters in Recognition Science
The result supplies the positivity axiom for the InternetSpectralGapCert certificate and is used to define asCoreGap_pos at k=2. It anchors the phi-ladder in the NetworkScience domain, consistent with the self-similar fixed point phi from the T0-T8 forcing chain. No open questions remain for this positivity statement.
scope and limits
- Does not establish the numerical magnitude of the gap at any k.
- Does not prove the ratio between gaps at consecutive k.
- Does not connect to the gap=45 result from Gap45.Derivation.
- Does not include empirical fitting to real Internet data.
formal statement (Lean)
22theorem spectralGap_pos (k : ℕ) : 0 < spectralGap k :=
proof body
Term-mode proof.
23 inv_pos.mpr (pow_pos phi_pos k)
24
25/-- Adjacent k-core spectral gap ratio = 1/φ. -/