SmallWorldFromSigmaCert
plain-language theorem explainer
The SmallWorldFromSigmaCert structure bundles the core derived claims for scale-free small-world networks: the degree exponent equals 3 and solves the fixed-point equation uniquely above 2, average path length grows as log base phi of N, and the clustering ratio sits in (0.617, 0.622). Network scientists comparing Recognition Science predictions to empirical degree distributions would cite this certificate. It is assembled as a structure definition that directly references prior component theorems for each field.
Claim. The certificate asserts that the power-law exponent satisfies $γ=3$, $(γ-1)(γ-2)=2$, and is the unique solution greater than 2; that the average path length $L(N)=log_φ N$ is positive and strictly increasing for $N>1$; and that the clustering ratio $1/φ$ lies in $(0.617,0.622)$.
background
The module re-derives the Barabási-Albert exponent as the self-similar fixed point of the φ-recurrence on the recognition graph. Here gamma is defined as 3. The average path length is defined as log N / log phi and shown positive for N>1 together with strict monotonicity. The clustering ratio is defined as 1/phi and proved to lie in the stated numerical band via bounds on phi. The local setting is Track F9: power-law degree distribution from φ-recurrence, with the master certificate collecting the small-world properties.
proof idea
This is a structure definition whose fields are populated downstream. The construction smallWorldFromSigmaCert supplies each field by reflexivity for the equality gamma=3 and by direct reference to the component theorems gamma_fixed_point, gamma_unique, avgPathLength_pos, path_length_log_growth, and clusteringRatio_band.
why it matters
The structure is instantiated by smallWorldFromSigmaCert and constitutes the master certificate for §4 of the module. It encodes the derivation of gamma=3 from the σ-conservation fixed-point equation, the log_φ N scaling, and the clustering ratio 1/φ. It connects directly to the Recognition Science T6 phi fixed point and the network-science falsifier on real networks whose best-fit exponents fall outside [2.5,3.5].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.