PRCStrengthenedNativeCostUniquenessTarget
plain-language theorem explainer
Any map on ratio orbits that obeys the strengthened native-cost hypotheses must agree with the canonical J-cost display under cross-multiplication equivalence. This Prop replaces a refuted weaker uniqueness claim in the primitive recognition calculus. Selection lemmas and the continuum-price residue wall cite it as the statement to discharge or refute. The declaration is pure definition: a quantified target with no proof obligations of its own.
Claim. For every map $F$ from ratio orbits to ratio orbits, if $F$ satisfies the strengthened native cost hypotheses, then for every ratio orbit $q$ one has cross-multiplication equivalence $F(q)\sim\mathrm{onRatioOrbit}(q)$ (signed-orbit balance of cross products of numerators and denominators).
background
In the primitive recognition calculus (PRC), rational data live as ratio orbits: a signed-orbit numerator over a nonzero distinction-nat denominator. Two such displays are identified by cross-equivalence when the scaled products of numerator and denominator balance as signed orbits; that is the internal rational equality on $\delta$-orbit positions.
The native cost display on a ratio orbit is the J-cost pulled back to that carrier (onRatioOrbit). Observer and multiplicative-recognizer layers elsewhere treat cost as J-cost of a recognition event or of a comparator on positive ratios; here the same cost is expressed entirely in the $\delta$-native language.
The strengthened native-cost hypotheses package the cost-level constraints used after the older uniqueness claim was refuted, including prime-pair field data at the cost level. The present definition simply names the uniqueness conclusion those hypotheses are asked to force.
proof idea
Definitional, not a proved theorem. The body is the universal Prop: quantify over maps $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$, assume the strengthened native-cost hypotheses on $F$, and demand cross-equivalence of $F(q)$ with the native cost orbit of every $q$. No tactics or lemmas fire at this site; downstream theorems inhabit or refute the Prop by discharging those hypotheses under extra factorization and calibration assumptions.
why it matters
This is the replacement uniqueness target after the old native uniqueness statement failed. It sits on the path toward T5-style J-uniqueness inside the $\delta$-native carrier rather than on continuous real functions.
Many implication theorems in the same module prove the target from character factorization plus two-point calibration together with admissible rigidity, global orientation, signed-unit calibration, prime coherence, or coherent global propagation. The continuum-price residue wall records the negative: even this strengthened target remains insufficient on the base ledger, so uniqueness still demands an infinite independent calibration family rather than a finite native package. That wall is the prereg residue of what continuous one-point calibration buys in the classical J-cost forcing law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.