recipShift_fixed_iff
plain-language theorem explainer
Among reals strictly larger than 1, the map x ↦ 1 + 1/x has a unique fixed point, and that point is the golden ratio φ. Anyone citing the reciprocal-generator unification (cost symmetry and scale from one involution) needs this uniqueness half. The proof reduces the fixed-point equation to x² = x + 1 and invokes the unique positive root of that quadratic.
Claim. For every real $x > 1$, one has $1 + x^{-1} = x$ if and only if $x = \varphi$, where $\varphi$ is the golden ratio (the unique positive root of $t^2 = t + 1$).
background
This module isolates the reciprocal involution $\iota(x) = x^{-1}$ on the positive reals as the single structural generator behind both the recognition cost $J$ and the scale $\varphi$. The cost side is $\iota$-symmetry of $J$; the scale side is uniqueness of the fixed point of the affine shift $g(x) = 1 + \iota(x)$ among reals greater than 1.
Here $g$ is written recipShift. The golden ratio $\varphi$ is already known in the library to satisfy $\varphi = 1 + 1/\varphi$ and to be the unique positive root of $t^2 - t - 1 = 0$. The present statement packages that uniqueness as a fixed-point characterization of $g$ on $(1,\infty)$, matching the module's claim that $\varphi$ is "the unique fixed point $> 1$ of the $\iota$-shift."
Upstream support is elementary real arithmetic plus the PhiSupport uniqueness lemma for the positive root of $x^2 = x + 1$. No cost-function facts are required for this direction.
proof idea
Unfold the shift to $1 + x^{-1}$. From $1 < x$ get $x > 0$ and $x \neq 0$.
Forward: assume $1 + x^{-1} = x$. Multiply both sides by $x$ to obtain $x + 1 = x^2$ (via $x \cdot x^{-1} = 1$). Apply PhiSupport.phi_unique_pos_root to conclude $x = \varphi$.
Reverse: substitute $x = \varphi$ and quote PhiSupport.phi_fixed_point (rewriting $1/\varphi$ as the reciprocal) to recover $1 + \varphi^{-1} = \varphi$.
why it matters
This is the scale half of the reciprocal-generator story. It is plugged directly into three local capstones: recip_generates_cost_and_scale (cost symmetry of $J$ under $\iota$ conjoined with this uniqueness), recip_pins_unit_and_scale (fixed point of $\iota$ is the unit/cost-zero point; fixed point of $1+\iota$ is $\varphi$), and the certificate reciprocalGeneratorCert_holds via its scale_unique field.
In the Recognition forcing chain this is the concrete fixed-point form of T6: $\varphi$ is forced as the self-similar scale, here derived from the same involution that forces $J$'s symmetry axis rather than from an independent hierarchy postulate. The module's point is logical upstreamness: one generator, two forced quantities, not a glued pair of unrelated facts as in the older OneLaw assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.