PRCCharacterTwoAdicAxisTwist
plain-language theorem explainer
A predicate on maps of ratio orbits: the prime-2 axis is sent to its reciprocal, while every other native prime axis is fixed. It packages the obvious two-adic valuation countermodel for character rigidity. Downstream uniqueness arguments cite it to build the uncalibrated and prime-calibrated twist targets and to force two-three local orientation failure. The body is a pure Prop conjunction of cross-equality clauses; no proof.
Claim. A map $\chi$ from ratio orbits to ratio orbits has the two-adic axis-twist form when $\chi$ sends the prime-$2$ direction to its reciprocal (cross-equality) and, for every native prime orbit $p\neq 2$, sends the $p$-direction to itself (cross-equality).
background
In the Primitive Recognition Calculus, rationals are displayed as ratio orbits: a signed-orbit numerator over a nonzero distinction-orbit denominator. Two such displays are identified by cross-equality: the internal PRC relation that balances scaled numerators and denominators as signed orbits (K4.10). Reciprocal is the total involution on ratio orbits that mirrors $q\mapsto 1/q$ on $\mathbb{Q}$, sending zero to zero.
Prime directions are the ratio-orbit axes attached to native prime distinction orbits. The two-prime direction is the axis for orbit $2$. A ratio character is a structure-preserving map on these displays; the present predicate isolates one concrete branch of such a map.
The local module develops native-cost uniqueness via character rigidity. This definition is the explicit two-adic twist branch: reciprocal orientation only on the $2$-axis, identity orientation on every other prime axis. Doc-comment: it is "the obvious countermodel one would construct from a native two-adic valuation."
proof idea
Definitional, not a theorem. The Prop is the conjunction of (i) cross-equality of $\chi$ on the two-prime direction with the reciprocal of that direction, and (ii) a universal quantifier over prime distinction orbits $p\neq 2$ requiring cross-equality of $\chi$ on the $p$-direction with the $p$-direction itself. No tactics or lemmas fire at the definition site.
why it matters
This is the uncalibrated construction target for the two-adic axis-twist branch in native-cost uniqueness. It feeds PRCTwoAdicAxisTwistRatioCharacter (existence of a ratio character carrying the twist) and the calibrated variant that also demands prime-direction calibration. Pass-115 style results show calibration is automatic once a ratio character carries this branch behavior.
Downstream, the twist forces mixed image on the two-three composite direction and yields absurdity for two-three composite local orientation. Those lemmas close a rigidity fork: a character cannot both be a ratio character with this two-adic twist and preserve two-three local orientation. In the broader Recognition chain this sits under J-uniqueness and native cost identification (T5 / RCL side), ruling out valuation-style countermodels before the cost functional is forced.
Parent objects include the prime-calibrated twist character and the theorems that the twist implies two-three local orientation failure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.