phiLatticePoint_reciprocal
plain-language theorem explainer
The reciprocal map on phi-ladder rungs sends each integer rung r to -r, so the associated lattice point on the log scale is negated. Modelers of the phi-ladder in Recognition Science cite the result when verifying inversion symmetry before applying Poisson summation. The proof is a one-line wrapper that unfolds the reciprocal definition and invokes the already-proved negation property of the lattice points.
Claim. For every integer rung $r$, the phi-ladder lattice point at the reciprocal rung equals the negation of the lattice point at rung $r$: let $l(r) := r log phi$, then $l(-r) = -l(r)$.
background
The phi-ladder is the geometric sequence of powers of the golden ratio forced by RS theorem T6. On the log scale it becomes the additive lattice $r log phi$ for $r in Z$. The definition phiLatticePoint(r) returns exactly this value $r log phi$. The map phiLatticeReciprocal is the involution $r mapsto -r$, the discrete counterpart of the inversion $x mapsto 1/x$ on the multiplicative half-line.
proof idea
The proof is a one-line wrapper. It unfolds the definition of phiLatticeReciprocal (which replaces the argument by -r) and then applies the upstream theorem phiLatticePoint_neg, whose own proof is an unfolding plus ring arithmetic after casting.
why it matters
This supplies the lattice-level statement of reciprocal symmetry required by the Recognition Composition Law. It is the direct prerequisite for the module's later results cost_at_phi_pow_eq and cost_phi_ladder_reciprocal, which establish that the J-cost is even on the phi-ladder. In the broader framework it realizes the involution needed for the phi-Poisson summation hypothesis structure stated in the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.