recip_fixed_iff_cost_zero
plain-language theorem explainer
For positive reals, the reciprocal involution fixes x exactly when the recognition cost J vanishes at x; both sides hold only at the unit. Anyone treating the reciprocal as the shared generator of cost symmetry and scale will cite this coincidence. The proof is a two-rewrite chain through the fixed-point law for the reciprocal and the zero-set characterization of J.
Claim. For every real $x > 0$, $x^{-1} = x$ if and only if $J(x) = 0$, where $J(x) = \frac{x + x^{-1}}{2} - 1$. Equivalently, both sides hold precisely when $x = 1$.
background
The module isolates the reciprocal involution $\iota(x) = x^{-1}$ on the positive reals as the single structural object upstream of both the recognition cost and the golden-ratio scale. The cost side asserts that $J$ is exactly $\iota$-symmetric; the scale side asserts that $\varphi$ is the unique fixed point greater than 1 of the affine shift $g(x) = 1 + \iota(x)$.
Here $J$ is the standard RS recognition cost $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). Upstream, $J(x) = 0$ holds for positive $x$ if and only if $x = 1$, and the reciprocal's own fixed-point equation is likewise $x = 1$. The present statement identifies those two characterizations: the symmetry axis of $\iota$ coincides with the null set of $J$.
proof idea
One-line rewrite proof. First apply the sibling fixed-point lemma for the reciprocal on positive reals (fixed points of $\iota$ are exactly $x = 1$). Then rewrite by the cost zero-set lemma $J(x) = 0 \leftrightarrow x = 1$ for $x > 0$. The two biconditionals compose to the claimed equivalence. No case splits or arithmetic beyond those two lemmas.
why it matters
This is the sharp cost-side half of the reciprocal-as-generator thesis: not merely $J \circ \iota = J$, but that $\iota$'s fixed point is exactly the zero of $J$. Downstream it is packaged into the conjunction that one involution pins both fundamental constants (unit as cost-zero, and $\varphi$ as fixed point of $1+\iota$), and it is one of the five fields of the reciprocal-generator certificate.
In the forcing chain this sits under T5 J-uniqueness: the cost form $J(x) = (x+x^{-1})/2-1$ is already forced, and here its null set is identified with the fixed locus of the dual-recognition symmetry. That identification is what lets the module claim a genuine common generator rather than a glued pair of independent facts from OneLaw.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.