PRCZeroCalibratedNativeCostUniquenessTarget_of_character_targets
plain-language theorem explainer
Zero-calibrated native costs on ratio orbits are unique once they factor through a ratio character and that character is rigid at the two-point. Anyone proving the PRC native cost is forced to the canonical identity-character cost cites this glue step. The argument is a short transport: factor, calibrate at two by crossEq, then apply rigidity and transitivity.
Claim. Assume every zero-calibrated native cost $F$ factors as a ratio-character cost, and every ratio character calibrated at the orbit $2$ agrees with the canonical identity-character cost. Then any $F$ satisfying the native-cost hypotheses and zero-calibrated doubled-trace condition obeys $F(q)\sim q$ (cross-multiplication equivalence) for every ratio orbit $q$.
background
In the Primitive Recognition Calculus, costs act on RatioOrbit displays: signed-orbit numerators over nonzero distinction denominators. Equality of displays is the internal relation crossEq (K4.10): cross-multiplication balance of scaled signed orbits, not classical $\mathbb{Q}$ equality.
A native cost $F$ is a map on ratio orbits obeying the PRC native-cost hypotheses. Its doubled-trace form can be zero-calibrated. The canonical comparison object is the identity-character cost onRatioOrbit. Character costs are built by costFromCharacter from a PRCRatioCharacter $\chi$.
Two interface targets package the remaining work: factorization (every zero-calibrated native $F$ is crossEq to some character cost) and rigidity (a character cost calibrated at the orbit two must be the identity character everywhere). The rigidity target is documented as the blocker that eliminates prime-direction freedom.
proof idea
Term-mode proof by introduction and transport along crossEq.
Fix $F$, its native hypotheses, zero-calibration, and a query orbit $q$. Apply the factorization hypothesis to obtain a ratio character $\chi$ with $F\sim\mathrm{costFromCharacter},\chi$ pointwise. At the orbit two, symmetrize the factorization identity and compose (via crossEq_trans) with $F$'s two-calibration to get that $\chi$'s character cost is calibrated at two. Feed that calibration into the rigidity hypothesis to conclude $\mathrm{costFromCharacter},\chi\sim\mathrm{onRatioOrbit}$ at $q$. One more crossEq_trans with the factorization identity at $q$ yields $F(q)\sim\mathrm{onRatioOrbit}(q)$.
why it matters
This closes the uniqueness target for zero-calibrated native costs in PRC: under the two named interface hypotheses, the only such cost is the canonical identity-character cost on ratio orbits. That is the PRC-side counterpart of J-uniqueness (forcing chain T5), where the cost is forced rather than chosen.
No downstream consumers are wired yet (used_by is empty), so the declaration presently seals the uniqueness Prop itself. It sits between character factorization and character rigidity; discharging those two targets is what would finish forcing the native cost to onRatioOrbit without residual prime-direction freedom. Framework-wise it supports the claim that recognition cost is unique once zero-calibration and the composition law structure are fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.