`networkScience_one_statement`

proved

show as: view math explainer →

module: IndisputableMonolith.NetworkScience.SmallWorldFromSigma
domain: NetworkScience
line: 124 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.NetworkScience.SmallWorldFromSigma on GitHub at line 124.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.