module module

`IndisputableMonolith.Gravity.UltramassiveBH`

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 (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost.JcostCore module_import

declarations in this module (26)

structure RSBH L44
def schwarzschildRadius L49
def horizonArea L53
def k_R L58
lemma k_R_pos L60
def horizonCells L63
def rs_entropy L68
def rs_hawkingTemp L74
theorem Jcost_finite_on_pos L81
theorem Jcost_zero_iff_one L88
theorem Jcost_lower_bound L108
theorem nothing_costs_arbitrarily_large L117
theorem rs_entropy_eq L138
theorem rs_entropy_pos L142
theorem entropy_quadruples_on_double L153
theorem rs_hawkingTemp_pos L163
theorem temp_decreases_with_mass L171
theorem temp_halves_on_double L180
theorem hamiltonian_approximation_bound L202
theorem small_strain_hamiltonian_valid L208
def phiRung L217
theorem phi_ladder_recovery L221
theorem cosmic_censorship_automatic L236
theorem bh_interior_finite_cost L242
structure UltramassiveBHCert L254
def ultramassiveBHCert L264