gamma_fixed_point
The declaration verifies that the network degree exponent gamma satisfies the quadratic fixed-point equation (gamma - 1)(gamma - 2) = 2. Recognition Science researchers deriving small-world properties from phi-recurrence on the recognition graph cite it to anchor the Barabasi-Albert exponent at 3. The proof is a one-line term that unfolds the definition of gamma and reduces the identity via the ring tactic.
claimThe network degree exponent $gamma$ satisfies the sigma-conservation fixed-point equation $(gamma - 1)(gamma - 2) = 2$.
background
The module re-derives the Barabasi-Albert preferential-attachment model from the phi-recurrence on the recognition graph, producing the power-law degree distribution $P(k) propto k^{-gamma}$ with gamma set to 3. The sigma-conservation fixed-point equation is the algebraic relation that gamma must obey for self-similarity. Upstream results include the J-cost structure from PhiForcingDerived.of and the ledger factorization from DAlembert.LedgerFactorization.of, which calibrate the recognition costs that generate the recurrence; the module also imports the Euler-Mascheroni constant but treats gamma as a distinct network exponent.
proof idea
The proof is a term-mode one-liner. It unfolds the definition of gamma and applies the ring tactic to reduce the resulting arithmetic identity to reflexivity.
why it matters in Recognition Science
This result is invoked directly in networkScience_one_statement to bundle gamma = 3 with the fixed-point equation and the clustering-ratio band, and again in smallWorldFromSigmaCert to certify the small-world properties. It fills the fixed-point step in the phi-recurrence derivation of scale-free networks, linking to the self-similar fixed point (T6) and the eight-tick octave. It touches the open empirical question of whether real networks with more than 10^5 nodes exhibit best-fit exponents strictly inside [2.5, 3.5].
scope and limits
- Does not prove uniqueness of the positive solution greater than 2 (see gamma_unique).
- Does not derive the preferential-attachment rule or the power-law form from scratch.
- Does not perform numerical simulations or empirical fits to specific networks.
- Does not address higher-order corrections to the mean-field recurrence.
Lean usage
have h : (gamma - 1) * (gamma - 2) = 2 := gamma_fixed_pointformal statement (Lean)
46theorem gamma_fixed_point :
47 (gamma - 1) * (gamma - 2) = 2 := by
proof body
Term-mode proof.
48 unfold gamma; ring
49
50/-- `γ = 3` is the unique positive solution of `(γ - 1)(γ - 2) = 2`
51with `γ > 2`. The other solution is `γ = 0`, which is non-physical. -/