twoAdicGeneratedNativeCost_signed_unit
plain-language theorem explainer
The two-adic axis-twist native cost agrees with the signed unit on the ratio-orbit display: its value on the orbit of −1 matches the calibrated signed-unit cost under cross-multiplication equality. Anyone assembling the PRC native-cost minimality certificate for the two-adic generator cites this. The argument is a short crossEq-transitivity chain that reduces to rational equality of the character displays at −1.
Claim. The two-adic axis-twist native cost is signed-unit calibrated: its ratio-orbit cost on the orbit of $-1$ is cross-equal to the generated native cost of the negative-one ratio, equivalently the rational displays agree after transporting through the two-adic twist character and the on-orbit $J$-cost.
background
In the Primitive Recognition Calculus, costs are compared on RatioOrbit displays: an integer numerator over a nonzero distinction-nat denominator. Two orbits are identified by crossEq (cross-multiplication of signed numerators and denominators). The bridge theorem crossEq_iff_toRat_eq states that cross-equality is exactly equality of the rational verifier displays, so one may move freely between the choice-free integer bridge and ordinary $\mathbb{Q}$ arithmetic.
Native costs in this module are built from multiplicative characters on ratio orbits. The two-adic axis-twist cost is the cost induced by the two-adic twist character; signed-unit calibration asks that this cost, evaluated on the orbit of $-1$, match the generated native cost of that same orbit. The ambient setting is the PRC native-cost minimality certificate stack, which packages several calibration hypotheses (native, signed unit, zero orbit) into a slim sans-pair class.
Upstream, crossEq_trans supplies choice-free transitivity of cross-equality by routing through the integer bridge and cancelling the middle denominator.
proof idea
Unfold the signed-unit calibration predicate. Apply RatioOrbit.crossEq_trans with the already-proved fact that the two-adic generated native cost is cross-equal to the generated cost on negativeOneRatio. The remaining goal is cross-equality of that generated cost with the character-derived cost on the same orbit. Rewrite by crossEq_iff_toRat_eq, then chase the rational displays: costFromCharacter_toRat, twoAdicAxisTwistCharacter_toRat, onRatioOrbit_toRat, negativeOneRatio_toRat, and finally twoAdicTwistRat_neg_one, which evaluates the two-adic twist at $-1$ and closes the equality.
why it matters
Signed-unit calibration is one of the three fields required by twoAdicGeneratedNativeCost_sans_pair_hypotheses, which asserts that the two-adic twist inhabits the slim sans-pair class (native, signed_unit, zero_calibrated). That package is the certificate that the two-adic generated native cost meets the PRC minimality interface without residual pair hypotheses.
In the broader Recognition stack this sits inside the foundation layer that forces the unique $J$-cost (T5: $J(x)=(x+x^{-1})/2-1$) and the multiplicative recognizer structure. Calibrating the signed unit ensures the character-derived cost respects the ${\pm 1}$ kernel of the ratio display, so later minimality and uniqueness arguments can treat the two-adic generator on the same footing as the canonical $J$-cost. No open scaffold remains: the claim is fully proved and only feeds the sans-pair assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.