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)
113def smallWorldFromSigmaCert : SmallWorldFromSigmaCert where
114 gamma_eq_3 := rfl
proof body
Definition body.
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`. -/
depends on (13)
Lean names referenced from this declaration's body.
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
as
in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
avgPathLength_pos
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
clusteringRatio_band
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
gamma_fixed_point
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
gamma_unique
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
path_length_log_growth
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
SmallWorldFromSigmaCert
in IndisputableMonolith.NetworkScience.SmallWorldFromSigma
decl_use
-
point
in IndisputableMonolith.Numerics.Interval.Basic
decl_use
-
Power
in IndisputableMonolith.Superhuman.Core
decl_use