module module moderate

`IndisputableMonolith.Gravity.UltramassiveBH`

The module defines a black hole in Recognition Science using native units where fundamental length, time, and light speed equal one. It supplies the RS black hole object along with horizon radius, area, entropy, and temperature expressions built on the J-cost. Gravity researchers modeling discrete spacetime or thermodynamic limits would reference these. The module contains only definitions imported from the constants and J-cost core.

claimIn units with $\ell_0 = \tau_0 = c = 1$, defines the RS black hole together with Schwarzschild radius $r_s$, horizon area $A$, cell count, entropy $S$, and Hawking temperature $T$ via the J-cost function.

background

The module sits inside the Gravity domain of Recognition Science and imports the time quantum $\tau_0 = 1$ tick from Constants together with the J-cost core. It works entirely in RS-native units where length, time, and $c$ are set to unity, allowing direct application of the J-cost to horizon quantities. The setting extends the Recognition Composition Law to black-hole thermodynamics without invoking the full forcing chain.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the black-hole primitives required by any downstream gravity theorems that link J-cost to horizon entropy or temperature. It fills the concrete object needed to apply the phi-ladder and eight-tick octave to ultramassive objects, though no used-by edges are recorded yet.

scope and limits

Does not derive any black-hole property from the T0-T8 forcing chain.
Does not evaluate the mass formula or phi-ladder rung for specific objects.
Does not address the alpha band or Berry creation threshold.
Does not contain theorems or numerical computations.

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