PRCPrimeSignedStrengthenedNativeCostUniquenessTarget_of_signed_admissible_factorization
plain-language theorem explainer
If every native cost map that is prime-calibrated and signed-unit-calibrated factors through a signed-admissible ratio character, then that map is uniquely the standard native cost on rational orbits. Foundation workers cite this when closing the strengthened uniqueness target after the sign and prime no-go repairs. The proof is a short term argument: factor, apply signed-admissible character rigidity, and transit cross-equality.
Claim. Assume that every map $F$ on rational orbits satisfying the prime-and-signed strengthened native-cost hypotheses admits a signed-admissible ratio character $\chi$ with $F(q)$ cross-equal to the cost reconstructed from $\chi$ at every orbit $q$. Then every such $F$ is cross-equal to the standard native cost on every rational orbit.
background
In the Primitive Recognition Calculus, rational data are packaged as RatioOrbit: an integer numerator over a nonzero distinction-nat denominator. Equality of two such displays is the choice-free relation crossEq (integer cross-multiplication), which is transitive by routing through an integer bridge and cancelling the middle denominator.
A native cost on orbits is a map $F$ obeying the strengthened hypotheses: prime-axis calibration and signed-unit calibration at the cost level itself (the repairs after the zero-flat and absolute-value no-gos). The uniqueness target asserts that any such $F$ agrees with the standard native cost onRatioOrbit under crossEq.
The factorization hypothesis supplies, for each such $F$, a signed-admissible ratio character $\chi$ whose reconstructed cost matches $F$. Upstream rigidity already proves that every signed-admissible character is itself cross-equal to the standard native cost.
proof idea
Term-mode, three steps. Introduce $F$, the strengthened hypotheses, and an orbit $q$. Unpack the factorization hypothesis to obtain a signed-admissible character $\chi$ with $F(q)$ cross-equal to the cost-from-character of $\chi$ at $q$. Apply the proved signed-admissible character rigidity theorem to get that cost-from-character of $\chi$ cross-equal to the standard native cost at $q$. Close by crossEq_trans.
why it matters
This is the bridge from signed-admissible factorization to the strengthened uniqueness target after both no-go repairs (sign and every prime axis calibrated at native-cost level). The immediate parent is the ordinary-character route: uniqueness from plain character factorization is obtained by first lifting ordinary factorization to signed-admissible factorization, then invoking this theorem.
In the Recognition framework this sits inside the foundation layer that forces the native cost shape feeding J-uniqueness (T5) and the Recognition Composition Law. Closing uniqueness of the calibrated native cost is what lets later layers treat the cost as canonical rather than one of many d'Alembert solutions. The declaration is fully proved; it does not leave a scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.