IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger · Recognition explainer

used by (1)

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

IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostMinimalityCertificate module_import

declarations in this module (104)

theorem crossDisp L69
theorem dispCross L73
def jq L77
theorem jq_onRatioOrbit L79
theorem costFromCharacter_jq L82
theorem jq_one L85
theorem jq_zero L87
theorem jq_closed L89
theorem jq_nonneg L94
theorem jq_lt_zero L98
theorem jq_eq_zero L105
theorem jq_neg L116
theorem jq_inv L121
theorem jq_mono L128
theorem jq_strictMono L143
theorem jq_le_reflect L160
theorem jq_rcl L168
theorem jq_two L176
theorem jq_eq_two_cases L179
def natOrbit L199
theorem natOrbit_toRat L201
def IsPosIntOrbit L205
theorem natOrbit_isPosInt L207
theorem two_isPosInt L210
theorem primeDirection_isPosInt L212
def PRCNativeCostSignReversing L228
def PRCNativeCostMonotone L234
def PRCNativeCostPositive L240
theorem canonicalSelectedNativeCost_jq L245
theorem canonicalSelectedNativeCost_signReversing L249
theorem canonicalSelectedNativeCost_monotone L259
theorem canonicalSelectedNativeCost_positive L267
theorem signReversing_forces_signed_unit L277
structure PRCSignReversingNativeCostHypotheses L291
def PRCSignReversingNativeCostUniquenessTarget L297
theorem PRCSignReversingNativeCostUniquenessTarget_proved L303
theorem canonicalSelectedNativeCost_signReversing_hypotheses L316
theorem signReversing_class_forces_slim L326
theorem absValueGeneratedNativeCost_not_signReversing L339
lemma exists_pow_gt_rat L363
lemma cut_pins_aux L378
theorem cut_pins L414
structure MonoMult L428
theorem pow L436
theorem pos L445
theorem ge_one L461
theorem transfer_le L502
theorem transfer_ge L511
theorem trivial_of_two_eq_one L522
theorem monoMult_gauge L548
theorem natCast_monoMult L569
theorem monotone_multiplicative_pins L580
structure PRCStructuralNativeCostHypotheses L594
def PRCStructuralNativeCostUniquenessTarget L601
theorem structural_character_calibrated_on_positive_integers L609
theorem PRCStructuralNativeCostUniquenessTarget_proved L688
theorem canonicalSelectedNativeCost_structural_hypotheses L744
theorem structural_forces_slim L755
theorem structural_forces_positive L770
structure PRCStructuralNativeCostHypothesesSansAnchor L786
def PRCStructuralSansAnchorUniquenessTarget L793
theorem structural_iff_sansAnchor_and_two_calibrated L800
def powerGeneratedNativeCost L833
theorem powerGeneratedNativeCost_toRat L837
theorem powerGeneratedNativeCost_base L845
theorem powerGeneratedNativeCost_monotone L865
theorem powerGeneratedNativeCost_zero_calibrated L873
theorem powerGeneratedNativeCost_signReversing L884
def oddPowerGeneratedNativeCost L892
theorem oddPowerGeneratedNativeCost_toRat L895
theorem oddPowerGeneratedNativeCost_sansAnchor L899
theorem oddPowerGeneratedNativeCost_anchor_injective L911
def cubeGeneratedNativeCost L927
theorem cubeGeneratedNativeCost_toRat L930
theorem cubeGeneratedNativeCost_sansAnchor L934
theorem oddPowerGeneratedNativeCost_zero L940
theorem cubeGeneratedNativeCost_two_not_canonical L945
def GaugeOrbitIsOddPowerFamily L1065
theorem gauge_orbit_contains_every_odd_power L1072
theorem PRCStructuralSansAnchorUniquenessTarget_refuted L1083

… and 24 more