degreeExponent_gt_two
plain-language theorem explainer
The declaration proves the RS-predicted degree exponent exceeds 2, satisfying the scale-free condition for power-law networks. Network modelers using preferential attachment at D = 3 would cite it to place the golden-ratio value inside the observed γ interval 2.1-2.3. The proof unfolds the definition γ := 1 + φ and applies linear arithmetic to the upstream fact 1 < φ.
Claim. Let γ = 1 + φ where φ is the golden ratio. Then γ > 2.
background
The module derives internet topology from sigma conservation under preferential attachment. Scale-free networks obey P(k) ∝ k^{-γ} with measured γ ≈ 2.1-2.3. Recognition Science fixes γ = 1 + φ ≈ 2.618 because each attachment step is a recognition-cost decision whose J-cost ratio at the canonical band equals 1/φ. The sibling definition degreeExponent : ℝ := 1 + phi supplies the explicit expression. The upstream lemma one_lt_phi states 1 < phi and is imported from both Constants and PhiSupport.
proof idea
The term-mode proof unfolds degreeExponent to obtain 1 + phi, then invokes linarith on the hypothesis one_lt_phi : 1 < phi to conclude 1 + phi > 2.
why it matters
The result populates the scale_free field inside networkTopologyCert, which certifies that the RS exponent meets the mathematical requirement for scale-free topology. It completes the local derivation γ = 2 + 1/φ that follows from J-cost conservation at the phi band and the eight-tick octave. The step supports the broader claim that D = 3 plus sigma conservation forces the observed Zipf-Pareto range.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.