recip_involutive
plain-language theorem explainer
The reciprocal map ι(x)=x⁻¹ is an involution on the positive reals: applying it twice recovers x. Anyone citing the dual-recognition symmetry as the shared generator of J-cost symmetry and the φ fixed-point equation needs this identity. The proof is a one-line simplification from the definition ι(x)=x⁻¹.
Claim. For every real $x>0$, $\iota(\iota(x))=x$, where $\iota(x)=x^{-1}$.
background
This module isolates the reciprocal involution $\iota(x)=x^{-1}$ on the positive reals as the single structural object upstream of both the cost functional and the golden-ratio scale. The module doc states the program explicitly: $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)$. Both halves of the OneLaw assembly therefore quantify over the same map rather than two unrelated constructions.
Locally, recip is the noncomputable definition $\iota(x)=x^{-1}$ on $\mathbb{R}$. The positivity hypothesis $x>0$ keeps the reciprocal inside the positive ray where the dual-recognition symmetry is stated. Upstream, the same reciprocal idea appears in the primitive recognition calculus on ratio orbits (total reciprocal sending zero to zero), but the present theorem is the classical real-analytic form used by the universal-forcing certificate.
proof idea
One-line tactic proof: unfold recip (which is $x\mapsto x^{-1}$) and simplify. Mathlib's field simplifier discharges $(x^{-1})^{-1}=x$ under the standing positivity hypothesis, so no further lemmas are invoked.
why it matters
Involution is the first field of ReciprocalGeneratorCert, discharged by reciprocalGeneratorCert_holds via involutive := fun _ hx => recip_involutive hx. Without $\iota^2=\mathrm{id}$, the cost-side claim $J\circ\iota=J$ and the scale-side fixed-point analysis of $g(x)=1+\iota(x)$ would not share a common generator. That shared generator is what upgrades the OneLaw conjunction from an assembly of independent facts into a deduction from one dual-recognition symmetry. In the broader forcing chain this sits beneath T5 (J-uniqueness via the RCL) and T6 ($\varphi$ as self-similar fixed point): both cite properties of this same $\iota$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.