PRCSlimSansPairUniquenessTarget
plain-language theorem explainer
Uniqueness target for maps on ratio orbits that obey the slim ledger without the prime-pair product field: any such F must match the canonical J-cost under cross-equivalence. Downstream refutation and the slim-ledger minimality certificate cite it to show the pair field cannot be dropped. Pure Prop packaging of a quantified claim; no proof content.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the slim sans-pair hypotheses (native cost base, signed-unit calibration, and doubled-trace zero calibration), then for every ratio orbit $q$, $F(q)$ is cross-equivalent to the rational $J$-cost $J(q)=((q+q^{-1})/2)-1$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero orbit denominator. Cross-equivalence equates two such orbits when the signed cross-products of numerators and denominators balance; it is the internal PRC stand-in for rational equality.
The canonical cost on a ratio orbit is the rational J-object $J(q)=((q+q^{-1})/2)-1$, built from orbit addition, reciprocal, and subtraction. The slim sans-pair hypotheses package three calibrations on a candidate cost map $F$: the native cost base, signed-unit calibration, and zero calibration of the doubled trace. They deliberately omit the prime-pair product field.
This module sits in the native-cost minimality certificate layer: it isolates removable calibration fields so each can be shown necessary by exhibiting an impostor when dropped.
proof idea
Definition only: the body is the quantified Prop that every $F$ obeying the slim sans-pair hypotheses agrees with onRatioOrbit under crossEq at every ratio orbit. No tactics, no lemmas applied; it names the uniqueness claim that later theorems refute or package.
why it matters
This target is the claim that base + sign + zero already force the canonical J-cost. Downstream, PRCSlimSansPairUniquenessTarget_refuted shows the claim is false: the two-adic twist satisfies those three calibrations yet fails prime-pair products at the mixed $(2,3)$ orbit, so the pair field cannot be dropped. That negation is wired into SlimLedgerMinimalityCertificate as the pair_field_necessary clause of the field-by-field minimality certificate for the slim ledger.
In the Recognition framework this supports the forcing of the unique J-cost (T5 / RCL) by showing each slim-ledger calibration is load-bearing. Without the pair field, uniqueness fails; the certificate records that necessity alongside the other three removable fields.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.