twoAdicTwistRat_zero
plain-language theorem explainer
The classical two-adic branch twist on rational displays fixes zero: the leading factor of zero annihilates any power of two. Cost-calibration arguments along the two-adic axis cite this as the zero-orbit base case. Proof is a one-line unfold of the twist definition plus the zero-multiplication identity.
Claim. Let $T_2:\mathbb{Q}\to\mathbb{Q}$ be the two-adic branch twist $T_2(x)=x\cdot 2^{-2\,v_2(x)}$. Then $T_2(0)=0$.
background
In the Primitive Recognition Calculus, native cost uniqueness is checked against classical verifier maps on rational displays. The two-adic twist is the branch that fixes odd-prime axes and inverts the orbit-2 exponent: $T_2(x)=x\cdot 2^{-2,v_2(x)}$, where $v_2$ is the 2-adic valuation on $\mathbb{Q}$.
The ambient module builds minimality certificates for native cost functionals generated by such twists. Zero is the distinguished display whose numerator kills every product, so any multiplicative twist must fix it before cost calibration can proceed.
Upstream, the rational zero-multiplication identity (and its LogicNat/PRCInt analogues) supplies the algebraic fact used here; the twist definition itself lives in the uniqueness layer.
proof idea
One-line term proof. Unfold the definition of the two-adic twist, which is a product $x\cdot 2^{-2,v_2(x)}$. Instantiate the zero-multiplication lemma on rationals (or the imported ArithmeticFromLogic/IntegerRational form) to conclude $0\cdot_,=,0$.
why it matters
Feeds the downstream certificate that the two-adic axis-twist cost calibrates the zero orbit (twoAdicGeneratedNativeCost_zero_calibrated). That certificate rewrites the doubled-trace zero-calibration predicate into a cross-equality of ratio orbits and needs $T_2(0)=0$ so the generated native cost matches the zero display on the nose.
In the broader PRC stack this is a bookkeeping lemma on the uniqueness-to-minimality path: before comparing native cost against character-generated costs, the verifier twist must preserve the zero orbit. It does not itself invoke J-uniqueness (T5), phi, or the eight-tick octave, but it sits under the native-cost uniqueness layer that those landmarks eventually constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.