IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate
Certificate layer for native cost minimality in the Primitive Recognition Calculus. It introduces a Liouville-type sign on rational displays and a twist display built from it, together with the elementary multiplicative identities needed downstream. Anyone proving structural ledger identities for PRC native cost cites this module. The content is definitional plus short algebraic lemmas on prime-factor parity.
claimOn rationals, define the Liouville-type sign $\lambda(q)=(-1)^{\Omega(\mathrm{num})+\Omega(\mathrm{den})}$ of a reduced fraction $q$ (with $\lambda(0)=+1$), and the associated twist display. Then $\lambda$ is completely multiplicative on $\mathbb{Q}$, takes values in $\{\pm 1\}$, equals $-1$ on every prime, and satisfies the elementary identities $\lambda(q)^2=1$, $\lambda(1)=1$, $\lambda(-1)=1$, and $\lambda(q^{-1})=\lambda(q)$.
background
Primitive Recognition Calculus works with rational displays of recognition cost. Native cost minimality (imported from PRCNativeCostMinimality) needs a discrete parity invariant that tracks how numerator and denominator factor, without leaving the rational setting.
The Liouville-type sign is exactly that invariant: for a reduced fraction, raise $-1$ to the total number of prime factors counted with multiplicity in numerator and denominator. Mathlib's totalized big-Omega sends $0$ to $0$, so the sign is $+1$ at zero; on every prime it is $-1$, and everywhere it lands in ${\pm 1}$. The twist display packages this sign for ledger bookkeeping.
The module sits in the Foundation/PRC stack: it does not redefine $J$-cost or the forcing chain, but supplies the arithmetic certificate that later structural-ledger arguments consume when they compare native cost presentations.
proof idea
Most of the file is definitional: liouvilleSign via totalized cardFactors on num/den of a reduced rational, and liouvilleTwistDisplay built from it. The supporting lemmas are short algebraic facts: multiplicativity under product and inverse, evaluation at $0,1,-1$ and at prime naturals, non-vanishing, and $\lambda(q)^2=1$. Cross-multiplication identities for numerator/denominator under rational products close the bookkeeping. No deep analytic number theory; pure finite arithmetic on $\mathbb{Q}$.
why it matters in Recognition Science
PRCNativeCostStructuralLedger imports this module, so every structural ledger identity that needs a multiplicative $\pm 1$ certificate on rational cost displays routes through these definitions. In the Recognition stack this is bookkeeping infrastructure for native cost minimality certificates inside Primitive Recognition Calculus, not a forcing-chain step (T5–T8) itself. It keeps the parity of prime content available as a first-class Lean object so later ledger comparisons stay inside the native rational presentation rather than floating into real analysis.
scope and limits
- Does not prove native cost minimality; only supplies the Liouville-sign certificate layer.
- Does not address J-uniqueness, phi-forcing, eight-tick structure, or D=3.
- Does not define physical constants, mass ladders, or alpha bounds.
- Does not treat irrational displays or real-analytic Liouville lambda on R>0.
- Does not by itself discharge structural ledger equalities; those live downstream.
used by (1)
depends on (1)
declarations in this module (60)
-
def
liouvilleSign -
def
liouvilleTwistDisplay -
theorem
liouvilleSign_mul_self -
theorem
liouvilleSign_ne_zero -
theorem
liouvilleSign_one -
theorem
liouvilleSign_neg_one -
theorem
rat_mul_num_den_cross -
theorem
liouvilleSign_mul -
theorem
liouvilleSign_inv -
theorem
liouvilleSign_natCast_prime -
theorem
liouvilleTwistDisplay_zero -
theorem
liouvilleTwistDisplay_one -
theorem
liouvilleTwistDisplay_neg_one -
theorem
liouvilleTwistDisplay_two -
theorem
liouvilleTwistDisplay_ne_zero -
theorem
liouvilleTwistDisplay_mul -
theorem
liouvilleTwistDisplay_inv -
theorem
liouvilleTwistDisplay_prime_pair -
def
liouvilleTwistNativeCost -
theorem
liouvilleTwistNativeCost_toRat -
structure
PRCNativeCostHypothesesSansTwoCalibration -
structure
PRCSlimSansTwoCalibrationHypotheses -
def
PRCSlimSansTwoCalibrationUniquenessTarget -
theorem
slim_iff_sansTwo_and_two_calibrated -
theorem
canonicalSelectedNativeCost_sans_two_hypotheses -
theorem
liouvilleTwistNativeCost_sans_two_hypotheses -
theorem
liouvilleTwistNativeCost_two_not_canonical -
theorem
PRCSlimSansTwoCalibrationUniquenessTarget_refuted -
structure
PRCSlimSansPairHypotheses -
def
PRCSlimSansPairUniquenessTarget -
theorem
slim_iff_sansPair_and_pair_calibrated -
theorem
canonicalSelectedNativeCost_sans_pair_hypotheses -
theorem
twoAdicTwistRat_zero -
theorem
twoAdicTwistRat_neg_one -
theorem
twoAdicGeneratedNativeCost_signed_unit -
theorem
twoAdicGeneratedNativeCost_zero_calibrated -
theorem
twoAdicGeneratedNativeCost_sans_pair_hypotheses -
theorem
PRCSlimSansPairUniquenessTarget_refuted -
structure
PRCSlimSansSignHypotheses -
def
PRCSlimSansSignUniquenessTarget -
theorem
slim_iff_sansSign_and_signed_unit -
theorem
canonicalSelectedNativeCost_sans_sign_hypotheses -
theorem
absValueGeneratedNativeCost_sans_sign_hypotheses -
theorem
PRCSlimSansSignUniquenessTarget_refuted -
theorem
slim_iff_sansZero_and_zero_calibrated -
theorem
canonicalSelectedNativeCost_sans_zero_hypotheses -
structure
PRCNativeCostHypothesesSansRcl -
structure
PRCSlimSansRclHypotheses -
def
PRCSlimSansRclUniquenessTarget -
theorem
slim_iff_sansRcl_and_rcl -
theorem
canonicalSelectedNativeCost_sans_rcl_hypotheses -
def
rclSpikeNativeCost -
theorem
rclSpikeNativeCost_toRat -
theorem
rclSpike_inv_iff -
theorem
rclSpikeNativeCost_sans_rcl_hypotheses -
theorem
rclSpikeNativeCost_five_not_canonical -
theorem
PRCSlimSansRclUniquenessTarget_refuted -
structure
SlimLedgerMinimalityCertificate -
theorem
slimLedgerMinimalityCertificate_holds -
theorem
slim_ledger_minimality_certificate_tagged