avgPathLength_pos
plain-language theorem explainer
For N greater than 1 the quantity log base phi of N is strictly positive. Network modelers working on scale-free graphs with the Recognition Science phi-recurrence cite this to confirm the small-world path-length scaling is well-defined. The proof is a direct term-mode reduction that unfolds the definition and applies positivity of the logarithm to both numerator and denominator before invoking division positivity.
Claim. For every real number $N > 1$, the quantity $L(N) = {}$log$ N / $log$ phi is positive, where phi denotes the golden ratio.
background
The module derives small-world properties from the phi-recurrence on the recognition graph. It establishes that the degree exponent gamma equals 3 as the unique positive solution of (gamma-1)(gamma-2)=2 and that average path length scales as log_phi N. The definition avgPathLength N := Real.log N / Real.log phi supplies the predicted L(N) = log_phi N. This theorem depends on the upstream result one_lt_phi : 1 < phi, which is established in Constants.lean by direct comparison with the quadratic root.
proof idea
The term proof unfolds avgPathLength, applies Real.log_pos to the hypothesis 1 < N to obtain positivity of the numerator, applies Real.log_pos to one_lt_phi to obtain positivity of the denominator, and concludes with div_pos.
why it matters
The result is required by the SmallWorldFromSigmaCert structure, which packages gamma_eq_3, the fixed-point equation, uniqueness, avgPathLength_pos, and path_log_growth. It supports the small-world property in the Recognition Science network derivation that links the phi-ladder to logarithmic path scaling. The module falsifier concerns networks whose fitted exponents lie outside [2.5, 3.5].
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.