phiLatticeReciprocal
plain-language theorem explainer
The phi-ladder reciprocal map sends each integer rung index r to -r. This discrete involution is the direct analog of the multiplicative inverse on the positive reals and is cited by proofs establishing cost invariance on the phi-ladder. The implementation is a one-line definition that directly encodes the sign flip without additional computation.
Claim. The reciprocal involution on the phi-ladder rungs is the map sending each integer rung index $r$ to $-r$.
background
The phi-ladder is the geometric sequence of powers of the golden ratio phi, which forms a lattice on the logarithmic scale as described in the module: on the multiplicative half-line the ladder consists of the points phi^r for r integer, becoming the additive progression r · log phi on the log scale. The reciprocal symmetry x to 1/x corresponds exactly to sending rung r to -r. This definition supplies the discrete counterpart to the cost reciprocal operation within the self-similar structure forced by theorem T6.
proof idea
The declaration is a direct definition that assigns to each rung r the value -r. No lemmas or tactics are required beyond the built-in negation on integers.
why it matters
This definition supplies the involution used to prove cost invariance under reciprocal symmetry in cost_phi_ladder_reciprocal and to establish that the map is its own inverse in phiLatticeReciprocal_involutive. It realizes the discrete analog of reciprocal symmetry on the phi-ladder forced by T6 and supports the structural facts in phi_ladder_certificate needed for the phi-Poisson summation hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.