twoAdicGeneratedNativeCost_zero_calibrated
plain-language theorem explainer
The two-adic axis-twist native cost has doubled-trace display equal to zero at the zero ratio orbit, in the cross-equality sense. Anyone assembling the sans-pair certificate for this cost cites it as the zero-calibration leg. The proof reduces the certificate predicate to rational equality, feeds in the generated cross-equation at zero, and finishes by arithmetic simplification on the rational displays.
Claim. The doubled-trace display of the two-adic axis-twist native cost is zero-calibrated: its value at the zero ratio-orbit equals the zero orbit under cross-multiplication (equivalently, the rational displays agree and both are $0$).
background
In the Primitive Recognition Calculus, costs are carried as native objects whose verifier displays live in RatioOrbit: a signed-orbit numerator over a nonzero distinction-nat denominator. The map toRat sends each such display to $\mathbb{Q}$, and crossEq is the integer cross-multiplication relation; K4.10 records that crossEq a b iff a.toRat = b.toRat.
Addition and multiplication of ratio orbits are compatible with toRat (add_toRat, mul_toRat), and the unit and zero orbits display as $1$ and $0$. The two-adic axis-twist character supplies a generated native cost; its doubled-trace display is the object whose zero-orbit value must match the zero orbit for calibration.
Locally this module packages minimality certificates for that native cost. Zero-calibration is one structural leg of the slim sans-pair hypothesis bundle.
proof idea
Term-mode proof. Unfold the zero-calibration predicate and replace cross-equality by rational equality via crossEq_iff_toRat_eq. Instantiate the generated cross-equation of the two-adic native cost at the zero orbit, then rewrite that hypothesis through costFromCharacter_toRat, twoAdicAxisTwistCharacter_toRat, zero_toRat, and twoAdicTwistRat_zero, so the character contribution at zero is the rational $0$.
Unfold the doubled-trace display and push toRat through multiplication and addition (mul_toRat, add_toRat) together with the constants two_toRat, one_toRat, and zero_toRat. Substitute the simplified generator hypothesis and close with norm_num.
why it matters
Zero-calibration is the third field of the slim sans-pair package for the two-adic generated native cost. The immediate parent is twoAdicGeneratedNativeCost_sans_pair_hypotheses, whose doc-comment states that the two-adic twist inhabits the sans-pair class; that theorem wires this result in as zero_calibrated alongside the native and signed-unit legs.
In the Recognition foundation, native-cost minimality certificates sit under the Primitive Recognition Calculus that feeds the forcing chain: unique $J$-cost (T5), $\varphi$ as self-similar fixed point (T6), and the discrete octave structure. Establishing that the two-adic axis twist is zero-calibrated removes an ad-hoc pair hypothesis and keeps the cost inside the certified native class used for later uniqueness and minimality arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.