PRCTwoAdicAxisTwistRatioCharacter
plain-language theorem explainer
Existence of a ratio-orbit map that is a unit-preserving multiplicative character yet twists the two-prime axis to its reciprocal while leaving every other prime axis identity-oriented. Cost-uniqueness and prime-calibration arguments cite this as the uncalibrated two-adic countermodel target. The body is a pure existential packing of the character axioms with the axis-twist branch condition; no construction is supplied.
Claim. There exists a map $\chi$ from ratio orbits to ratio orbits such that $\chi$ is a ratio character (unit at $1$ and multiplicative up to cross-equivalence) and $\chi$ realizes the two-adic axis twist: the image of the two-prime direction is cross-equivalent to its reciprocal, while every other native prime direction is cross-equivalent to itself.
background
In the primitive recognition calculus, costs on ratio orbits are analyzed through d'Alembert-type factorizations. A ratio character is a map $\chi$ on ratio orbits that fixes the unit orbit and is multiplicative, both up to cross-equivalence rather than definitional equality, so the interface stays quotient-native.
A ratio orbit is the K4.7 display of a signed-orbit numerator over a nonzero distinction-nat denominator. The two-adic axis-twist condition singles out the prime orbit of $2$: $\chi$ sends that direction to its reciprocal, and sends every other native prime axis to itself (again up to cross-equivalence). The doc-comment calls this "the obvious countermodel one would construct from a native two-adic valuation."
This module studies uniqueness of the native PRC cost. The present definition is the uncalibrated construction target for that two-adic branch: it asks only whether some ratio character already carries the twist, before any prime-calibration field is imposed.
proof idea
Definitional packing, not a proved theorem. The proposition is the existential $\exists,\chi:(\mathrm{RatioOrbit}\to\mathrm{RatioOrbit}),;\mathrm{PRCRatioCharacter},\chi\land\mathrm{PRCCharacterTwoAdicAxisTwist},\chi$. No witness is built; the body just conjoins the character structure (unit and multiplicativity via cross-equivalence) with the concrete two-adic branch predicate on prime axes.
why it matters
Pass 115 treats this as the uncalibrated two-adic target: once the twist is carried by a ratio character, the prime-calibration field is automatic. Downstream, it is equivalent to the prime-calibrated two-adic axis-twist character (iff and both directions of the bridge).
It is the hypothesis in a family of negative results: assuming the twist character, one obtains the negations of prime-identity branch uniformity, two-prime identity forcing, prime-pair product cost consistency, and two-prime mixed composite cost consistency. Companion absurdity lemmas (from mixed composite consistency, or from absence of a calibrated twist) close the countermodel analysis.
In the broader forcing chain this sits under native cost uniqueness for the J-cost factorization (T5 landmark: $J(x)=(x+x^{-1})/2-1$), ruling out two-adic valuation-style branch defects before the self-similar fixed point $\phi$ and the eight-tick octave are forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.