phi_is_recipShift_fixed

This module isolates the reciprocal involution $\iota(x) = x^{-1}$ on the positive reals as the shared generator beneath both the cost functional $J$ and the golden ratio $\varphi$. The module doc states the program explicitly: cost side, $J \circ \iota = J$; scale side, $\varphi$ is the unique fixed point $> 1$ of the $\iota$-shift.

The reciprocal-shift is defined by $g(x) = 1 + \iota(x) = 1 + x^{-1}$. Its fixed-point equation $g(x) = x$ is the self-similarity constraint $x = 1 + 1/x$, the classical characterizing equation of $\varphi$. Upstream, PhiSupport.phi_fixed_point already records that identity for the RS constant $\varphi$; this theorem restates it in the language of recip and recipShift so the certificate can quantify over one shared generator.

Term-mode, four steps. Unfold recipShift and recip to expose $1 + \varphi^{-1}$. Invoke PhiSupport.phi_fixed_point, which states the golden-ratio fixed-point identity in reciprocal form. Rewrite with one_div so the reciprocal matches the unfolded definition, then take symmetry of the equality. No new arithmetic is proved here; the work is alignment of notation with the PhiSupport lemma.

This is the scale-side witness inside the reciprocal-generator certificate. Downstream, reciprocalGeneratorCert_holds fills the field phi_solves with exactly this theorem, alongside involutivity of $\iota$, $J$-symmetry under $\iota$, the cost-zero characterization of the unit, and uniqueness of the fixed point $> 1$.

In the Recognition forcing chain this is the local form of T6: $\varphi$ forced as the self-similar fixed point. The module's point is structural, not numerical: both the cost symmetry axis and the scale ratio are properties of one function $\iota$, so the capstone conjunction is a deduction from a shared generator rather than a glued pair of independent facts. Uniqueness among reals $> 1$ is the sibling recipShift_fixed_iff; existence is this lemma.