liouvilleTwistDisplay_ne_zero
plain-language theorem explainer
If a rational twist parameter is nonzero, its Liouville-twisted display (sign times the parameter) is nonzero. Cost-minimality and slim-field certificates for the Liouville twist cite this to keep the display off zero. The proof is a one-line product-nonzero wrapper from the always-nonzero Liouville sign and the hypothesis.
Claim. For every rational $t \neq 0$, the twisted display $\mathrm{sign}_L(t)\cdot t$ is nonzero, where $\mathrm{sign}_L$ is the Liouville sign on $\mathbb{Q}$.
background
In the Primitive Recognition Calculus native-cost layer, the Liouville twist is a candidate cost display built from a sign factor on rationals. The twisted display is defined by $\mathrm{liouvilleTwistDisplay}(t) := \mathrm{liouvilleSign}(t)\cdot t$: the Liouville sign times the rational parameter itself.
The Liouville sign is never zero on $\mathbb{Q}$ (proved by unfolding and positivity). The ambient setting is the certificate module that checks which slim-field axioms a native cost satisfies without the two-point calibration anchors. Non-vanishing of the twisted display is a local arithmetic hygiene fact needed before reciprocal and cross-ratio identities can be stated for the twist.
proof idea
One-line wrapper. Apply the standard product-nonzero lemma to the pair $(\mathrm{liouvilleSign}, t,, t)$: the first factor is nonzero by liouvilleSign_ne_zero, the second by the hypothesis $t \neq 0$. The definition of the twisted display is exactly that product, so the display is nonzero.
why it matters
Feeds liouvilleTwistNativeCost_sans_two_hypotheses, which asserts that the Liouville twist satisfies every slim-field axiom except the two-point anchor. That certificate is part of the PRC native-cost minimality story: identifying which displays can serve as recognition costs before full calibration.
In the broader Recognition framework this sits in Foundation, under Primitive Recognition Calculus, not yet at the T5 J-uniqueness or RCL layer. It is bookkeeping that keeps the Liouville-twisted display off zero so later reciprocal and orbit-arithmetic steps remain well-defined. No open scaffold: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.