PRCZeroCalibrationForcesNativeCostSignedUnitCalibrationTarget
plain-language theorem explainer
Names the target claim that native-cost hypotheses plus zero-calibration of the doubled trace force signed-unit calibration of the cost at −1. Downstream uniqueness and foundation ledgers cite this Prop as a discrete forcing route. The body is pure quantification: no proof content, only the implication to be tested or refuted.
Claim. For every map $F$ from rational orbits to rational orbits, if $F$ obeys the native cost hypotheses (reciprocal symmetry, normalization invariance, and the discrete Recognition Composition Law) and the doubled trace $T_F(q)=2(F(q)+1)$ satisfies $T_F(0)=0$, then $F$ is signed-unit calibrated: $F(-1)$ matches the on-orbit native cost at the signed unit $-1$.
background
In the Primitive Recognition Calculus, costs live on RatioOrbit: integer numerator over a nonzero orbit denominator (K4.7). A native cost $F$ is constrained by PRCNativeCostHypotheses: reciprocal cross-equality, invariance under ratio normalization, and the discrete RCL on the rational surface. The field two_calibrated in those hypotheses rules out the zero cost until a real completion exists.
The doubled trace is $T_F(q)=2(F(q)+1)$, written nativeCostDoubledTrace. For a character-generated cost this equals $\chi(q)+\chi(q)^{-1}$. Zero-calibration of a doubled trace means $T(0)=0$ by cross-equality; the nonzero d'Alembert law alone cannot force this at the zero orbit.
Signed-unit calibration asks that $F$ see the signed unit $-1$, not only positive prime and prime-pair probes: $F(-1)$ must match the on-orbit native value at $-1$. That repair sits after an absolute-value no-go on the discrete surface.
proof idea
Definition only: the declaration is the Prop $\forall F,; \mathrm{NativeHyp}(F)\to \mathrm{ZeroCal}(T_F)\to \mathrm{SignedUnitCal}(F)$. No tactics, no lemmas applied. Downstream code treats the name as a target to prove or refute; the refutation theorem instantiates $F$ at the absolute-value generated native cost and uses that this $F$ meets the native hypotheses and zero-calibration yet fails signed-unit calibration.
why it matters
This target is one exact Lean split of the still-open native-cost uniqueness problem (T5-style J-uniqueness on the discrete rational surface). The pass-25 blocker certificate records it under the zero-calibration signed-unit slot, and the universal-foundation open-target ledger carries the matching negative entry once the route is closed.
The companion theorem ...Target_refuted shows the implication is false: zero-calibration of $T_F$ plus native hypotheses do not force signed-unit calibration. That refutation prunes a forcing path that would have jumped from zero-orbit compatibility straight to the signed-unit repair, so uniqueness work must use a stronger admissible or character-factorization route instead of this shortcut.
Framework role: it is bookkeeping for the discrete half of cost uniqueness (RCL / J-cost lineage), not a physics constant claim. Positive factorization targets remain open; this particular forcing arrow is closed as impossible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.