module module

`IndisputableMonolith.Physics.NoHairTheorem`

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

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (17)

structure BHCharges L29
def BHState L35
def hair_cost L41
theorem hair_cost_nonneg L45
theorem hair_cost_zero_iff L53
theorem no_hair_field_decay L77
theorem bh_state_determined_by_charges L91
theorem bh_state_eq_of_charges_eq L108
def bekenstein_hawking_entropy L124
theorem entropy_nonneg L127
theorem entropy_linear_in_area L131
def schwarzschild_entropy L138
theorem schwarzschild_entropy_eq L141
theorem schwarzschild_entropy_monotone L147
def hawking_temperature L160
theorem hawking_temp_positive L163
theorem hawking_temp_decreases L169