module module

`IndisputableMonolith.Cost.GaugeOrbitClassification`

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.

scripts.cost_unit_axiom_audit module_import

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.GaugeOrbitFromRealCharacter module_import
IndisputableMonolith.Cost.MonotoneMultiplicativePower module_import

declarations in this module (17)

theorem le_of_trace_le L62
theorem cost_display L83
theorem cost_at_zero L93
theorem cost_at_neg L99
theorem degenerate_is_signGauge L109
theorem natChar_monotoneMultiplicative L138
theorem exists_nat_exponent L156
theorem char_at_pos L186
theorem cost_at_pos L211
theorem nontrivial_is_signedPower L225
theorem vanishes_at_two_iff_trace_two L273
theorem vanishes_at_two_iff_flat L289
theorem charges_positively_at_two L303
theorem strict_somewhere_iff_charges_at_two L320
theorem charges_at_two_iff_not_signGauge L339
theorem signGauge_sees_orientation_only L355
theorem GaugeOrbitIsSignedPowerFamily_of_sixExponentials L373