PRCNativeCostSignedUnitCalibrated
plain-language theorem explainer
Defines the signed-unit calibration condition on a native-cost map of ratio orbits: the image of the orbit of −1 must be cross-equal to the orbit of −1 itself. Minimality and uniqueness certificates for native costs cite it as the repair after the absolute-value no-go, so costs see the signed unit rather than only positive prime probes. The body is a one-line Prop abbreviation via cross-equality at −1.
Claim. A map $F$ from ratio orbits to ratio orbits is signed-unit calibrated when $F$ sends the orbit of $-1$ to an orbit cross-equal to the orbit of $-1$ (i.e., $F$ acts as the identity on the signed unit up to the orbit equivalence).
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits that encode recognition cost data without an a-priori real-valued $J$. Ratio orbits package rational ratios up to the equivalence used by the calculus; crossEq is the equality relation on those orbits (agreement after projection to rationals).
Upstream cost notions (rung-coarsen total cost, multiplicative-recognizer derived cost, observer $J$-cost of a recognition event) all ultimately rest on a non-negative cost of ratios. After an absolute-value no-go, positive prime and prime-pair probes alone do not force the signed unit. The local module therefore strengthens the native-cost interface with an explicit calibration at $-1$.
The companion doubled-trace and character-trace constructions convert such an $F$ into real-valued cost data comparable with the classical $J(x)=(x+x^{-1})/2-1$ uniqueness line (T5) and the Recognition Composition Law.
proof idea
Definitional abbreviation, not a proved theorem. The Prop is exactly the single atomic statement that the image under $F$ of the negative-one ratio orbit is cross-equal to the canonical embedding of that same orbit. No tactics or lemmas fire; consumers unfold or package the field into slim hypothesis structures.
why it matters
This is the signed-unit repair field in the pass-274 native-cost interface. Downstream slim ledgers and certificates (native-cost selection slim premise ledger; PRCSlimSansPairHypotheses, PRCSlimSansRclHypotheses, PRCSlimSansTwoCalibrationHypotheses; Liouville-twist and RCL-spike sans-hypotheses theorems; two-adic generated signed-unit certificate) all require it so that uniqueness/minimality arguments cannot ignore $\mathrm{sign}$.
Framework role: native-cost uniqueness feeds the forcing chain toward T5 $J$-uniqueness and the RCL. Without signed-unit calibration, absolute-value pathologies survive positive-axis probes. The definition closes that gap as a named hypothesis rather than a derived theorem, keeping the slim deposit auditable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.