clusteringRatio_lt_one

formal source

  86theorem clusteringRatio_pos : 0 < clusteringRatio :=
  87  div_pos one_pos phi_pos
  88
  89theorem clusteringRatio_lt_one : clusteringRatio < 1 := by
  90  unfold clusteringRatio
  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