clusteringRatio_lt_one
plain-language theorem explainer
The Recognition Science small-world model predicts a clustering ratio of 1/phi that lies strictly below the Erdős-Rényi baseline. Network physicists deriving topology from phi-recurrence would cite this bound to confirm the clustering component of the small-world regime. The proof is a direct term reduction that unfolds the definition and invokes the established inequality 1 < phi.
Claim. In the Recognition Science derivation of small-world networks, the clustering ratio satisfies $1/phi < 1$.
background
The module re-derives the Barabási-Albert preferential-attachment model from the phi-recurrence on recognition graphs, yielding a power-law degree distribution with exponent gamma = 3 as the unique positive fixed point of the sigma-conservation equation. ClusteringRatio is defined as 1/phi and represents the ratio of the RS-predicted clustering coefficient to the Erdős-Rényi random-graph baseline. The upstream lemma one_lt_phi establishes that the golden ratio phi exceeds 1, which supplies the decisive inequality for this result.
proof idea
The term-mode proof first unfolds the definition of clusteringRatio to obtain 1/phi. It then rewrites the target inequality via div_lt_one after confirming positivity of phi, and concludes by applying the lemma one_lt_phi.
why it matters
This bound verifies that the RS clustering prediction remains below the random-graph value, a required step in establishing the small-world property within the phi-ladder framework. It contributes to the overall SmallWorldFromSigmaCert by confirming the clustering band alongside the gamma = 3 fixed point and logarithmic path-length scaling. The result sits inside the Recognition Science forcing chain at the self-similar fixed point phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.