PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_prime_identity_forces_two
plain-language theorem explainer
Under the hypothesis that prime calibration forces identity on the orbit-2 axis whenever any calibrated prime is identity, every ratio character twisting the two-adic axis must still pick a canonical local orientation at the mixed composite 2·3. Downstream failure-character absurdity and the universal foundation certificate cite it. Proof is a one-line reverse of the target/no-twist iff applied to the already-proved absurdity of a two-adic twist character.
Claim. Assume that every ratio character which is prime-direction calibrated and identity on some calibrated prime axis is forced to be identity on the orbit-$2$ prime axis. Then every ratio character that carries a two-adic axis twist still chooses one of the two canonical local orientations at the first mixed composite $2\cdot 3$.
background
In the Primitive Recognition Calculus, a ratio character is a map on ratio orbits compatible with the multiplicative structure used to build native cost. The two-adic axis twist marks characters that put the orbit-$2$ prime on the reciprocal (non-identity) branch. The $2\cdot 3$ composite-local orientation condition requires that any such twisted character still select one of the two canonical local orientations at the first mixed composite $2\cdot 3$; that is the positive form of the current two-adic branch blocker.
The standing hypothesis is the one-sided distinguished-axis target: prime calibration must force identity at the orbit-$2$ prime axis from identity at any calibrated prime axis. An upstream lemma already converts that hypothesis into absurdity of any two-adic axis-twist ratio character. A separate equivalence identifies the composite-local orientation target with the non-existence of such a twist character.
proof idea
One-line term proof. Apply the reverse direction of the equivalence
PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget ↔ ¬ PRCTwoAdicAxisTwistRatioCharacter,
feeding it the upstream absurdity
PRCTwoAdicAxisTwistRatioCharacter_absurd_of_prime_identity_forces_two hforces.
No extra case analysis: the target is exactly the no-twist statement under that iff.
why it matters
Closes one link in the native-cost uniqueness chain that supports J-uniqueness (forcing step T5): the two-adic branch cannot survive once prime calibration forces identity at orbit 2. Immediate parent is the absurdity of the $2\cdot 3$ composite-local orientation failure character under the same hypothesis. That package is consumed by prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles the conditional PRC foundation certificate (kernel, real complete ordered field, trace logic). Without this bridge, the positive composite-local form of the two-adic blocker would remain unlinked from the prime-identity forcing hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.