module module

`IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter`

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.Cost.GaugeOrbitClassification module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.RealCharacterFactorization module_import
IndisputableMonolith.Foundation.PrimitiveRecognitionCalculus.PRCNativeCostStructuralLedger module_import

declarations in this module (41)

theorem realCharacterFactorizationHypotheses_of_structural L30
theorem structural_sansAnchor_realCharacterFactorization L47
def signGaugeCostDisplay L64
def signGaugeNativeCost L68
theorem signGaugeNativeCost_toRat L73
theorem signGaugeNativeCost_base_sans_two L84
theorem signGaugeNativeCost_signReversing L128
theorem signGaugeNativeCost_monotone L140
theorem signGaugeNativeCost_zero_calibrated L152
theorem signGaugeNativeCost_sansAnchor L163
theorem signGaugeNativeCost_rationalTrace_two L171
theorem signGaugeNativeCost_realCharacterCandidate L182
theorem signGaugeNativeCost_characterExponent_zero L191
theorem signGaugeNativeCost_character_not_oddPower L208
theorem signGaugeNativeCost_not_oddPowerGeneratedNativeCost L224
theorem GaugeOrbitIsOddPowerFamily_refuted L243
def GaugeOrbitIsSignOrOddPowerFamily L251
def signedPow L283
theorem signedPow_zero_arg L285
theorem signedPow_one_arg L288
theorem signedPow_mul L291
theorem signedPow_inv L296
theorem signedPow_div L300
theorem signedPow_neg L304
theorem signedPow_ne_zero L309
theorem signedPow_of_one_le L312
theorem signedPow_mono L318
theorem signedPow_even L330
def signedPowerNativeCost L337
theorem signedPowerNativeCost_toRat L341
theorem signedPowerNativeCost_base L349
theorem signedPowerNativeCost_signReversing L369
theorem signedPowerNativeCost_monotone L375
theorem signedPowerNativeCost_zero_calibrated L384
theorem signedPowerNativeCost_sansAnchor L396
theorem signedPowerNativeCost_even_eq_oddPower L404
theorem signedPowerNativeCost_one_two_toRat L410
theorem signedPowerNativeCost_one_not_oddPower L415
theorem signedPowerNativeCost_one_not_signGauge L435
theorem GaugeOrbitIsSignOrOddPowerFamily_refuted L446
def GaugeOrbitIsSignedPowerFamily L461