spectralGap

formal source

  17open Constants
  18
  19/-- Spectral gap at k-core level k: λ₂(k) = φ^(-k). -/
  20noncomputable def spectralGap (k : ℕ) : ℝ := (phi ^ k)⁻¹
  21
  22theorem spectralGap_pos (k : ℕ) : 0 < spectralGap k :=
  23  inv_pos.mpr (pow_pos phi_pos k)
  24
  25/-- Adjacent k-core spectral gap ratio = 1/φ. -/
  26theorem spectralGapRatio (k : ℕ) :
  27    spectralGap (k + 1) / spectralGap k = phi⁻¹ := by
  28  unfold spectralGap
  29  have hk := (pow_pos phi_pos k).ne'
  30  rw [pow_succ, mul_inv]
  31  field_simp [hk, phi_ne_zero]
  32
  33/-- At k=2: spectral gap = 1/φ². -/
  34theorem spectralGap_k2_val : spectralGap 2 = (phi ^ 2)⁻¹ := rfl
  35
  36structure InternetSpectralGapCert where
  37  gap_pos : ∀ k, 0 < spectralGap k
  38  phi_inv_ratio : ∀ k, spectralGap (k + 1) / spectralGap k = phi⁻¹
  39
  40noncomputable def internetSpectralGapCert : InternetSpectralGapCert where
  41  gap_pos := spectralGap_pos
  42  phi_inv_ratio := spectralGapRatio
  43
  44end IndisputableMonolith.NetworkScience.InternetSpectralGapFromPhiLadder