PRCPrimeCalibratedTwoAdicAxisTwistCharacter
plain-language theorem explainer
Packages the existence of a ratio-orbit character that is multiplicative, unit-preserving, J-calibrated on every native prime direction, and two-adically twisted: the prime-2 axis is reciprocal while every other prime axis is identity. Downstream absurdity lemmas cite it as the concrete countermodel the native-valuation branch must kill. The body is a three-conjunct existential Prop, not a construction.
Claim. There exists a map $\chi$ on rational orbits such that $\chi$ is a ratio character (unit at $1$, multiplicative up to cross-equivalence), the cost generated by $\chi$ agrees with canonical $J$-cost on every native prime direction, and $\chi$ sends the prime-$2$ direction to its reciprocal while fixing every other prime direction (identity orientation).
background
In the primitive recognition calculus, costs factor through d'Alembert-type characters on rational orbits. A rational orbit is an integer numerator over a nonzero orbit denominator (K4.7). A ratio character $\chi$ is a map on those orbits that preserves the unit and multiplies, with equalities taken up to cross-equivalence so the statement stays quotient-native.
Prime-direction calibration demands that the cost built from $\chi$ match the canonical $J$-cost on every prime orbit. The two-adic axis-twist form is the obvious native-valuation countermodel: orbit $2$ is reciprocal-oriented, and every other native prime axis is identity-oriented. The surrounding module develops uniqueness of the native cost against such character candidates.
proof idea
Definitional packaging only: the Prop is the existential conjunction of three already-named predicates on a map $\chi : \mathrm{RatioOrbit}\to\mathrm{RatioOrbit}$ (ratio character, prime-direction calibration, two-adic axis twist). No construction, no tactics, no lemmas applied.
why it matters
This is the named target the character-rigidity branch must refute. Downstream absurdity theorems discharge it from mixed-composite cost consistency, absence of non-two mixed reciprocal-identity characters, prime-identity-forces-two, prime-pair product consistency, and the two-three local orientation target. An iff links it to the bare two-adic axis-twist ratio-character package. In the Recognition forcing chain the point is uniqueness of the $J$-cost (T5) against native valuation twists; killing this model closes the two-adic loophole on the path to rigid native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.