prc_native_cost_orientation_underdetermined
plain-language theorem explainer
On the discrete ratio-orbit carrier, reciprocal-character axioms plus identity orientation on every odd prime still leave the 2-axis free: the two-adic axis twist is a full PRC ratio character that inverts only the orbit-2 direction. Anyone arguing that δ-native arithmetic forces the canonical J-cost must cite this non-forcing witness. The proof is a term construction of that twist plus a short crossEq contradiction if the 2-axis were identity-oriented.
Claim. There exists a map $\chi$ on ratio orbits that is a PRC ratio character (unit-preserving, multiplicative, reciprocal-symmetric under cross-equivalence), such that for every prime distinction orbit $p$ other than the orbit of $2$, $\chi$ is cross-equivalent to the identity on the prime direction of $p$, yet $\chi$ is not cross-equivalent to the identity on the prime direction of $2$.
background
In the Primitive Recognition Calculus, costs are built from ratio characters on RatioOrbit, the δ-native rational carrier. A PRC ratio character $\chi$ is a map on ratio orbits that is unit-normalized, multiplicative, and reciprocal under cross-equivalence (the internal balance relation on signed orbits: $a$ and $b$ match when $a.num\cdot b.den$ balances $b.num\cdot a.den$). Orientation of a prime axis means whether $\chi$ acts as the identity or as reciprocal on that prime direction.
The multiplicative group of the rational carrier is free abelian on the prime axes, so each prime contributes an independent $\pm 1$ orientation choice. The canonical reciprocal cost $J(x)=(x+x^{-1})/2-1$ corresponds to the all-identity choice, but that choice is not forced by discrete arithmetic alone.
Cross-equivalence (not definitional equality) is the native equality used throughout, so characters remain quotient-correct. Upstream, the continuous Law-of-Logic package forces $J$ only after calibration and connectivity on $(0,\infty)$; the discrete carrier has neither a derivative nor a connected topology.
proof idea
Term proof: exhibit the witness $\chi$ as the two-adic axis twist character. Package three facts already proved for that map: it is a PRC ratio character; on every non-two prime direction it is identity-oriented (the second half of the branch lemma); and it remains only to show it is not identity-oriented at $2$.
Assume for contradiction that the twist is cross-equivalent to the identity on the two-prime direction. Symmetrize that assumption and transit with the first half of the branch lemma (which says the twist sends the two-prime direction to its reciprocal). The result is that the two-prime direction is cross-equivalent to its own reciprocal, contradicting the lemma that no prime direction is cross-equivalent to its reciprocal. Hence the twist is a genuine non-identity orientation at $2$.
why it matters
This is the headline discrete non-forcing blocker for δ-native cost uniqueness. It shows why J-forcing (T5 in the forcing chain, and the continuous law_of_logic_forces_jcost) cannot be closed on the rational carrier alone: free-abelian prime axes leave an independent orientation at $2$ even after locking every odd prime.
Downstream it feeds the $\lambda=2$ cost family member $F_2(x)=(x^2+x^{-2})/2-1$, the completion-side twin of the same underdetermination (calibration fails while other Law-of-Logic axioms hold), and the three-adic axis-twist reciprocity lemma that extends the same construction off the $2$-axis. The doc-comment's repair path is explicit: derive unit calibration from the cost of a single δ-act on the continuous completion, rather than pinning each prime axis by hypothesis. Without that continuous step, the Recognition Composition Law and the unique $J$ remain underdetermined on discrete orbits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.