spectralGap_strictly_decreasing
plain-language theorem explainer
Network theorists modeling AS-level Internet graphs cite this result to confirm that the spectral gap contracts strictly with each increment in core depth k on the phi-ladder. The declaration shows that the gap at depth k+1 is smaller than at depth k, where the gap equals phi to the power minus k. The tactic proof reduces the claim to the elementary fact that phi inverse is less than one by rewriting the exponent and applying positivity and multiplication lemmas from Mathlib.
Claim. For every natural number $k$, the spectral gap at core depth $k+1$ is strictly smaller than at depth $k$, i.e., $phi^{-(k+1)} < phi^{-k}$.
background
The InternetSpectralGap module places the second eigenvalue of the normalized graph Laplacian on the phi-ladder for k-core decompositions of AS graphs. The gap is defined to equal phi to the minus k, so that successive cores contract by the factor 1/phi, matching the CAIDA observation near 0.382 at k=2. The module imports Mathlib and Constants to access real-number arithmetic and phi properties.
proof idea
The tactic proof unfolds spectralGap, obtains phi ≠ 0 from Constants.phi_ne_zero, and rewrites the exponent -(k+1) as -k + (-1) via zpow_add₀. It casts the natural number, invokes zpow_pos for positivity of the power, and uses phi_gt_onePointFive together with inv_lt_one_of_one_lt₀ to get phi inverse less than one. The inequality then follows from mul_lt_mul_of_pos_left on the positive term, closed by simpa.
why it matters
This theorem supplies the strictly_decreasing field required by the internetSpectralGapCert definition, which bundles positivity, decrease, ratio, and core-gap properties into a single certificate. It thereby supports the structural prediction that AS-level spectral gaps follow the phi-ladder. In the Recognition framework the result instantiates the self-similar fixed point phi at the level of network spectra, consistent with the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.