SmallWorldFromSigmaCert
plain-language theorem explainer
The certificate structure bundles the key predictions of the Recognition Science network model: the degree exponent equals 3 and is the unique solution greater than 2 to (γ − 1)(γ − 2) = 2, the average path length is positive and strictly increasing with network size, and the clustering ratio lies in (0.617, 0.622). Network theorists studying small-world properties in scale-free graphs would cite this certificate when deriving the Barabási-Albert exponent from the φ-recurrence. It is assembled as a structure definition that directly references
Claim. Let γ be the power-law degree exponent, L(N) the average path length, and C the clustering ratio. Then γ = 3, (γ − 1)(γ − 2) = 2, γ is the unique x > 2 satisfying (x − 1)(x − 2) = 2, L(N) > 0 for all N > 1, L is strictly increasing on (1, ∞), and 0.617 < C < 0.622 with C = 1/φ.
background
In this module the power-law exponent is defined to be 3 and shown to satisfy the fixed-point equation (γ − 1)(γ − 2) = 2 that arises from σ-conservation on the recognition graph. The average path length is defined as log base φ of N and the clustering ratio as 1/φ. The module establishes the small-world property for networks whose degree distribution follows the φ-recurrence, with path length growing logarithmically and clustering ratio fixed at the golden-ratio reciprocal. Upstream results include the positivity of average path length for N > 1, which follows from the positivity of the logarithms, and the numerical bounds on clustering ratio derived from the interval 1.61 < φ < 1.62.
proof idea
The structure is populated by a direct assignment: the equality to 3 holds by reflexivity, the fixed-point equation by the fixed-point lemma, uniqueness by the uniqueness theorem, positivity of path length by the positivity theorem, strict increase by the monotonicity lemma, and the clustering band by the explicit numerical verification using the bounds on φ.
why it matters
This structure supplies the master certificate for section 4 of the module, which re-derives the exponent 3 as the self-similar fixed point of the φ-recurrence on the recognition graph. It is referenced by the small-world certificate definition that packages the full set of small-world properties. The result aligns with the T6 landmark that forces φ as the self-similar fixed point and provides the falsifier that real networks must exhibit exponents inside [2.5, 3.5] for the prediction to hold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.