module module high

`IndisputableMonolith.Gravity.UltramassiveBH`

The module defines black hole quantities such as Schwarzschild radius and horizon area for an ultramassive black hole in RS-native units with ℓ₀ = τ₀ = c = 1. Gravity researchers cite these when computing entropy or temperature from the J-cost framework. The module consists entirely of definitions and elementary lemmas with no complex proofs.

claimIn RS-native units where the fundamental length ℓ₀, time τ₀ and speed of light c are all set to 1, a black hole is characterized by its Schwarzschild radius $r_s$, horizon area $A$, and related J-cost quantities.

background

Recognition Science derives all physics from the J functional equation and the Recognition Composition Law. The module imports the definition τ₀ = 1 tick from Constants and the core J-cost machinery from JcostCore. It introduces black-hole-specific objects (RSBH, schwarzschildRadius, horizonArea, horizonCells, rs_entropy, rs_hawkingTemp) expressed directly in these units.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions supply the RS-native foundation for black-hole thermodynamics and feed the sibling lemmas rs_entropy and rs_hawkingTemp. They connect the J-cost lower-bound results to gravitational horizons within the Gravity domain.

scope and limits

Does not derive the mass formula from the phi-ladder.
Does not address rotating or charged black holes.
Does not compute numerical values for specific masses.
Does not include quantum corrections to the horizon.

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