twoAdicGeneratedNativeCost_crossEq_generated
plain-language theorem explainer
For every ratio orbit q, the two-adic axis-twist generated native cost agrees with the cost pulled back from the two-adic axis-twist character, under internal cross-multiplication equivalence. Downstream uniqueness and minimality certificates cite this as the bridge from the generated cost to the character display. The proof is a classical case split on the unit orbit, reducing to rational equality at one and reflexivity elsewhere.
Claim. For every ratio orbit $q$, the two-adic axis-twist generated native cost at $q$ is cross-equivalent (balanced cross-multiplication of signed numerator and denominator orbits) to the cost obtained by evaluating the two-adic axis-twist character at $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is a signed integer numerator over a nonzero distinction-nat denominator: the internal display of a rational. Cross-equivalence of two ratio orbits means the scaled numerators balance as signed orbits ($a.num\cdot b.den$ versus $b.num\cdot a.den$). By K4.10 this is equivalent to equality of the verifier rational displays toRat.
Native costs are maps from ratio orbits to ratio orbits obeying reciprocity and related PRC hypotheses. One constructs candidates from multiplicative characters on the ratio display; costFromCharacter is that pullback. The two-adic axis-twist character is the generator used for the two-adic native cost candidate: on the unit orbit the generated cost is forced to zero, and elsewhere it coincides with the character cost.
The local module develops uniqueness and non-uniqueness statements for such native costs. This lemma pins the generated two-adic cost to its character source under the internal rational relation, so later calibration and hypothesis packages can work entirely with cross-equivalence.
proof idea
Classical case split on whether $q$ is the unit ratio orbit.
If $q$ is the unit: unfold the generated cost (the if_pos branch), rewrite cross-equivalence to rational equality via crossEq_iff_toRat_eq, and reduce both sides with zero_toRat, costFromCharacter_toRat, the character evaluation at one, and one_toRat. The remaining rational identity is discharged by norm_num after the twist-at-one simplification.
If $q$ is not the unit: unfold the generated cost on the if_neg branch; it is definitionally the character cost, so crossEq_refl finishes.
why it matters
This is the identification lemma that lets the two-adic generated native cost inherit character-level properties under cross-equivalence. It is packaged directly into PRCTwoAdicAxisTwistGeneratedCostNativeHypothesesTarget_constructed and into twoAdicGeneratedNativeCost_hypotheses (reciprocity and the rest of the native-cost hypothesis bundle).
Minimality certificates use it to calibrate the signed unit and the zero orbit (twoAdicGeneratedNativeCost_signed_unit, twoAdicGeneratedNativeCost_zero_calibrated). The same bridge appears in the refutation of naive uniqueness (PRCNativeCostUniquenessTarget_refuted) and in the failure of prime-pair product calibration, where the generated cost is compared along composite directions.
In the Recognition forcing chain this sits under native J-cost uniqueness infrastructure (T5 territory): it shows how a concrete two-adic generator sits inside the PRC cost axioms without claiming global uniqueness of that cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.