PRCTwoThreeCompositeLocalOrientationForTwoAdicAxisTwistTarget_of_no_ratio_character_axis_twist
plain-language theorem explainer
If no ratio character carries the two-adic axis twist, then every such character (of which there are none) satisfies the 2·3 composite-local orientation condition. Cited when discharging the two-adic branch blocker by nonexistence of the uncalibrated ratio-character target. The proof is a one-line vacuous argument: any witness would contradict the hypothesis.
Claim. If there is no map $\chi$ on ratio orbits that is both a ratio character and carries the two-adic axis twist, then every ratio character that carries the two-adic axis twist satisfies the canonical local-orientation condition at the first mixed composite $2\cdot 3$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, ratio characters are maps on ratio orbits that encode multiplicative branch data for the cost. The two-adic axis twist is a specific branch behavior on the 2-primary axis; the uncalibrated construction target asserts existence of some ratio character carrying that twist.
The positive $2\cdot 3$ composite-local orientation target is the dual blocker form: every ratio character that does carry the two-adic axis twist must still pick one of the two canonical local orientations at the first mixed composite $2\cdot 3$. Doc-comment: "every ratio character carrying the two-adic axis branch must still choose one of the two canonical local orientations at the first mixed composite."
This lemma sits in the PRC native-cost uniqueness module, which reduces uniqueness of the native cost (tied to the J-cost and Recognition Composition Law) to character-trace and branch-uniformity constraints along the prime and composite lattice.
proof idea
Term-mode vacuous implication. Introduce an arbitrary ratio character $\chi$ assumed to carry the two-adic axis twist. Package $(\chi,$ character hypotheses, twist$)$ as a witness of the existential two-adic axis-twist ratio-character target. That witness contradicts the hypothesis that no such character exists, so exfalso discharges the orientation goal. No orientation arithmetic is invoked; the universal claim holds because its hypothesis class is empty.
why it matters
One half of the biconditional equating the $2\cdot 3$ composite-local orientation target with nonexistence of a two-adic axis-twist ratio character. Downstream, the iff packages both directions, and the prime-identity branch-uniformity route reuses this lemma after proving the ratio-character target is absurd under uniformity.
It also feeds prc_universal_foundation_conditional_certificate in UniversalFoundation, which assembles kernel, real-complete ordered field, and trace-logic certificates into the conditional PRC universal foundation. In the broader forcing picture this is bookkeeping on the character side of native-cost uniqueness (J-uniqueness / T5 and the RCL), not a new physical constant claim: it clears a two-adic branch obstruction so later calibration and octave structure can proceed without a rogue ratio-character countermodel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.