spectralGap_strictly_decreasing
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove that any concrete Internet graph realizes the phi-ladder exactly.
- Does not derive the gap formula from the Recognition Composition Law.
- Does not address higher eigenvalues or the full Laplacian spectrum.
- Does not compute explicit numerical gaps for particular k beyond the inequality.
Lean usage
example (k : ℕ) : spectralGap (k + 1) < spectralGap k := spectralGap_strictly_decreasing kformal statement (Lean)
35theorem spectralGap_strictly_decreasing (k : ℕ) :
36 spectralGap (k + 1) < spectralGap k := by
proof body
Tactic-mode proof.
37 unfold spectralGap
38 have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
39 have h : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
40 rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
41 rw [zpow_add₀ hphi_ne]; simp
42 have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
43 rw [hcast, h]
44 have hk_pos : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
45 have hphi_inv_lt_one : phi⁻¹ < 1 :=
46 inv_lt_one_of_one_lt₀ (by have := Constants.phi_gt_onePointFive; linarith)
47 have : phi ^ (-(k : ℤ)) * phi⁻¹ < phi ^ (-(k : ℤ)) * 1 :=
48 mul_lt_mul_of_pos_left hphi_inv_lt_one hk_pos
49 simpa using this
50
51/-- The AS-level spectral gap at k=2 (the observed CAIDA value ≈ 0.382 ≈ 1/φ²). -/