threeAdicTwistRat_ne_zero
plain-language theorem explainer
For every nonzero rational x, the three-adic branch twist of x is nonzero. Anyone building the three-adic axis twist into a PRC ratio character needs this non-vanishing fact first. The argument unfolds the twist as a product and applies the standard nonzero-product and integer-power rules on Q.
Claim. If $x\in\mathbb{Q}$ satisfies $x\neq 0$, then $x\cdot 3^{-2\,v_3(x)}\neq 0$, where $v_3$ denotes the $3$-adic valuation on rationals.
background
In Primitive Recognition Calculus, native-cost uniqueness is tested by twisting rational displays along single prime axes. The three-adic twist multiplies a rational by a power of three that inverts twice its 3-adic valuation: it leaves every prime axis other than 3 fixed and flips the orbit-3 exponent. It is the base-3 analogue of the two-adic twist, introduced so that calibration of the native cost against J at the prime 2 need not force agreement on other primes such as 3.
The surrounding module develops uniqueness of the native cost under PRC hypotheses, via ratio characters and doubled-trace D'Alembert structure. Non-vanishing of the twist on Q^x is a basic algebraic gate before the twist can be promoted to a ratio character.
proof idea
Unfold the definition: the twist is the product of x with an integer power of 3. A numeric check gives 3 ≠ 0 in Q. Any integer power of a nonzero rational is nonzero, so the second factor is nonzero. The product of two nonzero rationals is nonzero, which closes the goal.
why it matters
The lemma is consumed when showing that the three-adic axis twist character satisfies the PRC ratio-character interface. That step sits inside the native-cost uniqueness program: one exhibits a twist that keeps the ratio-character axioms while disagreeing with the J-calibrated cost on the 3-axis, proving that single-prime calibration does not propagate. In the Recognition Science forcing chain this supports T5 J-uniqueness (J(x)=(x+x^{-1})/2-1) as the unique native cost only after the full PRC hypothesis package is imposed, not after agreement at one prime alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.