PRCNativeCostSignedAdmissibleCharacterRigidityTarget_proved
plain-language theorem explainer
Any signed-admissible ratio character generates a cost cross-equal to the native PRC cost on every rational orbit. Uniqueness and factorization closures in the native-cost ledger cite this rigidity. The proof cases on global orientation (identity versus reciprocal) and finishes with reciprocal symmetry of the native cost.
Claim. For every map $\chi$ from rational orbits to rational orbits that is a signed-admissible ratio character, and every rational orbit $q$, the character-generated cost at $q$ is cross-equal to the native cost on $q$: $\mathrm{cost}_\chi(q)\sim\mathrm{cost}(q)$.
background
In the Primitive Recognition Calculus, a rational orbit is an integer numerator over a nonzero distinction-nat denominator. Cross-equality is the choice-free balanced equivalence on those displays (symmetric and transitive via an integer bridge). The native cost onRatioOrbit is the PRC rational cost; it is reciprocal-symmetric: cost at $q$ matches cost at the reciprocal orbit.
A character $\chi$ on orbits produces a cost by evaluation. Signed-admissible characters exclude sign-erasure pathologies that broke plain admissible rigidity. The target asserts that once signed admissibility holds, the character-generated cost is canonical: cross-equal to the native cost everywhere.
Upstream, global orientation of a signed-admissible character says that at each $q$, $\chi(q)$ is cross-equal either to $q$ or to its reciprocal. Congruence of the native cost under cross-equality and reciprocal symmetry then pin the comparison.
proof idea
Term-mode proof by introduction of $\chi$, signed-admissibility, and $q$. Apply global orientation of signed-admissible characters at $q$, splitting into two cases.
If $\chi(q)\sim q$, congruence of the native cost under cross-equality yields cost-from-character equal to native cost at $q$.
If $\chi(q)\sim\mathrm{recip}(q)$, congruence gives cost-from-character equal to native cost at the reciprocal; reciprocal symmetry of the native cost equates that to native cost at $q$; transitivity of cross-equality closes.
why it matters
This is the repaired admissible-rigidity step: signed admissibility forces the character-generated cost to be the native cost everywhere. Downstream uniqueness theorems reduce factorization hypotheses to this rigidity and transport calibration (zero-calibrated signed strengthened uniqueness, structural ledger uniqueness, prime and signed strengthened uniqueness-from-factorization). The blocker certificate and the no-signed-admissible-factor theorem for absolute-value-generated cost also depend on it.
In the Recognition forcing chain this sits under T5 J-uniqueness: the native cost is the unique object compatible with the composition law once sign is controlled. It closes the character side of the slim ledger that forces $J$, rather than leaving an open admissible gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.