pith. sign in
theorem

gamma_fixed_point

proved
show as:
module
IndisputableMonolith.NetworkScience.SmallWorldFromSigma
domain
NetworkScience
line
46 · github
papers citing
none yet

plain-language theorem explainer

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.

Claim. The 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

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].

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.