zeroFlatNativeCost_not_doubled_trace_zero_calibrated
plain-language theorem explainer
The zero-flat native cost induces a doubled character trace that fails zero-orbit calibration: its value at the zero ratio orbit is not cross-equal to zero. The PRC native-cost uniqueness argument cites this as the explicit counterexample to a blanket zero-calibration target. The proof unfolds calibration to a rational equality and obtains a numerical contradiction.
Claim. Let $T$ be the doubled character trace on ratio orbits induced by the zero-flat native cost. Then $T$ is not zero-calibrated: one does not have cross-equality $T(0)\sim 0$ (equivalently, the rational display of $T(0)$ is not equal to $0$).
background
Ratio orbits are rational displays: an integer numerator over a nonzero distinction-nat denominator, equipped with a verifier map into $\mathbb{Q}$. Cross-equality of two ratio orbits is equivalent to equality of those rational displays (K4.10 in the integer-rational layer). Addition, multiplication, and the constants $0,1,2$ push forward under the verifier in the expected way.
In the primitive recognition calculus, native costs induce doubled character traces $T$ on ratio orbits. Zero-calibration asks that $T$ send the zero orbit to a representative cross-equal to zero. As the local definition notes: the nonzero d'Alembert law cannot constrain $T(0)$, but character traces with the intended zero image have doubled trace $0$ at the zero orbit.
The zero-flat native cost is a concrete candidate whose doubled-trace value at the zero orbit can be expanded fully into ring operations on ratio orbits, so the calibration claim becomes a pure rational arithmetic statement.
proof idea
Assume zero-calibration of the doubled trace of the zero-flat native cost. Unfold the predicate to cross-equality of $T(0)$ with $0$, then replace cross-equality by rational equality via the K4.10 equivalence. Apply the specialized evaluation of this cost's doubled trace at zero, unfold the doubled-trace value formula, and transport the rational display through multiplication, addition, and the simp lemmas for $2$, $0$, and $1$. The resulting numerical equality is false by norm_num.
why it matters
This is the concrete witness that the blanket target "every native cost satisfying the native hypotheses has a zero-calibrated doubled trace" is false. The immediate parent applies it at the zero-flat cost under the zero-flat hypotheses and thereby refutes that target.
In the Recognition Science forcing chain, native-cost uniqueness feeds identification of the J-cost $J(x)=(x+x^{-1})/2-1$ (T5) and the Recognition Composition Law. Exhibiting a zero-flat candidate whose doubled trace breaks zero-orbit calibration clears a false branch before d'Alembert and self-similarity fix $\varphi$ and the eight-tick structure. The lemma is local to the PRC native-cost uniqueness module; it does not by itself force J-uniqueness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.