PRCPrimeSignedStrengthenedNativeCostUniquenessTarget
plain-language theorem explainer
Defines the uniqueness target for native cost after prime-axis and sign calibrations: any map F on ratio orbits obeying the prime-signed strengthened hypotheses must agree with the canonical cost on every orbit via cross-equality. Cited by the continuum-price residue wall and by the zero-flat refutation. The body is a pure Prop packaging, not a proved uniqueness theorem.
Claim. The prime-signed strengthened native-cost uniqueness target asserts: for every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the prime-signed strengthened native-cost hypotheses, then for every ratio orbit $q$ one has cross-multiplication equality $F(q) \simeq C(q)$, where $C$ is the canonical native cost on ratio orbits.
background
In the Primitive Recognition Calculus, costs are carried on ratio orbits: pairs of a signed integer orbit numerator and a nonzero distinction-nat denominator. Two orbits are identified by crossEq, the internal PRC rational relation: cross-multiplication of numerators and denominators balances as signed orbits (K4.10). The canonical native cost on this carrier is onRatioOrbit, the J-cost display pulled back to ratio orbits.
Earlier uniqueness targets (base ledger, then strengthened by prime-pair products) were shown insufficient: each admits countermodels. The present target is the next repair. Its hypotheses package both sign calibration and every-prime-axis calibration at the native-cost level, after the zero-flat and absolute-value no-gos. The module sits in the foundation layer that isolates what continuum-style one-point calibration must be purchased by infinite independent δ-native checks.
proof idea
Definitional packaging only. The Prop is the universal quantification: every $F$ obeying PRCPrimeSignedStrengthenedNativeCostHypotheses is pointwise cross-equal to the canonical onRatioOrbit. No tactics or lemmas are invoked in the body; discharge of the target is left to downstream theorems (character factorization implies the target) or to explicit refutation.
why it matters
This is the third rung on the native-cost uniqueness ladder inside the continuum-price residue argument. Downstream, ContinuumPriceResidueWall records prime_signed_insufficient : ¬ this target, alongside base and strengthened failures: what ContinuousOn plus one-point calibration buys for J-cost uniqueness (T5 / law_of_logic_forces_jcost) the δ-native carrier must buy as an infinite independent calibration family.
The target is explicitly refuted by PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_refuted: without zero-orbit calibration the zero-flat countermodel satisfies the prime-signed hypotheses yet displays $0$ at the zero orbit where the canonical cost displays $-1$. Positive routes exist too: character factorization (and the signed-admissible intermediate) imply the target via crossEq transitivity. The open pressure is therefore zero-orbit calibration, not further prime-axis work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.