costAtPhiPow
plain-language theorem explainer
This definition assigns to each integer rung r the real value of the J-cost function at the phi-ladder point phi to the power r. Researchers formalizing reciprocal symmetry on the phi-ladder cite it when proving invariance under inversion. It is introduced as a direct composition of the J-cost operator with integer exponentiation.
Claim. Define the cost at rung r by $c(r) := J(φ^r)$ for $r ∈ ℤ$, where $J(x) = (x + x^{-1})/2 - 1$ is the Recognition Science cost function and $φ$ is the golden ratio.
background
The phi-ladder lattice is the geometric sequence {φ^r : r ∈ ℤ} on the positive reals, which becomes an arithmetic progression on the log scale and admits Poisson summation. The J-cost is the strictly convex function J(x) = (x + 1/x)/2 - 1 with unique minimum at x = 1, as stated in the PhysicsComplexityStructure upstream result. This definition appears in the module that formalizes the phi-ladder and its reciprocal involution r ↦ -r, drawing on the J-cost calibration from LedgerFactorization and the tier structure from NucleosynthesisTiers.
proof idea
The definition is a one-line wrapper that applies the J-cost operator directly to the term phi raised to the integer power r.
why it matters
This definition feeds the reciprocal symmetry theorem cost_at_phi_pow_eq_neg, which shows J(φ^{-r}) = J(φ^r), and the phi_ladder_certificate that collects the structural facts of the ladder. It supports the self-similarity fixed point forced by T6 and the reciprocal symmetry encoded in the Recognition Composition Law, while leaving open the phi-Poisson summation hypothesis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.