SmallWorldFromSigmaCert

formal source

 102
 103/-! ## §4. Master certificate -/
 104
 105structure SmallWorldFromSigmaCert where
 106  gamma_eq_3 : gamma = 3
 107  gamma_fixed : (gamma - 1) * (gamma - 2) = 2
 108  gamma_unique : ∀ {x : ℝ}, 2 < x → (x - 1) * (x - 2) = 2 → x = gamma
 109  avgPathLength_pos : ∀ {N : ℝ}, 1 < N → 0 < avgPathLength N
 110  path_log_growth : ∀ {N M : ℝ}, 1 < N → N < M → avgPathLength N < avgPathLength M
 111  clusteringRatio_band : (0.617 : ℝ) < clusteringRatio ∧ clusteringRatio < 0.622
 112
 113def smallWorldFromSigmaCert : SmallWorldFromSigmaCert where
 114  gamma_eq_3 := rfl
 115  gamma_fixed := gamma_fixed_point
 116  gamma_unique := @gamma_unique
 117  avgPathLength_pos := @avgPathLength_pos
 118  path_log_growth := @path_length_log_growth
 119  clusteringRatio_band := clusteringRatio_band
 120
 121/-- **NETWORK SCIENCE ONE-STATEMENT.** Power-law exponent `γ = 3` is
 122the unique positive σ-conservation fixed point; average path length
 123scales as `log_φ N` (small-world); clustering ratio is `1/φ ≈ 0.618`. -/
 124theorem networkScience_one_statement :
 125    gamma = 3 ∧
 126    (gamma - 1) * (gamma - 2) = 2 ∧
 127    (0.617 : ℝ) < clusteringRatio ∧ clusteringRatio < 0.622 :=
 128  ⟨rfl, gamma_fixed_point, clusteringRatio_band.1, clusteringRatio_band.2⟩
 129
 130end
 131
 132end SmallWorldFromSigma
 133end NetworkScience
 134end IndisputableMonolith