avgPathLength_pos
For N greater than 1 the phi-scaled average path length log N over log phi is strictly positive. Network theorists deriving small-world scaling from recognition graphs cite this to confirm the logarithmic regime stays positive. The argument unfolds the definition and applies positivity of the real logarithm to both numerator and denominator before invoking division preservation.
claimFor every real number $N$ with $N > 1$, $0 < (log N) / (log phi)$.
background
The module derives the small-world property from the phi-recurrence on recognition graphs. Average path length is defined as $L(N) = log N / log phi$, the unique scaling that satisfies the self-similar fixed-point condition on the degree distribution. The upstream lemma one_lt_phi establishes phi > 1, which is required to guarantee that the denominator is positive and the logarithm is well-defined for N > 1.
proof idea
The term proof unfolds avgPathLength to expose the quotient of logarithms. It applies Real.log_pos to the hypothesis 1 < N to obtain a positive numerator, then applies the same lemma to one_lt_phi to obtain a positive denominator. The final step invokes div_pos to conclude the quotient is positive.
why it matters in Recognition Science
This result supplies the positivity clause inside the SmallWorldFromSigmaCert structure, which also records gamma = 3 and the monotonic growth of path length. It anchors the logarithmic scaling that distinguishes small-world networks from random graphs in the Recognition Science derivation of the Barabasi-Albert exponent. The parent certificate is used to certify the full small-world package against the falsifier of power-law exponents outside [2.5, 3.5].
scope and limits
- Does not compute a numerical value for the path length.
- Does not apply when N is at most 1.
- Does not address clustering coefficients or degree exponents.
- Does not extend to directed or weighted networks.
Lean usage
theorem path_pos_example : 0 < avgPathLength 100 := by apply avgPathLength_pos; norm_numformal statement (Lean)
67theorem avgPathLength_pos {N : ℝ} (h : 1 < N) : 0 < avgPathLength N := by
proof body
Term-mode proof.
68 unfold avgPathLength
69 have h_log_N_pos : 0 < Real.log N := Real.log_pos h
70 have h_log_phi_pos : 0 < Real.log phi := Real.log_pos one_lt_phi
71 exact div_pos h_log_N_pos h_log_phi_pos
72
73/-- Path length grows logarithmically in `N`. -/