gamma_unique
plain-language theorem explainer
The uniqueness result for the network exponent states that 3 is the only real number exceeding 2 satisfying the fixed-point equation (x-1)(x-2)=2. Researchers modeling small-world networks from recognition graphs cite this to fix the degree-distribution power at exactly 3. The proof reduces the given equation to a factored product via linear arithmetic and splits cases with the zero-product lemma, discarding the extraneous root under the hypothesis x>2.
Claim. If $x > 2$ and $(x-1)(x-2) = 2$, then $x = 3$, where 3 denotes the predicted power-law exponent for the degree distribution.
background
The SmallWorldFromSigma module derives scale-free network properties from the phi-recurrence fixed point on the recognition graph. Here gamma is defined as the constant 3. The equation (gamma-1)(gamma-2)=2 encodes sigma-conservation at the self-similar fixed point. Upstream, mul_eq_zero supplies the zero-product property from the integers-from-logic construction, while the gamma definition provides the target value. The module setting links this to the Barabási-Albert model re-derived via recognition composition.
proof idea
The tactic proof first invokes nlinarith on the hypothesis to obtain the equivalent equation x(x-3)=0. It then applies mul_eq_zero to produce the disjunction x=0 or x=3. The branch x=0 is eliminated by linarith using the assumption 2<x. The remaining branch unfolds the definition of gamma and closes by linarith.
why it matters
This result populates the gamma_unique field of the SmallWorldFromSigmaCert structure, which certifies the full set of small-world predictions including fixed-point satisfaction and logarithmic path-length growth. It completes the derivation of gamma=3 as the unique positive solution to the sigma-conservation equation in the module's plan. Within Recognition Science it anchors the network-science track by connecting the recognition graph's self-similarity to the observed exponent near 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.