PRCZeroCalibratedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted
plain-language theorem explainer
Every zero-calibrated native cost on ratio orbits need not factor through a signed admissible ratio character. The absolute-value-generated native cost is a counterexample: it meets the native-cost and zero-calibration hypotheses yet admits no such character. Uniqueness and foundation certificates cite this refutation to block the signed-admissible factorization route. The proof is a one-line specialization of the no-factor lemma to that concrete cost.
Claim. It is false that every map $F$ on ratio orbits satisfying the native-cost hypotheses and with zero-calibrated doubled trace admits a signed admissible ratio character $\chi$ such that $F(q)$ equals the cost reconstructed from $\chi$ at every orbit $q$.
background
In the Primitive Recognition Calculus, native costs are maps $F$ on ratio orbits obeying reciprocity and related structural hypotheses (PRCNativeCostHypotheses). From any such $F$ one builds a doubled-trace functional; zero-calibration means that doubled trace vanishes at the unit orbit in the cross-equality sense.
A ratio character $\chi$ produces a cost via costFromCharacter. The target proposition asserts that every zero-calibrated native cost factors this way through some signed admissible character. Signed admissibility is stricter than plain character admissibility: it forces a signed (orientation-sensitive) form rather than an absolute-value style generator.
The absolute-value-generated native cost is the concrete map that returns zero at the unit orbit and otherwise the cost of the absolute-value character. Upstream results already show it satisfies the native-cost hypotheses and that its doubled trace is zero-calibrated, and that no signed admissible character reconstructs it.
proof idea
Assume the universal factorization target. Instantiate it at the absolute-value-generated native cost, feeding the already-proved native-cost hypotheses and zero-calibration of its doubled trace. The resulting existential (a signed admissible character matching that cost) directly contradicts PRCNoSignedAdmissibleFactorForAbsValueGeneratedNativeCost. Discharge by exact on that contradiction. Pure term-mode specialization; no new algebra.
why it matters
This refutation is one half of the native-cost uniqueness blocker certificate: the unsigned/zero-calibrated factorization target is proved, while the signed-admissible variant is refuted. That certificate feeds the conditional universal-foundation certificate in UniversalFoundation, which packages kernel, real-complete ordered field, and trace-logic passes.
In the Recognition forcing chain the native cost is forced toward the $J$-cost $J(x)=(x+x^{-1})/2-1$ (T5). Blocking signed-admissible character factorization narrows the admissible generators: absolute-value style costs survive zero-calibration but cannot be signed-factorized, so uniqueness arguments must route through the unsigned (or otherwise constrained) character class rather than a signed d'Alembert factor. The result closes a false branch rather than constructing the unique cost itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.