clusteringRatio_band
plain-language theorem explainer
The theorem establishes that the clustering ratio in the Recognition Science network model lies strictly between 0.617 and 0.622. Network theorists deriving small-world properties from phi-based recurrences would cite this bound to confirm the predicted ratio of approximately 0.618. The proof unfolds the definition as one over phi and applies the established numerical bounds on phi together with division inequalities and linear arithmetic.
Claim. The predicted clustering ratio satisfies $0.617 < 1/phi < 0.622$.
background
The module derives power-law degree distributions and small-world properties from the phi-recurrence on the recognition graph. The clustering ratio is defined as the ratio of the RS-predicted clustering coefficient to the Erdős-Rényi baseline, given explicitly by 1/phi. The module doc states: 'The clustering coefficient ratio between RS-prediction and Erdős-Rényi baseline is 1/φ ≈ 0.618.' Upstream lemmas supply the tight bounds phi > 1.61 and phi < 1.62, with the former described as 'Even tighter lower bound: φ > 1.61.' The local setting is the re-derivation of gamma = 3 as the unique positive solution of the sigma-conservation fixed-point equation.
proof idea
The proof unfolds the definition of clusteringRatio to obtain 1/phi. It invokes the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo to obtain 1.61 < phi < 1.62. The target inequalities are rewritten using lt_div_iff₀ and div_lt_iff₀ (leveraging phi_pos) and discharged by linarith.
why it matters
This bound completes the one-statement summary of network science predictions in networkScience_one_statement, which asserts gamma = 3, the fixed-point equation (gamma - 1) * (gamma - 2) = 2, and the clustering ratio interval. It supports the small-world property with clustering ratio 1/phi, consistent with the phi self-similar fixed point. The result fills the clustering coefficient slot in the Barabási-Albert model re-derived via phi-recurrence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.