liouvilleSign_natCast_prime
plain-language theorem explainer
For any prime p, the Liouville-type sign of p as a rational equals -1. Anyone building twisted rational displays for the PRC native-cost certificate cites this base case. The proof unfolds the sign definition on the reduced fraction p/1 and applies Mathlib's Ω-count on primes and on 1, then closes by arithmetic.
Claim. If $p\in\mathbb{N}$ is prime, then the Liouville-type sign of the rational $p$ equals $-1$: $(-1)^{\Omega(|\mathrm{num}(p)|)+\Omega(\mathrm{den}(p))}=-1$.
background
In the Primitive Recognition Calculus native-cost certificate, rationals are displayed with a Liouville-type sign: for $t\in\mathbb{Q}$, $\mathrm{liouvilleSign}(t)=(-1)^{\Omega(|t_{\mathrm{num}}|)+\Omega(t_{\mathrm{den}})}$, where $\Omega$ is Mathlib's total prime-factor count with multiplicity ($\Omega(0)=0$). The sign is therefore $\pm 1$ everywhere and $+1$ at $0$. The twisted display is that sign times $t$ itself.
The local module certifies analytic cost-minimality statements that need controlled sign flips on prime and composite rational displays. Upstream, the sign is defined exactly as the power of $-1$ on the sum of $\Omega$ of absolute numerator and denominator of the reduced fraction; the present lemma is the prime base case of that definition.
proof idea
Term-mode rewrite chain. Unfold the sign definition, then replace numerator and denominator of the natural cast $p:\mathbb{Q}$ by $p$ and $1$ (and absolute value of the integer cast). Apply Mathlib's $\Omega(p)=1$ for prime $p$ and $\Omega(1)=0$. The remaining power $(-1)^{1+0}$ is discharged by norm_num.
why it matters
Feeds the twist-value layer of the PRC native-cost certificate. Downstream, liouvilleTwistDisplay_two specialises it at $p=2$ to get twisted display $-2$, and liouvilleTwistDisplay_prime_pair uses the multiplicative law together with this prime evaluation so that signs cancel on products of two primes (including squares). Those identities keep twisted rational displays equal to the untwisted product on prime pairs, which is the bookkeeping needed when the certificate compares native cost against Liouville-twisted competitors. No forcing-chain landmark (T5–T8) is touched directly; this is arithmetic scaffolding inside the cost-minimality certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.