rclRHS
plain-language theorem explainer
Defines the right-hand side of the Recognition Composition Law on ratio orbits: 2 J(x) J(y) + 2 J(x) + 2 J(y), built from the rational J-cost object and the constant two. Anyone proving the algebraic RCL surface on nonzero ratio orbits cites this. The body is a pure arithmetic expression in RatioOrbit add/mul.
Claim. For ratio orbits $x$ and $y$, the RCL right-hand side is the ratio orbit $$2\,J(x)J(y)+2\,J(x)+2\,J(y),$$ where $J$ is the rational cost $J(q)=((q+q^{-1})/2)-1$ evaluated on ratio orbits.
background
Primitive Recognition Calculus works with ratio orbits: integer numerators over nonzero orbit denominators, the discrete rational display of positive ratios. The module builds a native J-cost on that type before bridging to the continuous real uniqueness theorem.
The cost object onRatioOrbit is the rational formula $J(q)=((q+q^{-1})/2)-1$ as a RatioOrbit expression (subtract one from half the sum of $q$ and its reciprocal). The constant two is the ratio orbit with numerator the orbit of 2 and denominator one. The Recognition Composition Law (RCL) is the functional equation $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$ that forces the J-cost in the T5 uniqueness step of the forcing chain.
This definition packages only the right-hand side of that identity, still entirely inside the ratio-orbit algebra.
proof idea
Definition, not a proof. It nests RatioOrbit multiplication and addition: first form $2\cdot J(x)\cdot J(y)$, then add $2\cdot J(x)$, then add $2\cdot J(y)$, using the local constants two and onRatioOrbit. No lemmas are applied; the expression is the algebraic RHS of RCL.
why it matters
Feeds the theorem that the canonical PRC J-cost satisfies RCL algebraically on nonzero ratio orbits (the rational surface of the composition law, not continuous-real uniqueness). That theorem and the PRC cost certificate both consume this RHS side-by-side with the matching LHS. In the framework it is the discrete stand-in for the right-hand side of RCL, the same identity that underwrites T5 J-uniqueness $J(x)=(x+x^{-1})/2-1$. Closing the rational surface is a prerequisite before the real bridge and the full cost certificate can claim the composition law holds in PRC-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.