module module

`IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimality module_import

declarations in this module (60)

def liouvilleSign L99
def liouvilleTwistDisplay L103
theorem liouvilleSign_mul_self L106
theorem liouvilleSign_ne_zero L111
theorem liouvilleSign_one L115
theorem liouvilleSign_neg_one L119
theorem rat_mul_num_den_cross L126
theorem liouvilleSign_mul L145
theorem liouvilleSign_inv L177
theorem liouvilleSign_natCast_prime L187
theorem liouvilleTwistDisplay_zero L196
theorem liouvilleTwistDisplay_one L199
theorem liouvilleTwistDisplay_neg_one L202
theorem liouvilleTwistDisplay_two L205
theorem liouvilleTwistDisplay_ne_zero L212
theorem liouvilleTwistDisplay_mul L216
theorem liouvilleTwistDisplay_inv L223
theorem liouvilleTwistDisplay_prime_pair L238
def liouvilleTwistNativeCost L252
theorem liouvilleTwistNativeCost_toRat L256
structure PRCNativeCostHypothesesSansTwoCalibration L269
structure PRCSlimSansTwoCalibrationHypotheses L289
def PRCSlimSansTwoCalibrationUniquenessTarget L298
theorem slim_iff_sansTwo_and_two_calibrated L307
theorem canonicalSelectedNativeCost_sans_two_hypotheses L327
theorem liouvilleTwistNativeCost_sans_two_hypotheses L334
theorem liouvilleTwistNativeCost_two_not_canonical L386
theorem PRCSlimSansTwoCalibrationUniquenessTarget_refuted L394
structure PRCSlimSansPairHypotheses L404
def PRCSlimSansPairUniquenessTarget L412
theorem slim_iff_sansPair_and_pair_calibrated L419
theorem canonicalSelectedNativeCost_sans_pair_hypotheses L432
theorem twoAdicTwistRat_zero L439
theorem twoAdicTwistRat_neg_one L445
theorem twoAdicGeneratedNativeCost_signed_unit L454
theorem twoAdicGeneratedNativeCost_zero_calibrated L464
theorem twoAdicGeneratedNativeCost_sans_pair_hypotheses L478
theorem PRCSlimSansPairUniquenessTarget_refuted L487
structure PRCSlimSansSignHypotheses L499
def PRCSlimSansSignUniquenessTarget L506
theorem slim_iff_sansSign_and_signed_unit L513
theorem canonicalSelectedNativeCost_sans_sign_hypotheses L525
theorem absValueGeneratedNativeCost_sans_sign_hypotheses L532
theorem PRCSlimSansSignUniquenessTarget_refuted L540
theorem slim_iff_sansZero_and_zero_calibrated L554
theorem canonicalSelectedNativeCost_sans_zero_hypotheses L562
structure PRCNativeCostHypothesesSansRcl L581
structure PRCSlimSansRclHypotheses L593
def PRCSlimSansRclUniquenessTarget L602
theorem slim_iff_sansRcl_and_rcl L609
theorem canonicalSelectedNativeCost_sans_rcl_hypotheses L640
def rclSpikeNativeCost L647
theorem rclSpikeNativeCost_toRat L651
theorem rclSpike_inv_iff L661
theorem rclSpikeNativeCost_sans_rcl_hypotheses L676
theorem rclSpikeNativeCost_five_not_canonical L754
theorem PRCSlimSansRclUniquenessTarget_refuted L764
structure SlimLedgerMinimalityCertificate L778
theorem slimLedgerMinimalityCertificate_holds L790
theorem slim_ledger_minimality_certificate_tagged L809