canonical_rcl_surface
plain-language theorem explainer
On nonzero ratio orbits, the canonical PRC J-cost obeys the Recognition Composition Law as an algebraic identity of rational displays. Cite this for the discrete rational surface of RCL, before any continuous-real uniqueness argument. The proof rewrites cross-equality to rational equality, pushes the display map through orbit add/mul/div, then closes by field simplification and ring normalization.
Claim. Let $x,y$ be ratio orbits with nonzero rational displays. Then the two sides of the Recognition Composition Law, built from the canonical PRC J-cost on the ratio-orbit surface, are equal under cross-multiplication: $\mathrm{LHS}(x,y)$ and $\mathrm{RHS}(x,y)$ represent the same rational.
background
Primitive Recognition Calculus works on ratio orbits: discrete signed-orbit fractions that display as rationals via toRat. Equality of two such orbits is not bare rational equality of displays; it is the internal cross-multiplication relation crossEq, which balances scaled numerators and denominators as signed orbits and is proved equivalent to equality of rational displays.
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 continuous setting (T5). Here the same algebra is stated on the discrete surface: rclLHS and rclRHS assemble the two sides from the canonical orbit-level J-cost (onRatioOrbit) and the orbit arithmetic (add, mul, div by the fixed orbit two).
Upstream, add_toRat, mul_toRat, and the display lemmas for onRatioOrbit, two, and div make the orbit operations commute with the rational verifier. The module's later bridge section explicitly separates this rational surface identity from the continuous positive-real uniqueness theorem.
proof idea
Rewrite the goal via crossEq_iff_toRat_eq, so it suffices to equate rational displays. Unfold rclLHS and rclRHS, then push toRat through three adds and the multiplications that build the RCL sides, using add_toRat, mul_toRat, onRatioOrbit_toRat, and div_toRat. Simplify the constant orbit two by two_toRat. After one more mul_toRat, record that $x\cdot y\neq 0$ from the nonzero hypotheses, clear denominators with field_simp, and finish by ring_nf. Pure algebraic transport: no analysis and no uniqueness argument.
why it matters
This is the algebraic RCL certificate on the PRC rational surface. Downstream, prc_jcost_certificate packages it as the canonical_rcl field of the PRC J-cost certificate ("closed through canonical RCL and bridges honestly to the existing continuous-real uniqueness theorem"). Native cost uniqueness reuses it in costFromCharacter_canonical_rcl and in the zero-flat native-cost hypothesis bundle, so character-induced costs inherit the same composition law.
In the forcing chain this is the discrete footprint of T5 J-uniqueness and the RCL identity $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$, stated before real completion. It does not itself prove continuous uniqueness; it supplies the honest rational surface that the later bridge and classification theorems consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.