liouvilleSign_mul_self
plain-language theorem explainer
For every rational t, the Liouville-type sign of t squares to 1. Anyone proving inversion or multiplicativity identities for the twisted rational display in the native cost-minimality certificate cites this as the basic involution fact. The proof unfolds the definition and closes by power laws: the product is (-1) to an even exponent.
Claim. For every rational $t$, writing $\sigma(t)=(-1)^{\Omega(|\mathrm{num}(t)|)+\Omega(\mathrm{den}(t))}$ for the Liouville-type sign of $t$ (total prime-omega of reduced numerator and denominator), one has $\sigma(t)\cdot\sigma(t)=1$.
background
The Liouville-type sign of a rational is $(-1)$ raised to the total number of prime factors counted with multiplicity in the absolute numerator and the denominator of the reduced fraction. Mathlib's $\Omega$ totalizes $\Omega(0)=0$, so the sign is $+1$ at zero; it is $-1$ on every prime and $\pm 1$ on all rationals.
This module builds algebraic certificates for a twisted display $\sigma(t)\cdot t$ used in Primitive Recognition Calculus native cost-minimality arguments. The bare sign is the local definition $\sigma(t)=(-1)^{\Omega(|t.num|)+\Omega(t.den)}$.
The present identity is the elementary fact that $\sigma$ takes values in ${\pm 1}$ and is an involution under multiplication, which later lemmas need when moving factors across products and inverses.
proof idea
Unfold $\sigma(t)$ on both factors. Rewrite the product of powers as a single power via pow_add, so the exponent becomes $2n$ with $n=\Omega(|\mathrm{num}|)+\Omega(\mathrm{den})$. Factor the exponent by two_mul, apply pow_mul to obtain $((-1)^2)^n$, and finish with norm_num ($1^n=1$). No external lemmas beyond the definition and power arithmetic.
why it matters
Parent uses are liouvilleSign_inv (sign is invariant under rational inversion for $t\neq 0$) and liouvilleTwistDisplay_inv (the twisted display of an inverse is the inverse of the twisted display). Both rewrite through the square identity to cancel a pair of signs.
In the PRC native cost-minimality certificate, the twist $\sigma(t)\cdot t$ must behave cleanly under the multiplicative group of nonzero rationals so that cost comparisons stay well-defined after inversion and products. This one-line involution is the first algebraic brick in that chain; without $\sigma(t)^2=1$, the inversion lemmas for the display do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.