degreeExponent_eq_two_plus_inv
plain-language theorem explainer
The theorem identifies the degree exponent γ in scale-free networks as exactly 2 plus the reciprocal of the golden ratio. Complex network researchers modeling preferential attachment under cost conservation would reference this equality. The short tactic proof unfolds the definition and reduces the identity using the golden ratio quadratic equation and linear arithmetic.
Claim. The degree exponent γ defined by γ := 1 + φ satisfies γ = 2 + φ^{-1}, where φ is the golden ratio obeying φ² = φ + 1.
background
The module derives network topology predictions from the sigma conservation law in Recognition Science. Scale-free networks follow P(k) ∝ k^{-γ} with the RS-predicted γ = 2 + 1/φ ≈ 2.618 for D = 3. The definition degreeExponent := 1 + phi is introduced here, relying on the golden ratio φ satisfying φ² = φ + 1 from upstream lemmas in Constants and PhiLadderLattice.
proof idea
Unfold degreeExponent to obtain 1 + φ. Apply phi_sq_eq to get φ² = φ + 1. Use field_simp with phi_ne_zero to rearrange to φ^{-1} = φ - 1. Conclude the target equality by linarith.
why it matters
This equality is incorporated into networkTopologyCert to certify the scale-free exponent band. It completes the step linking σ-conservation to the exponent 2 + 1/φ, consistent with the phi self-similar fixed point in the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.