IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimality

declarations in this module (19)

• theorem PRCSignedStrengthenedNativeCostUniquenessTarget_refuted L73
• theorem PRCSignedStrengthenedNativeCostSignedAdmissibleCharacterFactorizationTarget_refuted L87
• lemma pair_two_case_split L99
• theorem character_pair_two_calibration_forces_prime_calibration L151
• structure PRCZeroCalibratedSignedStrengthenedNativeCostHypotheses L293
• def PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget L300
• lemma recovers L308
• theorem PRCZeroCalibratedSignedStrengthenedNativeCostUniquenessTarget_proved L310
• theorem all_prime_axis_field_redundant L343
• theorem slim_class_iff_full_class L352
• theorem canonicalSelectedNativeCost_slim_hypotheses L370
• theorem constantZeroNativeCost_slim_excluded L378
• theorem linearNativeCost_slim_excluded L387
• theorem zeroFlatNativeCost_slim_excluded L396
• structure CostSelectionPackageNativeSlim L426
• theorem costSelectionPackageNativeSlim_holds L444
• theorem cost_selection_native_slim_holds L459
• def nativeCostSelectionSlimPremiseLedger L470
• theorem nativeCostSelectionSlimPremiseLedger_all_deltaOnly L495