cost_at_phi_pow_eq_neg
plain-language theorem explainer
The theorem establishes that the J-cost on the phi-ladder satisfies cost(φ^{-r}) = cost(φ^r) for every integer rung r. Researchers modeling self-similar hierarchies or preparing Poisson summation on the ladder cite this symmetry to confirm invariance under inversion. The proof is a short term-mode reduction that unfolds costAtPhiPow, applies the Jcost_symm lemma after positivity, and simplifies via zpow_neg and inv_inv.
Claim. For every integer $r$, $Jcost(φ^{-r}) = Jcost(φ^r)$, where $Jcost$ is the cost function on positive reals and $φ$ is the golden ratio.
background
The phi-ladder lattice is the geometric sequence {φ^r : r ∈ ℤ} on ℝ>0, which becomes the arithmetic lattice {r · log φ} on the log scale and admits Poisson summation. The cost function is the J-cost J(x) = (x + x^{-1})/2 - 1, which obeys the reciprocal symmetry J(x) = J(x^{-1}) for x > 0 by the Jcost_symm lemma. This theorem belongs to the module formalizing reciprocal symmetry on the ladder, as stated in the module documentation: the phi-ladder intertwines reciprocal symmetry of the cost function.
proof idea
The proof unfolds costAtPhiPow, obtains positivity of φ^{-r} via zpow_pos and phi_pos, rewrites with the Jcost_symm lemma from Cost, applies congr, and finishes with zpow_neg and inv_inv to recover the positive-power case.
why it matters
This result supplies the reciprocal symmetry step that feeds directly into cost_phi_ladder_reciprocal, which states the full invariance of the ladder under the involution r ↦ -r. It closes one link in the Recognition Science chain from T6 (self-similarity forces φ) to the eight-tick octave and D = 3, while preparing the ground for the phi-Poisson summation hypothesis left as a structure in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.