liouvilleSign_mul
plain-language theorem explainer
The Liouville-type sign on nonzero rationals is completely multiplicative: the sign of a product equals the product of the signs. Anyone tracking parity of total prime factors through rational multiplications in the PRC native-cost certificate cites this. The proof equates Ω-parities via the reduced-fraction cross identity and Mathlib cardFactors multiplicativity, then reduces (−1)^n through mod-2.
Claim. For nonzero rationals $t_1, t_2 \in \mathbb{Q}^{\times}$, if $\sigma(t) = (-1)^{\Omega(|\mathrm{num}\, t|) + \Omega(\mathrm{den}\, t)}$ denotes the Liouville-type sign (total prime-factor count with multiplicity on the reduced fraction), then $\sigma(t_1 t_2) = \sigma(t_1)\,\sigma(t_2)$.
background
In the Primitive Recognition Calculus native-cost certificate, each rational display carries a Liouville-type sign $\sigma(t) = (-1)^{\Omega(|\mathrm{num}, t|) + \Omega(\mathrm{den}, t)}$, where $\Omega$ is Mathlib's total prime-factor count (with multiplicity). The sign is $-1$ on every prime and $\pm 1$ everywhere; Mathlib sets $\Omega, 0 = 0$, so the value at zero is conventionally $+1$.
The twisted display is the product of this sign with the rational itself. Multiplicativity of the sign is the arithmetic engine behind multiplicativity of the twist. The key upstream identity is the reduced-fraction cross relation: numerators and denominators of $t_1 t_2$ differ from the raw products only by a common cancelled factor, so total $\Omega$-parity is invariant under that cancellation.
Local setting is Foundation PRC cost-minimality bookkeeping: signs must pass cleanly through products and inverses before one can certify that twisted displays of prime pairs remain positive and that the native cost functional stays minimal on the intended orbit.
proof idea
Establish that absolute numerators and denominators of $t_1$, $t_2$, and $t_1 t_2$ are nonzero (via rational nonzeroness and den_ne_zero). Apply the cross identity rat_mul_num_den_cross, take natAbs, and obtain an equality of natural products. Multiplicativity of $\Omega = \mathtt{cardFactors}$ on those products yields an additive relation among the six $\Omega$-values. An omega step rearranges to congruence of total parities mod 2. Unfold three copies of the sign definition, rewrite $(-1)^{a+b}$ and reduce exponents mod 2 via neg_one_pow_eq_pow_mod_two, then substitute the parity congruence.
why it matters
This is the multiplicative core of the Liouville-sign calculus in the PRC native-cost certificate. Downstream, liouvilleSign_inv obtains sign-invariance under inversion by multiplying by the inverse and using $\sigma(1)=1$. The twisted display then inherits complete multiplicativity (liouvilleTwistDisplay_mul), which immediately gives cancellation of signs on products of two primes (liouvilleTwistDisplay_prime_pair): signs cancel so the twisted display of $p\cdot r$ equals $p\cdot r$ itself.
In the broader Recognition stack this is pure arithmetic scaffolding for cost-minimality bookkeeping on rational displays, not a forcing-chain step (T5–T8). It ensures the sign twist is a group homomorphism $\mathbb{Q}^{\times}\to{\pm 1}$, so orbit products and prime-pair displays stay under control when certifying native cost minima.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.