twoAdicAxisTwistCharacter_toRat
plain-language theorem explainer
Transport lemma: the ratio-orbit two-adic axis twist, read back as a rational, equals the classical two-adic branch twist of the orbit's rational display. Anyone proving that the orbit-level character is a PRC ratio character, a two-adic axis twist, or generates a calibrated native cost cites this. Proof is a one-line unfold plus the round-trip identity for ratioOrbitOfRat.
Claim. For every rational orbit $q$ (signed-orbit numerator over a nonzero distinction-nat denominator), the rational display of the two-adic axis-twist character applied to $q$ equals the classical two-adic branch twist of the rational display of $q$: $(\chi_{2}(q))^{\mathbb{Q}} = T_{2}(q^{\mathbb{Q}})$, where $T_{2}(x)=x\cdot 2^{-2\,v_{2}(x)}$ inverts the $2$-adic valuation exponent and fixes odd-prime axes.
background
In the Primitive Recognition Calculus, rationals are displayed as RatioOrbit: a signed orbit numerator over a nonzero distinction-nat denominator. The verifier map toRat sends such an orbit to $\mathbb{Q}$ by integer division (spec tag A5: a transport wrapper whose internal equality is cross-multiplication).
The classical two-adic branch twist on rational displays is $T_{2}(x)=x\cdot 2^{-2,v_{2}(x)}$. It fixes odd-prime axes and inverts the orbit-$2$ exponent. The orbit-level character is defined by pushing $q$ through toRat, applying $T_{2}$, and lifting back via ratioOrbitOfRat.
The module develops uniqueness and generation of native costs from ratio characters. The upstream round-trip ratioOrbitOfRat_toRat states that lifting a rational and reading it back recovers the original rational.
proof idea
One-line wrapper. Unfold the definition of the orbit-level two-adic axis-twist character, which is exactly ratioOrbitOfRat of the classical twist of q.toRat. The goal reduces to (ratioOrbitOfRat (T₂(q.toRat))).toRat = T₂(q.toRat), discharged by the upstream identity ratioOrbitOfRat_toRat.
why it matters
This is the bridge that lets every orbit-level property of the two-adic axis-twist character be checked on classical rationals. Downstream it feeds: the proof that the character is a PRC ratio character (unit and reciprocity via toRat); the branch axiom PRCCharacterTwoAdicAxisTwist; the non-identity on the successor-of-three orbit direction; and the cross-equality identifying the two-adic-generated native cost with costFromCharacter of this twist.
Those cross-equalities in turn calibrate the signed unit and the zero orbit in the minimality certificate module, so the native cost built from the two-adic twist sits inside the uniqueness/minimality pipeline for PRC native costs. In the broader Recognition forcing chain this is foundation scaffolding for the unique J-cost (T5) realized on ratio orbits, not yet the physical constants themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.