liouvilleSign
plain-language theorem explainer
The Liouville-type sign of a rational is $(-1)$ raised to the total number of prime factors (with multiplicity) in the reduced numerator and denominator. It equals $+1$ at zero by the convention $\Omega(0)=0$, and equals $-1$ on every prime. Multiplicativity lemmas and the twisted-display construction in the native cost-minimality certificate cite it as the discrete sign character on $\mathbb{Q}$. The body is a one-line power of $-1$.
Claim. For $t\in\mathbb{Q}$, define the Liouville-type sign by $\mathrm{sign}_L(t)=(-1)^{\Omega(|\mathrm{num}(t)|)+\Omega(\mathrm{den}(t))}$, where $\Omega$ is the total prime-factor count with multiplicity on the reduced fraction, and $\Omega(0)=0$ so that $\mathrm{sign}_L(0)=+1$. The value is always $\pm 1$, and equals $-1$ on every prime.
background
In classical number theory the Liouville function is $\lambda(n)=(-1)^{\Omega(n)}$ on the naturals, completely multiplicative and equal to $-1$ on primes. Here the same parity is lifted to a reduced rational $t=\mathrm{num}/\mathrm{den}$ by adding the factor counts of $|\mathrm{num}|$ and $\mathrm{den}$. Mathlib's $\mathrm{cardFactors}$ sets $\Omega(0)=0$, so the sign is well-defined and $+1$ at zero.
The surrounding module builds a native cost-minimality certificate for the Primitive Recognition Calculus. A companion construction, the twisted display, multiplies a rational display coordinate by this sign. Upstream, finite Hilbert displays package $F_{RS}[i]$ amplitudes as vectors; the sign character is the arithmetic ingredient that later controls parity and cancellation in products of those coordinates.
Notation: $\Omega$ is Mathlib's arithmetic function $\mathrm{cardFactors}$; numerator and denominator are those of the reduced fraction in $\mathbb{Q}$.
proof idea
Pure definition: evaluate $(-1)$ to the power $\Omega(|t.\mathrm{num}|)+\Omega(t.\mathrm{den})$. No lemmas are applied; the body is the arithmetic expression itself. Downstream proofs unfold this definition and use $\mathrm{cardFactors}$ identities (additivity on coprime factors, value $1$ on primes, value $0$ on $1$) together with reduced-fraction numerator/denominator calculus.
why it matters
This sign is the discrete character underlying the twisted display $\mathrm{sign}_L(t)\cdot t$ and the whole certificate suite in the same module. Immediate consumers prove: the square is identically $1$; the value is never zero; it is $1$ at $\pm 1$; it is completely multiplicative on nonzero rationals (cancellation of common prime factors preserves total parity); it is invariant under inversion; and it equals $-1$ on every prime. Those facts let the twisted display stay inside the same arithmetic class while flipping parity on prime rungs, which is the bookkeeping needed for native cost comparisons in the Primitive Recognition Calculus. It does not itself invoke the forcing chain (T5--T8) or the Recognition Composition Law; it is pure arithmetic scaffolding for the cost certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.