log_phi_inv
The theorem states that the natural logarithm of the reciprocal of the golden ratio equals the negative of the logarithm of the golden ratio. Researchers formalizing reciprocal symmetry on the phi-ladder lattice in Recognition Science cite it when mapping rung r to -r under x to 1/x. The proof is a one-line wrapper applying the standard real-analysis identity for the logarithm of a reciprocal.
claim$log(φ^{-1}) = -log φ$
background
The phi-ladder lattice is the geometric sequence {φ^r : r ∈ ℤ} on the positive reals, forced by RS theorem T6 as the self-similar fixed point. On the log scale this becomes the additive lattice {r · log φ : r ∈ ℤ}, which admits Poisson summation and encodes the reciprocal involution r ↦ -r. The module establishes the basic algebraic facts needed for cost-function symmetry under this map, including φ > 1 and φ^{-1} = φ - 1.
proof idea
The proof is a one-line wrapper that applies the Mathlib lemma Real.log_inv directly to phi.
why it matters in Recognition Science
This identity is required to prove that the cost J is invariant under rung negation, J(φ^r) = J(φ^{-r}), which feeds the reciprocal-symmetry theorems cost_at_phi_pow_eq and cost_phi_ladder_reciprocal. It supplies the logarithmic counterpart of the lattice involution described in the module documentation and aligns with the self-duality built into the Recognition Composition Law.
scope and limits
- Does not compute a numerical value for log φ.
- Does not address complex logarithms or branch cuts.
- Does not prove positivity of log φ (handled by a sibling theorem).
- Does not derive summation or Poisson properties of the lattice.
formal statement (Lean)
119theorem log_phi_inv : Real.log phi⁻¹ = -Real.log phi := by
proof body
Term-mode proof.
120 exact Real.log_inv phi
121
122/-! ## The phi-ladder lattice -/
123
124/-- The phi-ladder lattice point at integer rung `r`: the value
125 `r · log φ` on the log-scale (= `log(φ^r)`). -/