twoAdicTwistRat_primeDirection_of_ne_two
plain-language theorem explainer
For every native prime orbit other than the two-step orbit, the verifier two-adic twist acts as the identity on the rational display of that prime's direction. Used when assembling the two-adic axis twist character for native cost uniqueness. The proof unfolds the twist definition and substitutes vanishing of the 2-adic valuation.
Claim. Let $p$ be a prime distinction-orbit with $p \neq 2$. Write $\mathrm{dir}(p)$ for the prime direction of $p$ and $(\cdot)^{\mathbb{Q}}$ for its rational display. Then the two-adic twist satisfies $\mathrm{twist}_2\bigl(\mathrm{dir}(p)^{\mathbb{Q}}\bigr) = \mathrm{dir}(p)^{\mathbb{Q}}$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12). A prime orbit is a nonzero, non-unit position with no nontrivial factorization. The distinguished two-step orbit is the native stand-in for $2$.
Each prime orbit $p$ has a prime direction, displayed as a rational via toRat (spec tag A5: a transport wrapper whose internal content is cross-multiplication). The two-adic twist on rationals is the verifier realization of the branch twist along the $2$-adic axis; it is built from the $2$-adic valuation padicValRat 2.
The immediate upstream fact is that for any prime orbit other than the two-orbit, that valuation on the prime-direction rational is zero: padicValRat 2 (dir(p)^Q) = 0.
proof idea
Short tactic proof. Unfold the definition of the two-adic twist on rationals. Rewrite the $2$-adic valuation factor by the upstream lemma padicValRat_two_primeDirection_eq_zero_of_ne_two (using primality of $p$ and $p \neq 2$). The resulting arithmetic identity is closed by norm_num, which reduces the twist at valuation zero to the identity map on the rational.
why it matters
Native cost uniqueness in PRC needs a clean description of how the two-adic axis twist character acts on prime directions. This lemma supplies the off-two case: the twist is invisible on every prime direction other than $2$.
It is consumed by twoAdicAxisTwistCharacter_branch, which packages the full two-adic axis twist as a PRCCharacterTwoAdicAxisTwist (the on-two branch is handled separately by twoAdicTwistRat_two). That character is part of matching doubled-trace data to the native $J$-cost side of the Recognition Composition Law, feeding the uniqueness argument for the PRC native cost.
In the broader forcing chain this sits under foundation work toward T5 $J$-uniqueness, not a direct T0–T8 step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.