def
definition
smallWorldFromSigmaCert
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NetworkScience.SmallWorldFromSigma on GitHub at line 113.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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