rclLHS
plain-language theorem explainer
Left-hand side of the Recognition Composition Law on ratio orbits: J(xy) + J(x/y), with J the PRC rational cost ((q+q^{-1})/2)-1. Used by the algebraic RCL surface theorem and the PRC cost certificate. Pure definitional assembly: apply J to the product and the quotient, then add in the ratio-orbit monoid.
Claim. For ratio orbits $x,y$, define the left-hand side of the composition law by $\mathrm{LHS}(x,y) := J(xy) + J(x/y)$, where $J(q) = ((q + q^{-1})/2) - 1$ is the rational J-cost on ratio orbits and division is multiplication by the reciprocal.
background
Primitive Recognition Calculus works with ratio orbits: integer numerator over a nonzero orbit denominator (K4.7). These are the native rational objects before any real embedding.
The PRC J-cost on a ratio orbit is the orbit-level object $J(q) = ((q + q^{-1})/2) - 1$. It is not yet the real-analytic uniqueness theorem; that bridge sits downstream. Division of ratio orbits is multiplication by the reciprocal.
The Recognition Composition Law (RCL) is the functional equation $J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y)$. This definition packages the left-hand side as a single ratio-orbit expression so the algebraic surface identity can be stated by cross-equality of two orbits.
proof idea
Definitional, not a proof. Form the product $xy$ and the quotient $x/y$ in the ratio-orbit structure, apply the rational J-cost to each, then add the two resulting orbits. No lemmas are invoked beyond the constructors for multiplication, reciprocal-based division, J-cost, and addition.
why it matters
Feeds canonical_rcl_surface, which states that the canonical PRC J-cost satisfies RCL algebraically on nonzero ratio orbits ("the rational surface of the composition law, not the continuous-real uniqueness theorem"). Also appears in the PRC cost certificate structure that packages the rational formula and the real J-cost bridge.
In the forcing chain this is the rational skeleton under T5 J-uniqueness: once the surface identity holds on orbits and the real bridge is in place, the unique cost solving RCL is forced to be $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). Without a named LHS object the algebraic RCL statement cannot even be written at the orbit level.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.