PRCSignedStrengthenedNativeCostUniquenessTarget
plain-language theorem explainer
Defines the uniqueness target for native costs that also calibrate the signed unit: any map F on ratio orbits obeying the signed-strengthened native-cost hypotheses must agree with the canonical on-orbit cost under cross-multiplication. Downstream minimality work cites it as a named launch target. The body is a pure Prop abbreviation, not a proof.
Claim. The following uniqueness claim: for every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the signed-strengthened native-cost hypotheses (base native-cost axioms plus signed-unit calibration), then for every ratio orbit $q$ one has cross-multiplication equivalence $F(q) \sim J(q)$, where $J$ is the canonical native cost on ratio orbits.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equivalence crossEq is the internal PRC rational relation: two orbits match when the cross-scaled numerators balance as signed orbits (K4.10). The canonical native cost on ratio orbits is the on-orbit J-cost display.
Recognition cost elsewhere in the monolith is the J-cost of a recognition event (or a sum of ratio weights). The uniqueness program asks when a competing cost map $F$ is forced to equal that canonical display. After pass 281 the target was narrowed: uniqueness is demanded only of native costs that also calibrate the signed unit, not of the weaker base ledger alone.
The surrounding module packages native-cost uniqueness targets, character-factorization bridges, and calibration strengthenings that feed the slim-ledger minimality certificate.
proof idea
No proof: this is a definitional Prop. It quantifies over maps $F : \mathrm{RatioOrbit} \to \mathrm{RatioOrbit}$, assumes the signed-strengthened native-cost hypothesis bundle on $F$, and asserts pointwise cross-equivalence of $F(q)$ with the canonical on-orbit cost. Downstream theorems either inhabit the Prop from stronger factorization premises or refute it by exhibiting a countermodel.
why it matters
This is the named launch target for signed-strengthened native-cost uniqueness in the PRC cost-selection program. Pass 283 and the minimality module refute it: PRCSignedStrengthenedNativeCostUniquenessTarget_refuted shows the zero-flat native cost satisfies every signed-strengthened field (all live on nonzero orbits) yet fails uniqueness. That refutation is recorded in the slim-ledger minimality certificate as necessity of the zero-calibration field, and in the native cost-selection premise ledger as an itemized strength claim.
Conditional recovery paths remain: from signed-admissible character factorization (or character factorization plus two-calibration forcing prime calibration) one can still derive the target. In the broader Recognition framework this sits under T5 J-uniqueness and the Recognition Composition Law: the ledger work isolates exactly which calibration axioms force the canonical $J$ on ratio orbits, versus which admit kernel-checked impostors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.