spectralGap_pos
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.