recip_fixed_iff

This module isolates the reciprocal involution $ι(x)=x^{-1}$ on the positive reals as the single generator sitting under both the cost-form theorem and the φ-forcing theorem. The cost side asserts that $J$ is exactly the $ι$-symmetric cost ($J\circι=J$); the scale side asserts that $φ$ is the unique fixed point $>1$ of the $ι$-shift $g(x)=1+ι(x)$. Both halves quantify over the same reciprocal map.

Here $ι$ is written recip. Upstream, Jcost_symm already records $J(x)=J(x^{-1})$ for $x>0$, and several modules (ledger events, multiplicative recognizers, observer forcing) treat reciprocal ratios as the dual-recognition symmetry. The present lemma is the fixed-point fact for that involution alone: before linking fixed points to zero cost, one must know that the only positive solution of $ι(x)=x$ is the unit.

Unfold the definition of the reciprocal map. From $x>0$ obtain $x\neq 0$. Split the biconditional.

Forward: assume $x^{-1}=x$. Multiply both sides by $x$ to get $x^{-1}\cdot x=x\cdot x$, cancel the left side by inv_mul_cancel₀, and conclude $x^2=1$. With $x>0$, nlinarith forces $x=1$.

Backward: substitute $x=1$ and simplify. No external lemmas beyond positivity and field arithmetic are required.

This is the elementary fixed-point half of the cost-side unification. Its sole direct consumer is recip_fixed_iff_cost_zero, whose doc-comment states the sharp claim: for positive $x$, $ι x=x\leftrightarrow J(x)=0$, both holding iff $x=1$. Thus the symmetry axis of $ι$ coincides with the null set of $J$, rather than merely $J$ being $ι$-invariant.

In the broader Recognition framework this pins the unit as the unique zero-cost, self-reciprocal point on the positive line, the reference against which the φ-ladder and the Recognition Composition Law measure cost. It is logically upstream of the module's claim that one involution generates both cost symmetry and the golden-ratio fixed-point equation, and it feeds the ReciprocalGenerator certificate that packages those two sides together.