clusteringRatio_band

formal source

  91  rw [div_lt_one phi_pos]
  92  exact one_lt_phi
  93
  94theorem clusteringRatio_band :
  95    (0.617 : ℝ) < clusteringRatio ∧ clusteringRatio < 0.622 := by
  96  unfold clusteringRatio
  97  have h1 := phi_gt_onePointSixOne
  98  have h2 := phi_lt_onePointSixTwo
  99  refine ⟨?_, ?_⟩
 100  · rw [lt_div_iff₀ phi_pos]; linarith
 101  · rw [div_lt_iff₀ phi_pos]; linarith
 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 :