log_phi_pos
plain-language theorem explainer
The theorem establishes that the natural logarithm of the golden ratio is strictly positive. Ecologists deriving species-area exponents and gravitational physicists constructing horizon states cite it to fix the sign of log-lattice spacings. The proof is a direct one-line application of the library lemma Real.log_pos to the sibling fact that phi exceeds one.
Claim. $0 < log φ$ where $φ = (1 + √5)/2 > 1$.
background
The phi-ladder lattice is the geometric sequence {φ^r : r ∈ ℤ} on the positive reals, converted by logarithm to the additive lattice {r · log φ} in ℝ. This structure is forced by Recognition Science theorem T6 (self-similarity fixes the golden ratio) and supports Poisson summation on the log scale. The module records the elementary ordering facts needed before reciprocal symmetry and cost equality on the ladder can be stated. The identical statement appears upstream in BiodiversityScalingFromJCost with the hypothesis named one_lt_phi.
proof idea
The proof is the term Real.log_pos phi_gt_one. It applies the standard library fact that log is positive exactly when its argument is greater than one, using the already-proved sibling theorem phi_gt_one.
why it matters
This ordering is required by the BiodiversityScalingCert structure and by species_area_exponent_pos in Ecology.BiodiversityScalingFromJCost; it is also invoked in BlackHoleHorizonStates. It confirms that rung index increases with log-lattice position, a direct consequence of T6 and the eight-tick octave. No open scaffolding remains for this elementary sign fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.