PRCNativeCostDoubledTraceZeroCalibratedTarget_refuted
plain-language theorem explainer
The claim that every native cost map meeting the PRC interface forces a zero-calibrated doubled trace at the zero orbit is false. Uniqueness arguments for the native J-cost after the coherent-root step would cite this blocker-kill. Proof is a direct counterexample: instantiate the universal claim at the zero-flat native cost and contradict the known failure of its doubled-trace zero calibration.
Claim. It is false that every map $F$ from ratio orbits to ratio orbits that satisfies the native cost hypotheses has doubled trace zero-calibrated at the zero orbit: there exists a native-cost $F$ for which $\mathrm{nativeCostDoubledTrace}(F)$ fails zero-orbit calibration.
background
In the primitive recognition calculus, a native cost is a map on ratio orbits obeying the Recognition Composition Law interface (reciprocity and the cross-equation form of RCL) on nonzero inputs. From such an $F$ one builds a doubled trace via the character-trace construction; zero calibration at the zero orbit means that doubled trace evaluates to the zero orbit there.
After the coherent-root theorem, the remaining upstream blocker was exactly the universal assertion that every native-cost $F$ forces that zero calibration. The module isolates a canonical counterexample candidate: the zero-flat native cost, which agrees with the standard on-ratio cost off zero, but is flattened to zero at the zero orbit (and at the unit orbit). Because RCL only quantifies over nonzero inputs, this still satisfies the native cost hypotheses.
A sibling lemma already shows that the doubled trace of this zero-flat cost is not zero-calibrated. The present result packages that fact as a refutation of the universal blocker.
proof idea
Term-mode reductio. Assume the universal target. Apply it to the zero-flat native cost together with the theorem that this map meets the native cost hypotheses. The conclusion is zero calibration of its doubled trace. Discharge by the sibling lemma that this doubled trace fails zero calibration (via direct evaluation of the doubled-trace value at zero in rational coordinates).
why it matters
This kills the exact zero-orbit blocker left after the coherent-root theorem in the native-cost uniqueness path. In the Recognition forcing chain, native cost uniqueness feeds T5 (J-uniqueness: $J(x)=(x+x^{-1})/2-1$), which is forced by the RCL functional equation. Refuting the over-strong zero-calibration demand clarifies that uniqueness cannot be obtained by requiring every interface cost to vanish on the zero orbit of the doubled trace; the zero-flat spike is a legitimate interface map that refuses that demand.
No downstream consumers are wired yet (used_by is empty). The result is a negative landmark: it closes a false route rather than supplying a positive uniqueness step. Anyone tightening the native-cost hypotheses toward genuine J-uniqueness must add structure that excludes zero-flat spikes without breaking RCL on nonzero orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.