PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved
plain-language theorem explainer
Any native-cost map on ratio orbits whose doubled trace is zero-calibrated factors through a ratio character: the map agrees pointwise under cross-equality with the cost rebuilt from that character. Uniqueness, structural-ledger, and signed-strengthened arguments cite this as the slim base factorization step. The proof lifts the zero-calibrated doubled trace to a matching character, then converts the trace match into cross-equality with the character cost.
Claim. For every map $F$ from ratio orbits to ratio orbits satisfying the native-cost hypotheses, if the doubled trace of $F$ is zero-calibrated, then there exists a ratio character $\chi$ such that for every ratio orbit $q$, $F(q)$ is cross-equal to the cost reconstructed from $\chi$ at $q$.
background
In the Primitive Recognition Calculus, candidate costs are maps $F$ on ratio orbits. Native-cost hypotheses encode the algebraic skeleton expected of a recognition cost (composition, symmetry, and related structure). From such an $F$ one builds a doubled-trace functional; zero-calibration of that doubled trace pins the neutral point so the cost vanishes at the identity scale.
A ratio character $\chi$ is a multiplicative orbit map from which one reconstructs a cost via costFromCharacter. Cross-equality on ratio orbits is the native identification used in place of raw equality of representatives. The local target asserts that zero-calibrated native costs factor through some character in this sense.
Upstream, the zero-calibrated character-trace lift already produces a character whose doubled trace matches that of $F$. A separate conversion lemma turns a character-trace match into pointwise cross-equality between $F$ and the reconstructed character cost. Those two pieces are exactly what this target packages.
proof idea
Short composition, not a new calculation. Introduce $F$, the native-cost hypotheses, and zero-calibration of the doubled trace. Apply the already-proved zero-calibrated character-trace lift to obtain a ratio character $\chi$ together with a trace-match witness between $F$ and $\chi$. Discharge the goal by packaging that same $\chi$ with the conversion lemma that turns a character-trace match into pointwise cross-equality of $F(q)$ with the cost reconstructed from $\chi$ at each orbit $q$.
why it matters
This is the slim factorization step for native-cost uniqueness: base native hypotheses plus zero-calibration already force $F$ to be a character cost. Downstream, the signed-strengthened uniqueness proof opens by invoking it and then transporting pair and sign fields onto the factor character; the structural-ledger terminal uniqueness does the same under structural hypotheses. It is recorded in the native-cost uniqueness blocker certificate and in the conditional universal-foundation certificate.
In the Recognition forcing chain this supports T5 J-uniqueness: once costs factor through characters and rigidity closes, the only surviving cost is the canonical $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) obeying the Recognition Composition Law. The companion not_old theorem stresses that the zero-calibrated target is the live one; the older uncalibrated factorization target is refuted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.