prc_every_prime_axis_orientation_free
plain-language theorem explainer
On the discrete rational carrier, every prime orbit admits an independent orientation flip: a multiplicative reciprocal ratio-character that inverts that prime axis and fixes every other prime axis. Anyone arguing that δ-native arithmetic alone forces the J-cost cites this. The proof exhibits the axis-twist character and rules out self-identity via non-reciprocity of prime directions.
Claim. For every prime orbit $p$, there exists a ratio-orbit map $\chi$ that is a PRC ratio character (fixes the unit, is multiplicative, and respects reciprocals up to cross-equivalence) such that $\chi$ fixes the prime direction of every prime orbit $r \neq p$, yet $\chi$ does not fix the prime direction of $p$.
background
In the Primitive Recognition Calculus, costs on the rational carrier factor through ratio orbits. A PRC ratio character is a map $\chi$ on ratio orbits that preserves the unit, multiplies, and sends reciprocals to reciprocals, all up to cross-equivalence (the quotient-native equality on orbits). Prime orbits supply independent axes via primeDirection; cross-equivalence compares two orbits without choosing representatives.
The Recognition Composition Law, after $g = F+1$, becomes d'Alembert's identity. Continuous solutions are $F(x) = (x^\lambda + x^{-\lambda})/2 - 1$. On the completion, law_of_logic_forces_jcost uniquely selects the J-cost ($\lambda = 1$) once reciprocity, normalization, composition, and calibration $G''(0)=1$ are imposed. The discrete side has no such neighborhood constraint: each prime axis can be twisted independently.
This module classifies that non-forcing. Earlier per-prime witnesses covered $p=2$ and $p=3$; the present statement unifies them for every prime orbit at once.
proof idea
Term-mode existence: take $\chi$ to be the axis-twist character at $p$. Three facts discharge the conjuncts. First, that character is a PRC ratio character whenever $p$ is a prime orbit. Second, off the chosen axis it acts as the identity on every other prime direction (cross-equivalence). Third, on the $p$-axis it acts as reciprocal, so if it also fixed the $p$-direction one would obtain that the prime direction is cross-equivalent to its own reciprocal; primeDirection_not_crossEq_recip forbids that, closing the contradiction.
why it matters
This is the headline δ-native non-forcing result: orientation freedom is genuinely per-prime, so no finite (indeed no proper) set of prime calibrations forces $J$ on the rational carrier. The canonical reciprocal cost is the all-identity orientation, and discrete arithmetic does not select it.
Downstream, prc_jcost_strength_separation takes this theorem as delta_only_does_not_force, pairing it with completion-side calibration that does select J and with a strict strength increase from δ-only to trace closure. continuumPriceResidueWall_holds records it as every_prime_axis_free inside the continuum price residue wall. It also feeds prc_cost_joint_stratification and the native cost-selection premise ledger.
Framework link: T5 J-uniqueness and the RCL live on the continuous side; this theorem explains why the discrete carrier alone cannot close that uniqueness, matching the module note that only calibration on a neighborhood of the unit (not one axis at a time) forces $\lambda=1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.