pith. machine review for the scientific record. sign in
theorem proved term proof

networkScience_one_statement

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 124theorem networkScience_one_statement :
 125    gamma = 3 ∧
 126    (gamma - 1) * (gamma - 2) = 2 ∧
 127    (0.617 : ℝ) < clusteringRatio ∧ clusteringRatio < 0.622 :=

proof body

Term-mode proof.

 128  ⟨rfl, gamma_fixed_point, clusteringRatio_band.1, clusteringRatio_band.2⟩
 129
 130end
 131
 132end SmallWorldFromSigma
 133end NetworkScience
 134end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.