phi_mul_inv
plain-language theorem explainer
The theorem establishes that the golden ratio φ satisfies φ ⋅ φ⁻¹ = 1. Researchers modeling the phi-ladder lattice and reciprocal symmetries in Recognition Science cite this identity when manipulating phi-powers on the multiplicative half-line. The proof is a direct one-line application of the multiplicative inverse cancellation lemma to the prior fact that φ is nonzero.
Claim. $φ ⋅ φ^{-1} = 1$, where $φ = (1 + √5)/2$ is the golden ratio.
background
The phi-ladder lattice is the discrete hierarchy of complexity levels forced by RS theorem T6. On the positive reals it is the geometric sequence {φ^r : r ∈ ℤ}; on the log scale t = log x this becomes the additive lattice {r ⋅ log φ : r ∈ ℤ} that admits Poisson summation. The module formalizes phi as the golden ratio, phiRung as the rung index, and phiLatticeReciprocal as the involution r ↦ -r that corresponds to x ↦ 1/x. This theorem supplies the basic multiplicative inverse property required for that symmetry. It depends on the upstream lemma phi_ne_zero : phi ≠ 0, which itself follows from phi_pos.
proof idea
The proof is a one-line term that applies the multiplicative inverse cancellation lemma mul_inv_cancel₀ directly to the hypothesis phi_ne_zero.
why it matters
This identity realizes the self-duality of reciprocal symmetry on the phi-ladder, allowing the rung map r ↦ -r to correspond to φ^r ↦ φ^{-r}. It supports the module's key results including phi_inv_eq_phi_minus_one, cost_at_phi_pow_eq, and cost_phi_ladder_reciprocal. In the broader framework it supplies the algebraic content of T6 (self-similarity forces φ) and the Recognition Composition Law's compatibility with inversion. The module notes that the analytic content (phi-Poisson summation) remains a hypothesis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.