axisTwistCharacter_on_axis_reciprocal
plain-language theorem explainer
For any prime distinction orbit p, the axis-twist character attached to p sends the p-axis direction to its reciprocal, up to cross-equivalence of ratio orbits. Anyone proving per-prime orientation freedom for δ-native PRC cost cites this identity. The proof installs the Nat-prime fact, rewrites to rational displays, and closes by the self-reciprocal rational twist lemma.
Claim. Let $p$ be a prime distinction orbit. Then the axis-twist character of $p$, evaluated at the prime direction of $p$, is cross-equivalent (by balanced scaled numerators and denominators) to the reciprocal of that same prime direction.
background
In the Primitive Recognition Calculus, ratios live as RatioOrbit data built from signed δ-orbits, not bare rationals. Two orbits are identified by cross-equivalence: numerators and denominators balance after scaling, which is the internal PRC stand-in for rational equality (K4.10). Reciprocal flips a ratio orbit in that same language.
A prime orbit is a distinction-nat whose display is a genuine Nat prime; natPrime_toNat_of_primeOrbit is the bridge that imports ordinary prime factorization. The prime direction is the positive ratio orbit along that prime axis. An axis-twist character is a PRC ratio character engineered to invert one chosen prime axis while leaving the others fixed in orientation.
This module studies uniqueness and non-uniqueness of δ-native cost: which ratio characters are compatible with native cost hypotheses, and which axis orientations those hypotheses actually force.
proof idea
Term-mode proof with a short rewrite chain. First install Fact (Nat.Prime p.toNat) from natPrime_toNat_of_primeOrbit, so downstream rational lemmas that need a prime witness fire. Rewrite the goal via crossEq_iff_toRat_eq into equality of rational displays. Unfold axisTwistCharacter_toRat, recip_toRat, and primeDirection_toRat so both sides become ordinary rationals built from p.toNat. Finish with axisTwistRat_self on that natural prime: the rational twist map is self-reciprocal on its own prime.
why it matters
This is the on-axis evaluation step for the twist character: it really does invert the chosen prime direction. The sole direct consumer is prc_every_prime_axis_orientation_free, the headline δ-native cost non-forcing theorem: for every prime orbit there exists a PRC ratio character that fixes every other prime axis yet inverts the p-axis. That result replaces earlier per-prime witnesses (p=2 orientation underdetermined, p=3 single-prime calibration insufficient) by a uniform per-axis statement.
In the Recognition framework this is foundation-layer structure under the J-cost and RCL story (T5 J-uniqueness, native cost as doubled trace). It does not choose a physical orientation; it classifies residual gauge freedom once native cost hypotheses are fixed, so cost uniqueness cannot silently pin prime-axis signs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.