PRCZeroCalibratedNativeCostUniquenessTarget_of_signed_admissible_factorization
plain-language theorem explainer
Given a signed-admissible character factorization of zero-calibrated native costs on ratio orbits, every such cost is cross-equal to the standard on-orbit cost. Cite this when reducing native-cost uniqueness in the Primitive Recognition Calculus to factorization plus character rigidity. The argument is a short term proof: unpack the factor character, then chain cross-equality through the proved rigidity theorem.
Claim. Assume that every map $F$ on ratio orbits that satisfies the native-cost hypotheses and whose doubled trace is zero-calibrated factors, up to cross-equality, as the cost of some signed admissible ratio character. Then every such $F$ is cross-equal, at every ratio orbit $q$, to the standard on-orbit cost of $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is a rational display: a signed-orbit numerator over a nonzero distinction-nat denominator. Cross-equality is the choice-free equivalence on ratio orbits obtained by clearing denominators through an integer bridge (transitivity is crossEq_trans).
A native cost is a map $F$ on ratio orbits obeying the PRC native-cost hypotheses; its doubled trace is the associated d'Alembert-type functional. Zero calibration means that doubled trace vanishes at the neutral point. The standard comparison object is the on-orbit cost map; costs may also be rebuilt from a ratio character via costFromCharacter.
The factorization target asserts that any zero-calibrated native cost factors through some signed admissible character. The uniqueness target asserts that any such cost agrees with the on-orbit cost under cross-equality. This theorem is the implication from the former Prop to the latter.
proof idea
Fix $F$, the native-cost hypotheses, zero calibration of the doubled trace, and a ratio orbit $q$. Apply the factorization hypothesis to obtain a signed admissible character $\chi$ with $F(q)$ cross-equal to the character cost of $q$. The already-proved signed-admissible character rigidity theorem supplies cross-equality of that character cost with the standard on-orbit cost at $q$. Finish by transitivity of cross-equality (crossEq_trans).
why it matters
Native-cost uniqueness is the PRC-side counterpart of J-cost uniqueness in the forcing chain (T5: $J(x)=(x+x^{-1})/2-1$). This lemma closes the last glue step once factorization is available: uniqueness of the zero-calibrated native cost reduces to existence of a signed admissible character factor plus the rigidity theorem already proved in-module.
No downstream consumers are wired yet (used_by is empty), so the declaration currently sits as a proved reduction inside PRCNativeCostUniqueness. It does not itself discharge the factorization target; that remains the substantive open obligation on the uniqueness path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.