PRCNativeCostCharacterRigidityTarget
plain-language theorem explainer
Any ratio character whose generated cost matches the canonical J-cost at the orbit 2 must match that canonical cost on every ratio orbit. Native-cost uniqueness work in the Primitive Recognition Calculus cites this as the second exact blocker: calibration at two is supposed to kill prime-direction freedom. The declaration is only a Prop packaging that universal claim; no proof is attached, and a sibling later refutes the bare form.
Claim. For every map $\chi$ from ratio orbits to ratio orbits that is a ratio character (sends $1$ to $1$ and is multiplicative up to cross-equivalence), if the character-generated cost $J(\chi(2))$ is cross-equivalent to the canonical cost $J(2)$, then for every ratio orbit $q$ one has $J(\chi(q))$ cross-equivalent to $J(q)$.
background
In the Primitive Recognition Calculus, rationals are carried as ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Equality is the internal cross-multiplication relation crossEq, which balances scaled numerators and denominators as signed orbits rather than invoking real equality.
The canonical rational J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, realized as the orbit object onRatioOrbit. A ratio character $\chi$ is a multiplicative endomorphism of ratio orbits (unit at $1$, product preserved up to cross-equivalence). The cost generated by $\chi$ is $J\circ\chi$; the identity character recovers the canonical cost.
This module isolates native uniqueness of that cost. The present target asks whether calibration of a character cost at the distinguished orbit $2$ forces the character cost to equal the canonical cost everywhere, thereby eliminating residual prime-direction freedom.
proof idea
No proof: the declaration is a bare Prop abbreviation. It universally quantifies over endomorphisms $\chi$ of ratio orbits, assumes the ratio-character axioms, assumes cross-equivalence of the character cost with the canonical cost at the orbit $2$, and concludes the same cross-equivalence at every ratio orbit $q$. Downstream lemmas either discharge the Prop from prime-calibration subtargets or refute it by counterexample character.
why it matters
Doc-comment labels this the second exact blocker on the path to native cost uniqueness: after factorization into a character, prime-direction freedom must still be killed. It is one conjunct of the sharpened uniqueness target (factorization and rigidity), and both the ordinary and zero-calibrated uniqueness targets are recovered from the pair of character targets.
It also feeds the Pass-25 blocker certificate and the open-target list in UniversalFoundation. Critically, a sibling theorem refutes the bare target via the absolute-value character (calibrated at two yet non-canonical at $-1$). The framework therefore keeps the Prop as an exact interface while routing uniqueness through refined calibration and admissibility hypotheses rather than this unguarded form. Relative to the forcing chain, this sits under T5 J-uniqueness: it is the rational-orbit attempt to force the identity character before bridging to the real analytic $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.