absValueGeneratedNativeCost_doubled_trace_zero_calibrated
plain-language theorem explainer
The doubled-trace map built from the absolute-value generated native cost vanishes at the zero ratio-orbit (cross-equal to zero). Minimality certificates and uniqueness-refutation theorems cite this zero-calibration fact. The proof transports the claim to rational displays via crossEq↔toRat and finishes by norm_num after unfolding the absolute-value character branch.
Claim. Let $T$ be the doubled-trace map associated to the absolute-value generated native cost on ratio orbits. Then $T(0)$ is cross-equal to the zero orbit; equivalently, the rational display satisfies $T(0)_{\mathbb{Q}}=0$.
background
In the Primitive Recognition Calculus, costs and characters act on ratio orbits: pairs of a signed integer numerator over a nonzero distinction-nat denominator, with a verifier display toRat into $\mathbb{Q}$. Cross-equality of two orbits is equivalent to equality of those rational displays (K4.10).
Doubled traces package a cost into a map $T$ on ratio orbits. The nonzero d'Alembert identity does not fix $T(0)$; zero-calibration is the separate demand that $T$ send the zero orbit to zero (cross-equal). Character-generated costs with the intended zero image are expected to meet this.
The absolute-value generated native cost is the cost pulled back from the absolute-value character. Its doubled trace is the object whose zero-orbit value is checked here. Upstream arithmetic lemmas (add_toRat, mul_toRat, one_toRat, zero_toRat, and the factor-two display) make the transport fully computational on $\mathbb{Q}$.
proof idea
Term-mode rewrite proof. Unfold zero-calibration to cross-equality of $T(0)$ with zero, then replace cross-equality by rational equality via crossEq_iff_toRat_eq. Unfold the doubled-trace construction and push toRat through multiplication, addition, and the constants two, zero, and one.
On the absolute-value cost, discharge the zero branch of the defining if by showing the orbit is not one (congruence on toRat plus norm_num). Rewrite the remaining character cost through costFromCharacter_toRat and absValueCharacter_toRat, reduce the zero display, and close with norm_num.
why it matters
Zero-calibration is the missing orbit condition that the nonzero d'Alembert law cannot supply. This theorem installs it for the absolute-value generated native cost, so that cost inhabits the slim sans-sign hypothesis package used by the minimality certificate (absValueGeneratedNativeCost_sans_sign_hypotheses).
Downstream uniqueness machinery uses the same fact when refuting over-strong targets: zero-calibrated uniqueness, signed-unit calibration forced by zero-calibration, and signed admissible character factorization. Those refutations show that absolute-value cost meets the native and zero-calibrated hypotheses yet fails signed-unit or uniqueness claims, sharpening what native-cost uniqueness can and cannot assert.
In the broader Recognition forcing chain this sits in foundation work on native $J$-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), fixing the zero-orbit of the doubled-trace presentation before uniqueness and minimality arguments proceed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.