PRCCharacterSignedUnitCalibrated
plain-language theorem explainer
A ratio-orbit character is signed-unit calibrated when it fixes the orbit of −1 under the internal cross-multiplication relation. Anyone proving native-cost uniqueness or signed-admissible factorization cites this predicate to separate genuine signed characters from absolute-value maps. The body is a one-line Prop abbreviation: χ(−1) ∼ −1.
Claim. A map $\chi$ on ratio orbits is signed-unit calibrated when $\chi(-1)$ is cross-equivalent to the ratio orbit $-1$, i.e. the signed cross-multiplication balance $\mathrm{num}(\chi(-1))\cdot\mathrm{den}(-1)=\mathrm{num}(-1)\cdot\mathrm{den}(\chi(-1))$ holds.
background
In the Primitive Recognition Calculus, ratios are not bare rationals: a ratio orbit packages a signed numerator orbit over a nonzero distinction-nat denominator. Equality of displays is the internal relation crossEq: two orbits match when the scaled numerators balance as signed orbits (cross-multiplication on δ-orbit positions).
Characters here are endomorphisms of the ratio-orbit type used to factor native cost functionals. The signed unit is the distinguished orbit of −1. Calibration on that unit means the character fixes it up to cross-equivalence. The module develops native-cost uniqueness by forcing characters to match the canonical J-cost data; signed-unit calibration is an independent orientation constraint that prime-direction data alone does not supply.
Upstream, the reciprocal constructions (cost algebra and ledger forcing) encode inversion of recognition ratios; the present predicate is the discrete character-level counterpart that pins the sign of that inversion at −1.
proof idea
Definitional abbreviation, not a proved statement. The Prop is exactly one application of ratio-orbit cross-equivalence: evaluate the character at the negative-one ratio orbit and require cross-equivalence with that same orbit. No tactics, no lemmas unfolded in the body.
why it matters
Signed-unit calibration is the missing orientation gate after prime-pair admissibility. Downstream, the absolute-value character is shown not to satisfy it, so absolute-value maps are excluded from the signed uniqueness class. The cost-from-character lemma at −1 forces this calibration whenever the induced cost matches the native display on −1.
Parent targets include the zero-calibrated signed-strengthened native-cost uniqueness proof (slim ledger forces J), the structural-ledger uniqueness terminal, the admissible-character signed-unit target (pass 279: repaired prime-pair fields still do not force this), and the prime-signed strengthened factorization transport. In the Recognition forcing chain this sits under native J-uniqueness (T5 landmark): without fixing −1, factorization can flip global sign and fail to recover the canonical cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.