clusteringRatio_pos
plain-language theorem explainer
Clustering ratio positivity follows directly from its definition as one over phi. Network theorists deriving small-world properties from preferential attachment would cite this to confirm the RS-predicted clustering exceeds the Erdős-Rényi baseline. The argument is a one-line wrapper applying the division-positivity lemma to the unit and the golden-ratio constant.
Claim. $0 < 1/phi$, where the clustering ratio is the quotient of the recognition-science clustering coefficient and the Erdős-Rényi baseline.
background
The NetworkScience.SmallWorldFromSigma module re-derives the Barabási-Albert degree exponent gamma equals three as the unique positive fixed point of the sigma-conservation equation on the recognition graph. It also establishes average path length scaling as log_phi N and the clustering coefficient ratio between RS-prediction and Erdős-Rényi baseline as 1/phi. The clusteringRatio definition supplies the explicit value 1/phi for this ratio.
proof idea
The proof is a one-line wrapper that applies div_pos to one_pos and phi_pos.
why it matters
This result anchors the module claim that the RS clustering ratio equals approximately 0.618 and is strictly positive, supporting the small-world property alongside the gamma fixed point at three. It fills the clustering step in Track F9 of the plan and connects to the forced phi fixed point in the unified forcing chain. The module falsifier concerns real networks whose best-fit exponent falls outside [2.5, 3.5].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.