liouvilleSign_neg_one
plain-language theorem explainer
The Liouville-type arithmetic sign of the rational −1 equals +1. Anyone working the twisted-display identities in the native cost-minimality certificate cites this base case. The proof unfolds the definition and evaluates the total prime-factor count of the reduced fraction by norm_num.
Claim. For the Liouville-type sign on rationals, defined by $\operatorname{sign}(t)=(-1)^{\Omega(|n|)+\Omega(d)}$ where $t=n/d$ is in lowest terms, one has $\operatorname{sign}(-1)=1$.
background
In the Primitive Recognition Calculus native cost-minimality certificate, rational displays carry a Liouville-type sign: for a reduced fraction $t=n/d$, the sign is $(-1)$ raised to the total number of prime factors (with multiplicity) of $|n|$ and of $d$. Mathlib's $\Omega$ totalizes $\Omega(0)=0$, so the sign is $+1$ at zero; it is $-1$ on every prime and $\pm 1$ everywhere.
The twisted display is then this sign times the rational itself. The identity event in ObserverForcing sits at the J-cost minimum $x=1$; the present lemma is the parallel arithmetic base case at $-1$, needed before multiplicative and inverse laws for the sign can be applied cleanly to signed displays.
Local setting is the certificate layer over PRC native cost minimality: one builds enough arithmetic of the sign to control the twisted display on a generating set of rationals.
proof idea
Term-mode one-liner in spirit, written as two tactics: rewrite by the definition of the sign, then norm_num. For $t=-1$ the reduced numerator has absolute value $1$ and the denominator is $1$, so both $\Omega$ counts vanish and $(-1)^{0+0}=1$.
why it matters
Feeds directly into liouvilleTwistDisplay_neg_one, which concludes that the twisted display of $-1$ is $-1$ by rewriting the twist definition, applying this lemma, and simplifying $1\cdot(-1)$. That base case is part of the arithmetic scaffolding that certifies native cost minimality for rational displays in the Primitive Recognition Calculus.
Within the broader Recognition framework this sits in Foundation, upstream of the forcing chain (T5 J-uniqueness, T6 $\varphi$, T7 eight-tick, T8 $D=3$). It does not itself force a physical constant; it locks the sign convention so later multiplicative identities for the twist remain consistent on negative units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.