gamma_pos
The theorem establishes that the network exponent gamma defined as 3 is strictly positive. Researchers deriving scale-free networks from phi-recurrence on recognition graphs cite it to anchor the degree-distribution inequalities. The proof reduces directly to unfolding the constant definition and applying numerical normalization.
claimThe power-law degree-distribution exponent satisfies $0 < 3$.
background
In the SmallWorldFromSigma module the local definition sets gamma to the constant 3, the unique positive root of the sigma-conservation fixed-point equation (gamma-1)(gamma-2)=2 that arises as the self-similar fixed point of the phi-recurrence. The module derives the Barabasi-Albert exponent gamma=3 together with log_phi N scaling of average path length and a clustering ratio of 1/phi. Upstream the definition of gamma as 3 is supplied directly by the sibling declaration in the same module; the Euler-Mascheroni gamma from Constants is imported but remains a separate symbol.
proof idea
The proof is a one-line term wrapper that unfolds the definition of gamma to the numeral 3 and invokes norm_num to verify the inequality 0 < 3 in the reals.
why it matters in Recognition Science
The result supplies the elementary positivity fact required for the power-law degree distribution in the small-world model. It is referenced by the downstream euler_mascheroni_bounds theorem (which bundles positivity and upper bounds on the Euler-Mascheroni constant) and by the sibling gamma_pos declaration. Within the Recognition Science framework it instantiates the self-similar fixed point (T6) that forces gamma=3 from the phi-ladder, consistent with the eight-tick octave and D=3 spatial structure; the open question it touches is the full RS derivation of the Euler-Mascheroni constant, still blocked on the Riemann hypothesis as noted in the downstream doc-comment.
scope and limits
- Does not derive gamma from the phi-recurrence equation.
- Does not prove uniqueness of the fixed-point solution.
- Does not address the small-world path-length scaling or clustering ratio.
- Does not connect the network gamma to the Euler-Mascheroni constant.
formal statement (Lean)
43theorem gamma_pos : 0 < gamma := by unfold gamma; norm_num
proof body
Term-mode proof.
44
45/-- The σ-conservation fixed-point equation: `(γ - 1)(γ - 2) = 2`. -/