PRCPrimeCalibrationForcesNonunitOrbitLocalOrientationTarget_refuted
plain-language theorem explainer
Prime-axis calibration of a ratio character does not force local orientation on every nonunit orbit direction. The two-adic axis-twist character is a concrete counterexample: it is prime-calibrated yet fails on the 2·3 composite. Anyone tracking native-cost uniqueness blockers or the prime-floor successor path will cite this. The proof assumes the universal claim, specializes to the twist character, transports orientation along crossEq of the product orbit, and hits a known two-three absurdity.
Claim. It is not the case that every ratio-orbit character $\chi$ that is a PRC ratio character and is calibrated on prime directions necessarily has local orientation on every nonunit orbit direction. Equivalently, prime-direction calibration does not force nonunit-orbit local orientation for all such $\chi$.
background
In the Primitive Recognition Calculus, rational displays are RatioOrbit pairs (signed numerator over a nonzero DistinctionNat denominator). Two such displays are identified by crossEq: cross-multiplication balance of scaled signed orbits, the internal PRC stand-in for rational equality. Characters act on ratio orbits; a PRC ratio character is the structural class used to build native costs.
Prime-direction calibration says $\chi$ orients prime axes correctly. Nonunit-orbit local orientation asks for more: every nonunit orbit direction (not only primes) is oriented, up to identity or reciprocal, in the character's local sense. The target proposition asserts that prime calibration alone forces that stronger property for every ratio character.
The module studies uniqueness of native cost functionals built from such characters (J-cost lineage, d'Alembert/trace constraints). This declaration is the first component of a prime-floor successor blocker: it records that the naive implication "prime calibration $\Rightarrow$ full nonunit orientation" is false.
proof idea
Assume the universal target. Instantiate at the two-adic axis-twist character, already known to be a ratio character and prime-direction calibrated, to obtain nonunit local orientation for that character.
Form the product orbit $2\cdot 3$: nonzero by mul_ne_zero on the prime orbits, and nonunit by left-factor nonunit. Its orbit direction is crossEq-equivalent to the fixed two-three prime-composite direction via orbitDirection_mul_crossEq.
Because the twist character respects crossEq (from normalize-ratio canonicity), local orientation on the product transports to two-three composite local orientation (identity or reciprocal branch, using crossEq_symm/crossEq_trans and reciprocal congruence).
That composite orientation contradicts PRCCharacterTwoAdicAxisTwist_two_three_local_orientation_absurd. Hence the target is false.
why it matters
Native cost uniqueness cannot be closed by assuming prime calibration automatically orients all nonunit orbits. This refutation is the first prime-floor successor blocker component and feeds the product-local-orientation refutation one line downstream (the product target implies the plain target, so both fall).
It is wired into prc_native_cost_uniqueness_blocker_certificate, which packages several forced/refuted factorization and calibration targets for the uniqueness program, and appears in the conditional universal-foundation certificate chain. In framework terms it sits under the PRC foundation leading toward J-uniqueness (T5) and the Recognition Composition Law: cost characters must be constrained by global functional equations, not by prime-axis calibration alone.
The open path is the remaining uniqueness route that avoids this blocked implication (zero-calibrated factorization and related certificates already tracked in the same module).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.