gamma_pos
plain-language theorem explainer
The declaration establishes positivity of the power-law degree-distribution exponent in the small-world derivation. Network theorists citing the sigma-conservation fixed point would reference this result to anchor bounds before deriving log-phi path lengths. The proof is a one-line term wrapper that unfolds the constant definition of gamma as 3 and applies norm_num.
Claim. $0 < 3$, where $3$ is the unique positive solution of the fixed-point equation $(γ-1)(γ-2)=2$ for the power-law exponent in the preferential-attachment model.
background
The module derives power-law degree distributions from φ-recurrence on the recognition graph (Track F9). The local definition sets gamma to the constant 3 as the self-similar fixed point of the σ-conservation equation on degree distributions. Module documentation states that gamma equals 3 is the unique positive solution of (γ-1)·(γ-2)=2, with average path length scaling as log_φ N and clustering ratio 1/φ. Upstream results include the Euler-Mascheroni gamma definition (lim (H_n - ln n) ≈ 0.577) and its positivity theorem, plus the PPN gamma scaffold set to 1 at leading order.
proof idea
The proof is a term-mode one-liner. It unfolds the sibling definition gamma := 3, then applies norm_num to discharge the arithmetic inequality 0 < 3 in the reals. No further lemmas or hypotheses are invoked.
why it matters
This positivity result anchors the gamma=3 fixed point before path-length and clustering derivations in the same module. It is referenced by the Euler-Mascheroni bounds theorem and the gamma_pos result in the constants module. Within Recognition Science it supports the network-science track that re-derives the Barabási-Albert exponent as the φ-recurrence fixed point, consistent with the eight-tick octave and D=3 landmarks. It touches the open C-011 status of a full RS derivation of the Euler-Mascheroni constant, which remains blocked on the Riemann hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.