liouvilleSign_one
plain-language theorem explainer
The Liouville-type sign of the rational 1 equals +1. Anyone normalizing twisted displays or proving multiplicativity of the sign cites this base case. The proof unfolds the definition and evaluates the total prime-factor count of 1/1 by arithmetic.
Claim. The Liouville-type sign of the rational $1$ is $+1$: if $\mathrm{sign}(t)=(-1)^{\Omega(|\mathrm{num}(t)|)+\Omega(\mathrm{den}(t))}$ for $t\in\mathbb{Q}$, then $\mathrm{sign}(1)=1$.
background
In the Primitive Recognition Calculus native-cost certificate layer, rationals carry a Liouville-type sign: for $t\in\mathbb{Q}$, take the reduced fraction and raise $(-1)$ to the sum of big-Omega prime-factor counts of the absolute numerator and the denominator. Mathlib sets $\Omega 0=0$, so the sign is $+1$ at zero; every prime gets $-1$, and the value is always $\pm 1$.
The twisted display is this sign times $t$ itself. Base values at $0$ and $1$ anchor later algebraic identities (multiplicativity, inversion, prime casts) used when certifying that the native cost is minimal among competing displays.
proof idea
One-step unfold of the definition of the Liouville sign, then norm_num on the exponents: numerator and denominator of $1$ are both $1$, each with $\Omega(1)=0$, so $(-1)^{0+0}=1$.
why it matters
Feeds two immediate parents in the same certificate module: inversion invariance of the sign (which rewrites $t\cdot t^{-1}=1$ and needs $\mathrm{sign}(1)=1$), and the twisted-display evaluation at $1$ (sign times $1$). Those identities sit in the PRC native-cost minimality certificate stack, which supports the foundation claim that the Recognition cost $J$ is the unique minimal native cost on rational displays. No open scaffold: the result is fully proved and purely arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.