absValueGeneratedNativeCost_crossEq_generated
plain-language theorem explainer
For every rational orbit, the absolute-value-generated native cost agrees under cross-multiplication with the cost pulled back from the absolute-value character. Anyone assembling native-cost hypotheses or prime calibrations for the abs-value generator cites this bridge. The proof is a classical case split on the unit orbit: rational-display equality at zero when q is one, and reflexivity of crossEq off the unit.
Claim. For every ratio orbit $q$, the absolute-value-generated native cost of $q$ is cross-equivalent (same rational verifier display) to the cost obtained by evaluating the absolute-value character on $q$.
background
In the Primitive Recognition Calculus, a ratio orbit is an integer numerator over a nonzero distinction-nat denominator: the internal display of a positive rational. Cross-equivalence (crossEq) is the PRC-native relation that two ratio orbits balance under cross-multiplication of signed orbits; by K4.10 it agrees with equality of the rational verifier displays (toRat).
Native costs are maps from ratio orbits to ratio orbits meant to realize the recognition cost (the J-cost of the forcing chain) inside the orbit calculus. The absolute-value character is the multiplicative character that records absolute size; costFromCharacter turns such a character into a cost map. The absolute-value-generated native cost is the piecewise map that sends the unit orbit to zero and otherwise coincides with that character cost.
This lemma sits in the native-cost uniqueness module: it identifies the generated map with the character cost up to the internal rational relation, so later hypotheses can be transferred from the character side.
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) and rewrite cross-equivalence as equality of toRat displays. The left side is the zero orbit (zero_toRat); the right side is costFromCharacter of the absolute-value character at the unit, which reduces via absValueCharacter_toRat and one_toRat to $0$. Close by norm_num.
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 step that lets the absolute-value-generated native cost inherit structure from the absolute-value character. Downstream it is the first leg of every transfer: native hypotheses (absValueGeneratedNativeCost_native_hypotheses) compose it with reciprocity; prime-direction and prime-pair product calibrations compose it with the character's prime calibrations; and the strengthened native-hypotheses target packages the generated cost together with this crossEq witness.
In the broader Recognition framework the native cost is the orbit-level avatar of the unique J-cost forced at T5 ($J(x)=(x+x^{-1})/2-1$). Establishing that the abs-value generator satisfies the native-cost package is part of closing uniqueness of that cost inside PRC, before the cost is lifted to continuum and physical constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.