recip_pins_unit_and_scale
plain-language theorem explainer
The reciprocal involution ι(x)=1/x pins both framework constants at once: its fixed points are exactly the zeros of the recognition cost J (the unit 1), and the fixed points >1 of the affine shift 1+ι are exactly φ. Anyone citing the structural bridge between cost symmetry and golden-ratio forcing uses this. The proof is a term-mode pair that packages two prior fixed-point characterizations.
Claim. For every real $x>0$, $\iota(x)=x$ if and only if $J(x)=0$; and for every real $x>1$, $(1+\iota)(x)=x$ if and only if $x=\varphi$, where $\iota(x)=x^{-1}$, $J(x)=(x+x^{-1})/2-1$, and $\varphi$ is the golden ratio.
background
This module isolates a single generator beneath two otherwise separate RS landmarks: the recognition cost $J$ and the golden ratio $\varphi$. The generator is the reciprocal involution $\iota(x)=x^{-1}$ on the positive reals (dual-recognition symmetry). Module setup: $J$ is the $\iota$-symmetric cost ($J\circ\iota=J$), and $\varphi$ is the unique fixed point $>1$ of the $\iota$-shift $g(x)=1+\iota(x)$.
Upstream, $J$ is the standard RS cost $J(x)=(x+x^{-1})/2-1$ (zero only at the unit ratio). The reciprocal appears both as a bare map on $\mathbb{R}_{>0}$ and as the reciprocal automorphism in the cost algebra. Sibling lemmas already characterize fixed points: $\iota(x)=x$ iff $J(x)=0$ on positives, and $g(x)=x$ iff $x=\varphi$ for $x>1$. The present theorem simply conjoins those two characterizations under one statement about the same $\iota$.
proof idea
Term-mode pair constructor. The left conjunct is discharged by applying the sibling recip_fixed_iff_cost_zero at the positivity hypothesis. The right conjunct is discharged by applying the sibling recipShift_fixed_iff at the hypothesis $x>1$. No further algebra: the theorem is the packaging of those two fixed-point equivalences into a single conjunction.
why it matters
Doc-comment calls this the sharpest form of the bridge: unit and scale, the two constants the framework is built from, are the two fixed points of one involution family ($\iota$ fixes the unit $=J$'s null point; $1+\iota$ fixes $\varphi$). That is the structural content behind T5 (J-uniqueness via the cost form tied to reciprocal symmetry) and T6 ($\varphi$ forced as the self-similar fixed point).
In-module, it sits beside recip_generates_cost_and_scale and feeds the certificate ReciprocalGeneratorCert / reciprocalGeneratorCert_holds, which bundles the involution law, both downstream forcings, and the witness that $\varphi$ solves the $\iota$-shift equation. Even with no external used_by edges yet, it is the named pin that turns an assembly of unrelated facts into a deduction from one generator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.