liouvilleTwistDisplay_inv
plain-language theorem explainer
The Liouville-twisted display of a rational is reciprocal-compatible: twisting then inverting equals inverting then twisting. Anyone building the native-cost certificate for the Liouville twist cites this when checking the reciprocal axiom of the slim field. The proof splits on zero and, off zero, uses that the Liouville sign is involutive under inversion and squares to one.
Claim. For every rational $t$, if $D(t)$ denotes the Liouville-twisted display $D(t)=\lambda(t)\,t$ with $\lambda(t)=(-1)^{\Omega(|\mathrm{num}\,t|)+\Omega(\mathrm{den}\,t)}$, then $D(t^{-1})=D(t)^{-1}$.
background
In the Primitive Recognition Calculus native-cost certificate, displays are rational quantities on which a cost functional is evaluated. The Liouville sign $\lambda(t)$ is $(-1)$ raised to the total number of prime factors (with multiplicity) of the absolute numerator and the denominator of the reduced fraction; Mathlib totalizes $\Omega(0)=0$, so $\lambda(0)=+1$. The twisted display is the product $D(t)=\lambda(t),t$.
Upstream facts already established in this module: $\lambda(t)^2=1$ for all $t$, $\lambda(t)\neq 0$, and $\lambda(t^{-1})=\lambda(t)$ whenever $t\neq 0$. The zero case of the display is handled separately ($D(0)=0$). These are the only ingredients needed for reciprocal compatibility of $D$.
The local setting is the search for a native cost on ratio orbits that satisfies the slim-field axioms short of the two-point calibration anchor, as preparation for uniqueness of the $J$-cost in the forcing chain.
proof idea
Case split on $t=0$. If $t=0$, rewrite and apply the zero lemma for the twisted display (both sides become $0^{-1}$ in the extended sense already fixed by that lemma, or simplify directly). If $t\neq 0$, expand both sides by the definition $D(u)=\lambda(u),u$, invoke $\lambda(t^{-1})=\lambda(t)$, and use multiplicativity of inversion. It remains to replace $\lambda(t)^{-1}$ by $\lambda(t)$: from $\lambda(t)^2=1$ and $\lambda(t)\neq 0$, field simplification plus a short linear-arithmetic step yields the identity. Rewrite and finish.
why it matters
Reciprocal compatibility is one of the slim-field axioms demanded of a native cost. This lemma is applied inside liouvilleTwistNativeCost_sans_two_hypotheses, whose doc-comment states that the Liouville twist satisfies every slim field axiom except the two-point anchor. That certificate is a step toward showing that the unique cost compatible with the Recognition Composition Law is the $J$-cost $J(x)=(x+x^{-1})/2-1$ (forcing landmark T5). Without inversion-compatibility of the twisted display, the Liouville candidate could not even enter the slim-field comparison. The remaining open piece on this branch is the two-point calibration, not reciprocity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.