PRCTwoThreeCompositeLocalOrientationFailureCharacter
plain-language theorem explainer
Defines the witness proposition that some ratio-orbit character is a genuine ratio character, twists the two-adic axis, and fails local orientation on the 2·3 composite. Native-cost uniqueness arguments cite it as the constructive countermodel surface for the reduced two-adic ratio-character target. The body is a three-conjunct existential Prop, not a proved theorem.
Claim. There exists a map $\chi$ on ratio orbits that is a PRC ratio character, twists the two-adic axis, and fails the local orientation condition on the composite direction $2\cdot 3$.
background
In the Primitive Recognition Calculus, cost uniqueness is tracked through characters on ratio orbits: maps $\chi$ that encode how multiplicative directions (primes and composites built from them) are sent to identity, reciprocal, or mixed branches. A ratio character is the algebraic skeleton of a candidate native cost; the two-adic axis twist says the orbit of $2$ is sent to the reciprocal branch rather than identity.
Local orientation on the $2\cdot 3$ composite is the consistency demand that the character respect the composite direction built from $2$ and $3$ in the oriented way forced by the native cost axioms. Failure of that condition is the concrete obstruction surface for mixed non-two branches.
The surrounding module builds native-cost uniqueness from doubled-trace and d'Alembert structure on the J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Reciprocal structure from the cost algebra and ledger forcing supplies the inverse-ratio branch that the twist uses.
proof idea
No proof: this is a bare Prop abbreviation. The body is the existential package $\exists,\chi$ with three conjuncts (ratio character, two-adic axis twist, negation of $2\cdot 3$ composite local orientation). Downstream lemmas unpack the witness and re-package it into calibrated prime and mixed-branch obstruction characters.
why it matters
This definition is the shared hypothesis surface for the two-three local-orientation failure branch of native-cost uniqueness. Downstream, assuming the witness yields the prime-calibrated two-adic axis-twist character, the non-two mixed character, composite defect and cost-defect characters, and several negated calibration targets (prime-identity forcing two-prime identity, prime-pair product cost consistency, two-prime mixed composite cost consistency).
In framework terms it sits inside the J-uniqueness and native-cost forcing story (T5 and the RCL): it isolates the constructive countermodel where a character twists $2$ and breaks orientation on $2\cdot 3$, so uniqueness proofs can rule that branch out or convert it into calibrated obstruction forms. It is the reduced two-adic ratio-character target in witness clothing, not a closed uniqueness theorem by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.