phi_inv_eq_phi_minus_one
plain-language theorem explainer
The identity φ^{-1} = φ - 1 encodes the discrete self-similarity of the golden ratio in the Recognition Science phi-ladder. Researchers formalizing reciprocal symmetry on complexity hierarchies cite it to confirm that rung inversion r ↦ -r maps φ^r to φ^{-r} compatibly with the cost function. The proof is a short tactic sequence that reduces the claim to the quadratic relation φ² = φ + 1 via ring rewriting, field simplification, and linear arithmetic.
Claim. The golden ratio satisfies $φ^{-1} = φ - 1$.
background
In the NumberTheory.PhiLadderLattice module the golden ratio φ is the positive root of x² - x - 1 = 0. The phi-ladder is the geometric sequence {φ^r : r ∈ ℤ} on ℝ_{>0}; on the log scale it becomes the additive lattice {r · log φ : r ∈ ℤ}, which admits Poisson summation. The reciprocal identity ensures that the involution r ↦ -r on rungs corresponds to x ↦ 1/x while preserving the J-cost structure.
proof idea
The proof invokes phi_sq_eq to obtain φ² = φ + 1 and phi_ne_zero to obtain φ ≠ 0. It rewrites φ(φ - 1) as φ² - φ, substitutes the quadratic identity, normalizes by ring, then applies field_simp followed by linarith on the resulting equality to 1.
why it matters
This supplies the discrete-self-similarity property required by the downstream phi_ladder_certificate, which collects the structural facts (positivity, quadratic identity, reciprocal relation) used by cost_at_phi_pow_eq and phiLatticeReciprocal_involutive. It realizes the self-similar fixed point forced at T6 and supports the reciprocal symmetry that intertwines the phi-ladder with the J-cost function. The module leaves Sub-conjecture A.2 (phi-Poisson summation) as an open hypothesis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.