PRCNativeCostDoubledTraceZeroCalibratedTarget
plain-language theorem explainer
The zero-orbit calibration target for native costs: every map F on rational orbits that obeys the native cost hypotheses must send the doubled d'Alembert trace of the zero orbit to zero. Cost-classification and character-factorization arguments cite it as the remaining blocker after the coherent-root step. It is a pure Prop abbreviation, not a proved statement; a sibling theorem later refutes it.
Claim. For every map $F$ from rational orbits to rational orbits, if $F$ satisfies the native cost hypotheses (reciprocal symmetry, normalization invariance, and the canonical Recognition Composition Law), then the doubled trace $T_F(q)=2(F(q)+1)$ obeys $T_F(0)\simeq 0$ under cross-equality of orbits.
background
In the Primitive Recognition Calculus, costs live on RatioOrbit: integer numerator over a nonzero distinction-orbit denominator (K4.7). A native cost $F$ is required to satisfy PRCNativeCostHypotheses: reciprocal symmetry under $q\mapsto q^{-1}$, invariance under ratio normalization, and the discrete Recognition Composition Law on the rational surface. The field two_calibrated in those hypotheses rules out the identically zero cost until a real completion exists.
From any such $F$ one forms the doubled d'Alembert trace $T_F(q)=2(F(q)+1)$, written nativeCostDoubledTrace F. For a cost generated by a multiplicative character this equals $\chi(q)+\chi(q)^{-1}$. The predicate PRCDoubledTraceZeroCalibrated asks only that $T$ send the zero orbit to the zero orbit under cross-equality. The nonzero d'Alembert law alone cannot force $T(0)$; character traces with the intended zero image do have doubled trace zero at the origin. This definition packages the claim that native hypotheses already force that missing zero-orbit condition.
proof idea
Definitional unpacking only. The body is the universal quantification over maps $F:\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ of the implication from PRCNativeCostHypotheses F to PRCDoubledTraceZeroCalibrated (nativeCostDoubledTrace F). No tactics, no lemmas applied; the Prop is the target itself.
why it matters
Doc-comment places this as the exact upstream zero-orbit blocker left after the coherent-root theorem in the PRC-native cost uniqueness chain. Downstream, assuming the target yields both the character-trace lift target and, via that, the character-factorization target for native costs. Those are the discrete stand-ins for the continuous J-uniqueness step (T5) and the Recognition Composition Law on the rational surface.
The same module then proves the target false: PRCNativeCostDoubledTraceZeroCalibratedTarget_refuted exhibits the zero-flat native cost, which meets the native hypotheses yet fails zero-orbit calibration of its doubled trace. The definition therefore records a clean negative landmark: native hypotheses alone do not force $T(0)=0$, so character factorization needs a stronger or different calibration route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.