PRCZeroCalibratedNativeCostCharacterFactorizationTarget_not_old
plain-language theorem explainer
The zero-calibrated discrete d'Alembert factorization of PRC-native costs holds, while the uncalibrated factorization target is false. Cite this when separating the corrected uniqueness path from the original blocker. The proof is a one-line pairing of the positive zero-calibrated theorem with the refutation of the old target.
Claim. The zero-calibrated native-cost character factorization holds, and the uncalibrated one fails: for every map $F$ on ratio orbits satisfying the PRC-native cost hypotheses, if the doubled trace of $F$ is zero-calibrated, then there exists a ratio character $\chi$ such that $F(q)$ is cross-equal to the cost built from $\chi$ at every orbit $q$; without the zero-calibration hypothesis the same universal claim is false.
background
In the Primitive Recognition Calculus, admissible native costs are maps $F$ on ratio orbits obeying the PRC-native cost hypotheses (the discrete stand-in for the Recognition Composition Law / d'Alembert structure). The first exact blocker asked that every such $F$ factor through a ratio character $\chi$: $F(q)$ cross-equal to $\mathrm{costFromCharacter}(\chi,q)$ for all $q$. That is the discrete d'Alembert factorization step.
That uncalibrated target is too strong. The corrected target adds zero-calibration of the doubled trace of $F$ (the native cost's doubled-trace functional sits at the calibrated origin). Upstream, the uncalibrated target is refuted by reduction to a failed character-trace lift; the zero-calibrated target is proved by lifting through the zero-calibrated character-trace theorem and recovering the cost match.
proof idea
One-line term proof: pair the two already-established results. The left conjunct is PRCZeroCalibratedNativeCostCharacterFactorizationTarget_proved (introduces $F$, native hypotheses, and zero-calibration, then obtains $\chi$ from the zero-calibrated character-trace lift and matches costs). The right conjunct is PRCNativeCostCharacterFactorizationTarget_refuted (assumes uncalibrated factorization and derives a contradiction via the failed character-trace lift). No new algebra is done here.
why it matters
This declaration records the status split that replaces the original discrete d'Alembert factorization blocker: zero-calibration is necessary and sufficient for the character factorization route in PRC native-cost uniqueness, while the bare target is dead. It sits on the path toward uniqueness of the native cost that feeds J-uniqueness (forcing-chain T5: $J(x)=(x+x^{-1})/2-1$) and the Recognition Composition Law. No downstream consumers are wired yet; the value is archival clarity for the uniqueness module, so later uniqueness theorems cite the calibrated target rather than the refuted one.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.