smallWorldFromSigmaCert
plain-language theorem explainer
The declaration assembles a certificate structure confirming that the power-law degree exponent gamma equals 3 as the unique fixed point satisfying (gamma-1)(gamma-2)=2 under sigma conservation on the recognition graph. Network scientists modeling scale-free small-world networks would reference this to justify the observed gamma approximately 3 and the logarithmic path-length scaling. The construction is a direct structure instantiation that invokes reflexivity for the equality gamma=3 and delegates the remaining properties to established fixed
Claim. The structure asserts that the power-law exponent $gamma$ satisfies $gamma=3$, the fixed-point equation $(gamma-1)(gamma-2)=2$, uniqueness of this solution among $x>2$, positivity of the average path length for networks with more than one node, strict increase of path length with network size, and that the clustering ratio $1/phi$ lies in the interval $(0.617,0.622)$.
background
In the NetworkScience module the power-law exponent gamma is the unique positive solution to the equation $(gamma-1)(gamma-2)=2$ obtained from the phi-recurrence on the recognition graph. Average path length is defined to scale as $log_phi N$ and satisfies positivity together with monotonic growth for $N>1$. The clustering ratio is defined as $1/phi$ and is shown to lie in the narrow band $(0.617,0.622)$ around the golden-ratio value. The module documentation states that this recovers the Barabasi-Albert exponent gamma=3 together with the small-world property and the clustering ratio $1/phi$. The certificate collects these facts into a single structure that depends on the fixed-point result gamma_fixed_point, the positivity theorem avgPathLength_pos, and the uniqueness lemma gamma_unique from the same file.
proof idea
The definition constructs the SmallWorldFromSigmaCert structure by setting the gamma_eq_3 field via reflexivity and assigning the remaining fields directly to the theorems gamma_fixed_point, gamma_unique, avgPathLength_pos, path_length_log_growth, and clusteringRatio_band.
why it matters
This definition supplies the canonical certificate for the small-world properties derived from the sigma-conservation fixed point. It completes the one-statement summary given in the module documentation for Track F9, asserting gamma=3, logarithmic scaling of path lengths in base phi, and clustering ratio $1/phi$. The result supports the framework claim that the eight-tick octave and D=3 spatial dimensions produce scale-free networks with these exponents. It touches the open falsification question whether real networks with more than 10^5 nodes consistently exhibit best-fit exponents inside the predicted interval [2.5,3.5].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.