liouvilleTwistNativeCost
plain-language theorem explainer
Defines the Liouville-twisted native cost on rational orbits: apply the PRC J-cost to the signed display liouvilleSign(t)·t, sending the unit orbit to the literal zero representative. Used as the countermodel that satisfies every slim native-cost axiom except the two-point calibration anchor. Construction is a case split on the unit, then compose the twist display with the orbit section and onRatioOrbit.
Claim. For a rational orbit $q$, the Liouville-twisted native cost is the zero orbit when the verifier rational of $q$ is $1$, and otherwise the PRC $J$-cost $J(r)=((r+r^{-1})/2)-1$ evaluated on the orbit section of the twisted display $\mathrm{liouvilleSign}(t)\cdot t$ at $t=q$'s verifier rational.
background
In the Primitive Recognition Calculus, costs live on ratio orbits: structures with a signed-orbit numerator and a nonzero distinction-nat denominator. The verifier map toRat recovers the ordinary rational $q.\mathrm{num}/q.\mathrm{den}$. The native PRC $J$-cost on such an orbit is the orbit-level object $J(q)=((q+q^{-1})/2)-1$, matching the T5 uniqueness form $J(x)=(x+x^{-1})/2-1$.
The Liouville twist display multiplies a rational $t$ by a sign character liouvilleSign t, producing the twisted input $\mathrm{liouvilleSign}(t)\cdot t$. The section ratioOrbitOfRat lifts ordinary rationals back into ratio orbits so that classical rational countermodels can be tested against the PRC character interface without inventing new primitives.
This module builds certificates that the slim native-cost axiomatization needs a two-point calibration anchor. The twisted cost is the explicit competitor used in those certificates.
proof idea
Definition by cases, not a proof. If the verifier rational of the input orbit equals $1$, return the literal zero orbit (exact-unit wrapper). Otherwise: read $t=q.\mathrm{toRat}$, form the twisted display $\mathrm{liouvilleSign}(t)\cdot t$, lift it via ratioOrbitOfRat, and apply onRatioOrbit (the orbit-level $J$). Downstream lemmas such as liouvilleTwistNativeCost_toRat discharge the case split and recover the closed form $J(\mathrm{liouvilleTwistDisplay},t)$ on the verifier side.
why it matters
This definition is the concrete countermodel that forces the two-point anchor in the PRC native-cost uniqueness story. Downstream, liouvilleTwistNativeCost_sans_two_hypotheses shows it meets every slim field axiom except the two-point calibration; liouvilleTwistNativeCost_two_not_canonical shows it fails at orbit $2$, displaying $J(-2)=-9/4$ against the canonical $J(2)=1/4$; and PRCSlimSansTwoCalibrationUniquenessTarget_refuted concludes that slim-minus-two-calibration uniqueness is false.
In framework terms it protects the T5 $J$-uniqueness lineage at the rational-orbit level: without the two-point anchor, a Liouville-signed twist of the same functional shape would be admitted. The construction is local to the minimality-certificate module and does not itself claim uniqueness; it supplies the witness that uniqueness needs the anchor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.