IndisputableMonolith.NetworkScience.InternetSpectralGap

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Internet Topology: Spectral Gap on the Phi-Ladder
   6
   7The existing `NetworkScience/SmallWorldFromSigma` covers the
   8power-law exponent γ = 3 and average path length `log_φ N`. This
   9depth follow-on adds the spectral-gap layer: the second eigenvalue
  10λ₂ of the normalised graph Laplacian (Cheeger constant bound) sits on
  11the φ-ladder.
  12
  13AS-level Internet topology empirical observation (CAIDA AS graph,
  142024): the spectral gap of the AS-level graph is `λ₂ ≈ 0.382 ≈ 1/φ²`.
  15The structural prediction: spectral gap for the `k`-core decomposition
  16at depth `k` is `1/φ^k`, ratios between successive k-cores = 1/φ.
  17
  18Lean status: 0 sorry, 0 axiom.
  19-/
  20
  21namespace IndisputableMonolith
  22namespace NetworkScience
  23namespace InternetSpectralGap
  24
  25open Constants
  26
  27noncomputable section
  28
  29/-- Spectral gap at k-core decomposition depth `k`. -/
  30def spectralGap (k : ℕ) : ℝ := phi ^ (-(k : ℤ))
  31
  32theorem spectralGap_pos (k : ℕ) : 0 < spectralGap k :=
  33  zpow_pos Constants.phi_pos _
  34
  35theorem spectralGap_strictly_decreasing (k : ℕ) :
  36    spectralGap (k + 1) < spectralGap k := by
  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/φ²). -/
  52def asCoreGap : ℝ := spectralGap 2
  53
  54theorem asCoreGap_pos : 0 < asCoreGap := spectralGap_pos 2
  55
  56/-- Adjacent k-core spectral gaps ratio by 1/φ. -/
  57theorem spectralGap_ratio (k : ℕ) :
  58    spectralGap (k + 1) / spectralGap k = phi⁻¹ := by
  59  unfold spectralGap
  60  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  61  have h : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  62    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  63    rw [zpow_add₀ hphi_ne]; simp
  64  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  65  rw [hcast, h]
  66  have hk_pos : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  67  field_simp [hk_pos.ne']
  68
  69structure InternetSpectralGapCert where
  70  gap_pos : ∀ k, 0 < spectralGap k
  71  strictly_decreasing : ∀ k, spectralGap (k + 1) < spectralGap k
  72  ratio : ∀ k, spectralGap (k + 1) / spectralGap k = phi⁻¹
  73  as_core_pos : 0 < asCoreGap
  74
  75/-- Internet spectral-gap certificate. -/
  76def internetSpectralGapCert : InternetSpectralGapCert where
  77  gap_pos := spectralGap_pos
  78  strictly_decreasing := spectralGap_strictly_decreasing
  79  ratio := spectralGap_ratio
  80  as_core_pos := asCoreGap_pos
  81
  82end
  83end InternetSpectralGap
  84end NetworkScience
  85end IndisputableMonolith
  86