PRCSignedStrengthenedNativeCostHypotheses
plain-language theorem explainer
Packages strengthened native-cost axioms with direct calibration at the signed unit −1. Uniqueness arguments for the canonical cost on rational ratio orbits cite this as the working hypothesis class after the absolute-value counterexample. Pure Prop structure: two prior interfaces conjoined; no proof content.
Claim. For a map $F$ on rational ratio orbits, the signed strengthened native-cost hypotheses hold when $F$ satisfies the strengthened native-cost interface (reciprocity/RCL, normalization, base calibration, and prime-pair product calibration at the cost level) and, in addition, $F$ matches the canonical cost at the signed unit: $F(-1)\sim_{\mathrm{cross}} J(-1)$.
background
In the primitive recognition calculus, costs act on ratio orbits: integer numerator over a nonzero distinction-orbit denominator. The native cost interface encodes the Recognition Composition Law (RCL), normalization, and calibration probes so that the unique continuous solution is the J-cost $J(x)=(x+x^{-1})/2-1$ (forcing step T5).
After a two-adic no-go, the strengthened interface keeps those fields and adds prime-pair product calibration at the cost level. A further absolute-value no-go shows that positive prime and prime-pair probes alone are insufficient: the absolute-value generated cost satisfies the unsigned package yet fails at $-1$.
Signed-unit calibration therefore demands that $F$ agree with the canonical on-orbit cost at the negative unit orbit. This structure is exactly the conjunction of the strengthened package with that signed-unit field.
proof idea
Definitional structure, not a proved theorem. The body is the Prop pairing two fields: the strengthened native-cost hypotheses (themselves native hypotheses plus prime-pair product calibration) and the signed-unit calibration predicate, which is the single cross-equality $F(-1)\sim$ canonical cost at $-1$. No tactics or lemmas are invoked at this declaration.
why it matters
This is the post-pass-281 repaired target class: uniqueness is asked only of native costs that also calibrate the signed unit. Downstream, the slim cost-selection package builds zero-calibrated signed-strengthened hypotheses on top of it and states pointwise crossEq uniqueness of the canonical cost for that class. Certificates use it for non-vacuity of the sans-zero class, for the bridging iff with zero-orbit calibration, and to refute dropping the sign field (the absolute-value cost inhabits the unsigned package but not this one). It sits on the path to T5 J-uniqueness inside the native PRC ledger, closing the absolute-value loophole without restoring the deleted all-prime axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.