PRCPrimeCalibratedTwoAdicAxisTwistCharacter_absurd_of_prime_identity_forces_two
plain-language theorem explainer
If prime calibration forces identity on the orbit-2 axis whenever any calibrated prime axis is identity, then no ratio character can be both prime-direction calibrated and a two-adic axis twist. Character-rigidity arguments cite this to rule out the native valuation counter-model. The proof is a one-line transport of the hypothesis through an equivalence to mixed-composite cost consistency, then applies the corresponding absurdity lemma.
Claim. Assume every ratio character that is prime-direction calibrated and has identity on some calibrated prime axis must also have identity on the orbit-$2$ prime axis. Then there is no ratio character that is simultaneously a ratio character, prime-direction calibrated, and a two-adic axis twist.
background
In the primitive recognition calculus, ratio characters are maps on ratio orbits that encode multiplicative cost structure. Prime-direction calibration pins the character on distinguished prime axes. The two-adic axis twist is a concrete model that flips the orbit-$2$ axis onto the reciprocal branch while remaining calibrated on other primes; its existence would refute the current character-rigidity branch via a native valuation route.
The one-sided distinguished-axis target asserts that prime calibration must force identity at the orbit-$2$ prime axis whenever identity holds at any calibrated prime axis. A sibling equivalence identifies that target with a mixed-composite cost-consistency target. The local module develops native cost uniqueness for PRC characters, tying doubled-trace d'Alembert structure to J-cost uniqueness in the forcing chain (T5).
proof idea
One-line term wrapper. Apply the forward direction of the equivalence between the prime-identity-forces-two target and the mixed-composite cost-consistency target to the hypothesis, then feed the resulting consistency hypothesis into the already-proved absurdity lemma that mixed-composite cost consistency rules out any calibrated two-adic axis-twist character.
why it matters
Closes one direction of the two-adic twist exclusion under the distinguished-axis forcing target, a step in native cost uniqueness for PRC characters. Downstream it immediately yields the contrappositive (a calibrated two-adic twist kills the forcing target) and the broader absurdity for any two-adic axis-twist ratio character. It is also wired into the conditional universal-foundation certificate. In the Recognition framework this supports the character-rigidity path toward unique native cost (J-uniqueness, T5), by eliminating a concrete counter-model that would otherwise leave the orbit-$2$ axis free.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.