twoAdicAxisTwistCharacter_ratio_character
plain-language theorem explainer
The two-adic axis twist on ratio orbits is a full PRC ratio character: unit-preserving, multiplicative, reciprocal, normalization-invariant, and nonzero-preserving under cross-equivalence. Downstream uniqueness and orientation results cite it as the concrete counterexample character that flips only the orbit-2 axis. The proof discharges each structure field by reducing via toRat to the corresponding rational twist lemmas.
Claim. The two-adic axis twist map $\chi$ on ratio orbits is a PRC ratio character: $\chi(1)\sim 1$, $\chi(xy)\sim\chi(x)\chi(y)$, $\chi(x^{-1})\sim\chi(x)^{-1}$ under cross-equivalence, $\chi$ is invariant under ratio normalization, and $\chi$ sends nonzero orbits to nonzero orbits.
background
In the Primitive Recognition Calculus, costs admit a d'Alembert-style factorization through ratio characters. A PRCRatioCharacter is a map $\chi$ on ratio orbits that is unit-fixing, multiplicative, reciprocal, normalization-invariant, and nonzero-preserving, all stated with cross-equivalence rather than definitional equality so the structure stays quotient-native.
Ratio orbits carry a rational display toRat. Cross-equivalence of orbits is equivalent to equality of those displays (crossEq_iff_toRat_eq), and the orbit operations (one, mul, recip, normalize) commute with toRat. The two-adic axis twist is the orbit-level lift of the rational map $x\mapsto x\cdot 2^{-2v_2(x)}$: it multiplies by a pure power of 2 that cancels twice the 2-adic valuation, leaving odd primes fixed in orientation and inverting the 2-axis.
This module studies whether native PRC cost hypotheses force a unique admissible character. The twist is the standard non-identity candidate used to test that claim.
proof idea
Tactic proof that builds the PRCRatioCharacter structure field by field. Each field rewrites the cross-equivalence goal through crossEq_iff_toRat_eq and twoAdicAxisTwistCharacter_toRat, then applies the matching rational lemma:
- unit: reduce to
twoAdicTwistRat_oneviaone_toRat; - multiplicative: reduce to
twoAdicTwistRat_mulvia two uses ofmul_toRat; - reciprocal: reduce to
twoAdicTwistRat_invvia two uses ofrecip_toRat; - normalized_invariant: both sides display the same rational after
normalizeRatio_toRat; - nonzero_preserving: reduce to
twoAdicTwistRat_ne_zero.
No new algebra is done at the orbit level; the work is transport along the toRat bridge.
why it matters
This is the certificate that the two-adic axis twist is a legitimate ratio character, not an ad-hoc map. It is the witness inside prc_native_cost_orientation_underdetermined: there exists a full PRC ratio character that is identity-oriented on every odd prime axis and reciprocal-oriented on orbit 2. That underdetermination is the headline blocker for naive native-cost uniqueness.
Downstream, it feeds the refutations PRCNativeCostUniquenessTarget_refuted, PRCNoAdmissibleFactorForTwoAdicAxisTwistGeneratedCost, the factorization-admissibility upgrade negation, and several prime-calibration forcing targets (local orientation, reciprocal branch transport, prime-floor successor steps). Those results show that prime calibration alone does not pin orientation or force the canonical cost factor once this twist is admitted.
In the broader Recognition chain this sits under cost uniqueness / J-factorization pressure (toward T5 J-uniqueness and the RCL), clarifying that extra structure beyond a bare ratio character is needed before the native cost is forced.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.