reciprocal_symmetric
plain-language theorem explainer
The PRC rational cost of a ratio orbit equals the cost of its reciprocal: the two cost displays are cross-equivalent. Anyone forcing or uniquifying the canonical J-cost on rational displays cites this symmetry as the gauge identity J(q) = J(q^{-1}). The proof rewrites cross-equivalence as rational equality, unfolds cost and reciprocal displays, then closes by cases on zero with field simplification and ring.
Claim. For every rational orbit $q$, the native PRC cost of $q$ is cross-equivalent to the native PRC cost of the reciprocal orbit $q^{-1}$. Equivalently, writing $C$ for that cost map on ratio orbits, the rational displays satisfy $C(q)=C(q^{-1})$ as elements of $\mathbb{Q}$.
background
In Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator (K4.7). Two ratio orbits are cross-equivalent when the signed-orbit cross-multiples balance; by K4.10 this internal relation is equivalent to equality of the rational verifier displays.
The native PRC cost map sends each ratio orbit to another ratio orbit whose rational display is the discrete J-cost. Reciprocal inverts a ratio orbit on the nose. The Recognition Composition Law and the forced form $J(x)=(x+x^{-1})/2-1$ both require that cost be invariant under this inversion.
This module assembles that rational cost surface so later continuum results can bridge to the continuous uniqueness theorem for $J$.
proof idea
Rewrite cross-equivalence via the iff with equality of rational displays. Unfold the cost map on both sides and the reciprocal's rational display. Case on whether the rational display of $q$ vanishes: the zero case closes by simp; the nonzero case clears denominators with field simplification and finishes by ring, which is the algebraic identity that the cost formula is reciprocal-invariant.
why it matters
This is the rational reciprocal-symmetry field of the PRC J-cost certificate and the gauge half of the capstone forcing theorem on the completion $R_\delta$: recognition laws force the cost to be canonical $J(x)=(x+1/x)/2-1$, unique up to the identity-versus-reciprocal character gauge. Downstream wrappers restate it as canonical cost reciprocal symmetry; existence of a forced cost on the completion packages it with the definitional equality to the native cost map. Native cost uniqueness uses it for character-generated costs and prime-direction calibration.
In the foundation chain it is the discrete precursor of T5 J-uniqueness: $J(x)=J(x^{-1})$ already holds on ratio orbits before continuum completion, so the one-parameter gauge is available at the rational stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.