PRCTwoAdicAxisTwistRatioCharacter_constructed
plain-language theorem explainer
Existence of a ratio character on the rational orbit carrier that is identity-oriented on every odd prime yet reciprocal-oriented on the prime 2: the two-adic axis twist x ↦ x · 2^(-2 v₂(x)). Anyone arguing that discrete δ-native axioms force the all-identity branch of J will cite this countermodel. The proof is a three-field term packing an already-built character with its ratio-character and branch lemmas.
Claim. There exists a map $\chi$ on ratio orbits that is a full PRC ratio character (reciprocal-symmetric, multiplicative, normalized, nonzero-preserving) and realizes the two-adic axis twist: identity orientation on every odd prime axis and reciprocal orientation on the prime-$2$ axis.
background
In the Primitive Recognition Calculus the rational carrier is organized by ratio orbits. A PRC ratio character is a self-map of those orbits that is multiplicative, reciprocal-symmetric, normalized, and nonzero-preserving. Each prime axis of $\mathbb{Q}^\times$ (free abelian on the primes) may be oriented either as the identity or as the reciprocal; the character records that choice.
The two-adic axis twist is the concrete map $x \mapsto x \cdot 2^{-2 v_2(x)}$. It flips only the $2$-axis and leaves every odd prime axis identity-oriented. The target proposition asserts that this map is already a full ratio character carrying that branch signature.
Upstream, the continuous Law of Logic (law_of_logic_forces_jcost) forces the unique reciprocal cost $J(x)=\frac{x+x^{-1}}{2}-1$ once calibration and continuity are present on $(0,\infty)$. On the discrete rational carrier there is neither a derivative nor path-connectivity, so per-prime orientation freedom can survive. Multiplicativity and reciprocity of $J$-automorphisms supply the algebraic language in which the character is checked.
proof idea
Term-mode existential introduction. The witness is the already-constructed twoAdicAxisTwistCharacter. The second field applies the lemma that this map satisfies the full PRC ratio-character package (multiplicativity, reciprocity, normalization, nonzero-preservation). The third field applies the branch lemma recording identity orientation on odd primes and reciprocal orientation on $2$. No further tactic work; the three components discharge the $\exists$ packaging of the target proposition.
why it matters
This is the headline discrete non-forcing witness for $\delta$-native cost uniqueness. Downstream it is fed directly into the refutation that prime calibration forces uniform identity orientation on every prime axis: the refutation is literally the not-of-axis-twist lemma applied to this construction. That blocks any claim that the discrete arithmetic alone pins the all-identity branch of $J$.
In the broader Recognition chain this explains why T5 J-uniqueness (and the RCL route through law_of_logic_forces_jcost) must pass through the continuous completion: the free-abelian prime-axis structure leaves an independent orientation bit at $2$ that discrete reciprocal-character axioms cannot kill. The forward repair named in the module is to derive unit calibration from the cost of a single $\delta$ act on the completion, not to pin each prime by hypothesis. The construction also appears in the conditional universal-foundation certificate as part of the native-cost uniqueness ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.