PRCNativeCostSignedAdmissibleCharacterRigidityTarget
plain-language theorem explainer
Packages the signed-admissible character rigidity claim: every signed-admissible ratio-orbit character generates a cost cross-equivalent to the canonical rational J-cost on every orbit. Foundation work cites it when closing native cost uniqueness after sign erasure is excluded. The body is a Prop definition; the companion theorem discharges it by orientation case split.
Claim. For every map $\chi$ on ratio orbits that is a signed-admissible character (admissible interface plus signed-unit calibration), and every ratio orbit $q$, the character-generated cost $J(\chi(q))$ is cross-equivalent to the canonical rational cost $J(q)=\frac{q+q^{-1}}{2}-1$.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed integer numerator over a nonzero distinction-nat denominator. Cross-equality is the internal PRC rational relation: two orbits match when cross-scaled numerators balance as signed orbits (K4.10).
The rational J-cost on a ratio orbit is $J(q)=((q+q^{-1})/2)-1$, realized as the orbit object onRatioOrbit. A character $\chi$ generates a cost by composing: $\mathrm{cost}_\chi(q):=J(\chi(q))$. The identity character recovers the canonical cost.
Signed-admissible characters strengthen the unsigned admissible interface by requiring explicit preservation of the signed unit. The module isolates this repaired interface because unsigned admissibility alone cannot force signed-unit calibration (Pass 279).
proof idea
Definitional packaging only: the declaration is the universal Prop that every signed-admissible character $\chi$ satisfies $\mathrm{crossEq}(J(\chi(q)),J(q))$ for all ratio orbits $q$. No proof obligations live here. Discharge is deferred to the companion theorem, which splits on global orientation of the signed-admissible character and applies orbit congruence of $J$ or transitivity of cross-equality.
why it matters
This is the repaired rigidity target after sign erasure is excluded: character-generated cost becomes canonical everywhere. It feeds the proved companion theorem that closes the target, the Pass-25 native-cost uniqueness blocker certificate (which splits remaining gaps into exact Lean targets), and the universal-foundation open-target ledger.
In the broader RS chain this sits under T5 J-uniqueness: the cost shape $J(x)=(x+x^{-1})/2-1$ must be forced, not merely postulated. Signed admissibility is the interface that makes character rigidity hold on the native rational side before analytic bridging. Negative ledger entries nearby record routes (zero-calibrated unsigned factorizations) that cannot force the final surface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.