PRCSignedAdmissibleRatioCharacter
plain-language theorem explainer
Packages the repaired admissible ratio-character laws with an explicit signed-unit calibration: the character must fix the orbit of −1. Anyone proving native-cost uniqueness or factorization after the two-adic countermodel cites this interface. It is a pure Prop structure, not a proved theorem; Pass 279 shows the unsigned admissible interface does not imply the signed-unit field.
Claim. A map $\chi$ on rational orbits is a signed admissible ratio character when (i) it is an admissible ratio character (ratio-character laws, prime-direction calibration, and prime-pair product-cost consistency) and (ii) it is signed-unit calibrated: $\chi(-1)\sim -1$ under cross-equality of orbits.
background
In the Primitive Recognition Calculus, a RatioOrbit is a rational display: signed integer numerator over a nonzero distinction-nat denominator. Characters are endomorphisms of this orbit space used to generate candidate native costs via costFromCharacter.
After a two-adic countermodel, the unsigned repaired interface PRCAdmissibleRatioCharacter requires three fields: the basic ratio-character laws, prime-direction calibration, and prime-pair product-cost consistency. That interface still admits both global orientations and does not force behaviour on the signed unit. Signed-unit calibration is the separate demand that $\chi$ fix the orbit of $-1$ under cross-equality; prime-direction data alone cannot force it.
This structure simply conjoins the unsigned admissible package with that signed-unit field, giving the repaired interface used once sign erasure must be excluded.
proof idea
No proof body: the declaration is a structure ... : Prop bundling two fields. Inhabitance is by supplying an admissible ratio character together with a proof that $\chi(-1)$ is cross-equal to $-1$. Downstream lemmas project the fields (e.g. hadm.admissible, hadm.signed_unit) and feed them into orientation-propagation or rigidity arguments.
why it matters
This is the repaired character interface for native-cost uniqueness after Pass 279 showed that unsigned admissibility cannot imply signed-unit calibration (the absolute-value character is the counterexample). Downstream, signed-admissible rigidity (PRCNativeCostSignedAdmissibleCharacterRigidityTarget) asserts that any such $\chi$ generates the canonical cost everywhere. Several factorization targets require a factor through this interface rather than the unsigned one: strengthened, signed-strengthened, prime-signed-strengthened, and zero-calibrated variants. The theorem PRCSignedAdmissibleRatioCharacter_global_orientation lifts the package to global cost orientation via coherent prime-orientation propagation. The negative result PRCNoSignedAdmissibleFactorForAbsValueGeneratedNativeCost shows abs-value-generated cost admits no such factor. In the broader RS forcing chain this sits in the foundation layer that pins the unique J-cost (T5) before $\varphi$ and the eight-tick structure are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.