fixedPointMap
plain-language theorem explainer
Defines the self-dual real map f(x)=1+1/x whose positive fixed point is the golden ratio φ. Baryogenesis staging and any RS argument that ties φ to the per-channel suppression c=φ^{-1} cite this map. The body is a one-line definition; fixed-point and derivative identities are proved downstream.
Claim. Define the real map $f(x)=1+1/x$. (In the Recognition framework this is the self-dual map whose unique positive fixed point is the golden ratio $\varphi$, satisfying $\varphi=1+1/\varphi$.)
background
This module stages honest theorem targets for the Steve baryogenesis derivation. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ with sphaleron equilibration forces vanishing final baryon number.
In Recognition Science the cost functional forces $J(x)=(x+x^{-1})/2-1$ (T5), and the self-similar fixed point of the dual map is $\varphi$ (T6). The map $f(x)=1+1/x$ is exactly that dual iteration: a fixed point solves $x=1+1/x$, hence $x^2-x-1=0$, so the positive root is $\varphi$.
The inline comment records the intended physics reading: the per-channel recognition suppression $c=\varphi^{-1}$ equals $\varphi-1$ from the fixed-point equation, and the contraction rate $|f'(\varphi)|=\varphi^{-2}=c^2$ means one fixed-point step crosses two recognition rungs on the $\varphi$-ladder.
proof idea
Pure definition: the body is the term $1+1/x$. No tactics, no lemmas. Downstream theorems (notably the fixed-point and suppression identity for $\varphi$) unfold this map and discharge the algebraic consequences with real-arithmetic lemmas such as Real.sq_sqrt and positivity of $\varphi$.
why it matters
Gives a named handle for the self-dual map that T6 forces as the source of $\varphi$. The sole immediate consumer is phi_fixed_point_and_suppression_identity, which proves $f(\varphi)=\varphi$ and $1/\varphi=\varphi-1$, locking the suppression factor $c=\varphi^{-1}$ to the fixed-point algebra.
In the baryogenesis lane this is not decorative: recognition-channel suppression and rung counting enter washout and freeze-out bookkeeping. Naming the map keeps those identities honest rather than inlined magic constants. Framework landmarks: T5 $J$-uniqueness, T6 $\varphi$ as self-similar fixed point, and the $\varphi$-ladder mass/suppression calculus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.