cost_phi_ladder_reciprocal
plain-language theorem explainer
The theorem establishes invariance of the cost function on the phi-ladder under rung negation: cost at φ to the power -r equals cost at φ to the power r for any integer r. Lattice analysts working on self-dual properties of the Recognition Science hierarchy would cite it when assembling the structural certificate for the phi-lattice. The proof is a one-line wrapper that unfolds the reciprocal definition and invokes the pre-proved equality cost_at_phi_pow_eq_neg.
Claim. The cost function on the phi-ladder satisfies $J(φ^{-r}) = J(φ^r)$ for every integer $r$.
background
The phi-ladder lattice consists of the points φ^r for r ∈ ℤ on the positive reals (equivalently the additive lattice r · log φ on the log scale). This module defines φ = (1 + √5)/2, the rung map phiRung, the lattice points phiLatticePoint, and the reciprocal involution phiLatticeReciprocal that sends r to -r. The function costAtPhiPow extracts the J-cost at these points. Upstream results supply the identity event at zero cost, the active edge count A = 1, and the projection-defect hypothesis from the CPM2D bundle. The module packages Sub-conjecture A.2 as the hypothesis structure PhiLadderPoissonSummation for the analytic content of Poisson summation on this lattice.
proof idea
The proof unfolds the definition of phiLatticeReciprocal (which negates the rung index) and then applies the lemma cost_at_phi_pow_eq_neg to obtain the required equality.
why it matters
This theorem is invoked by phi_ladder_certificate, the theorem that assembles the complete list of structural facts about the phi-ladder lattice. It supplies the self-duality step needed for the phi-Poisson summation hypothesis in Sub-conjecture A.2. Within the Recognition Science framework it confirms the reciprocal symmetry forced by T6 (self-similarity fixes φ) and supports the eight-tick octave structure together with the D = 3 spatial dimension count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.