twoAdicTwistRat_neg_one
plain-language theorem explainer
The two-adic rational twist character sends the signed unit −1 to −1, because the 2-adic valuation of −1 vanishes. Downstream signed-unit calibration of the two-adic generated native cost cites this identity. The proof unfolds the twist, reduces to padicValRat 2 (−1) = 0 via the negation rule and non-divisibility of 1 by 2, then finishes by arithmetic.
Claim. The two-adic twist character on rationals satisfies $\mathrm{tw}_2(-1)=-1$. Equivalently, because the $2$-adic valuation $v_2(-1)$ is zero, the twist evaluates to the signed unit rather than to $+1$.
background
In the Primitive Recognition Calculus, native cost functionals on ratio orbits are built from multiplicative characters and J-type costs. The two-adic twist on rationals is one such character: it reads the $2$-adic valuation of a rational (and the ambient sign data) to produce a $\pm 1$ factor used when generating a native cost along the two-adic axis.
The local module certifies minimality and calibration properties of that two-adic generated native cost. Signed units matter because the recognition cost must treat the orientation-reversing unit $-1$ consistently with the orbit cross-equation and with the comparator-derived cost (the doubled $J$-cost in the engine).
Upstream, $v_2$ on $\mathbb{Q}$ is the standard $2$-adic valuation; Mathlib supplies padicValRat.neg and the fact that $v_2(1)=0$ since $2\nmid 1$. The twist definition (from the uniqueness development) is unfolded here only far enough to expose that valuation.
proof idea
Tactic proof. Unfold the definition of the two-adic rational twist. Prove the side fact $v_2(-1)=0$ by rewriting with the negation rule for padicValRat, then norm_num with padicValRat.of_int and padicValInt.eq_zero_of_not_dvd (so $2$ does not divide $1$). Substitute that valuation into the unfolded twist and close with norm_num, which evaluates the remaining arithmetic to $-1$.
why it matters
Feeds the parent theorem twoAdicGeneratedNativeCost_signed_unit, whose doc-comment states that the two-adic axis-twist cost calibrates the signed unit. That calibration is the bridge from the character on $\mathbb{Q}$ to the native-cost predicate PRCNativeCostSignedUnitCalibrated on the two-adic generated cost, via a cross-equation transport on the negative-one ratio orbit.
In the Recognition forcing picture this is bookkeeping on the discrete multiplicative skeleton before continuum $J$-uniqueness (T5) and the $\varphi$ fixed point (T6): the cost must fix orientation so that signed units do not spuriously raise recognition cost. Without $\mathrm{tw}_2(-1)=-1$, the signed-unit calibration lemma fails and the minimality certificate for the two-adic native cost cannot close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.