module module high

`IndisputableMonolith.Gravity.UltramassiveBH`

The UltramassiveBH module supplies type definitions and basic properties for black holes expressed in Recognition Science native units with ℓ₀ = τ₀ = c = 1. Gravity modelers working inside the RS framework would cite these objects when computing horizon quantities from J-cost. The module is purely definitional with no proof obligations or tactic steps.

claimAn RS black hole RSBH(M) of mass parameter M together with the associated Schwarzschild radius $r_s = 2M$, horizon area, cell count, and entropy expressed via the J-cost function in units where $c=1$, $τ_0=1$.

background

The module imports Constants, which fixes the RS time quantum τ₀ = 1 tick, and JcostCore, which supplies the J-cost function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). These imports set the native-unit convention ℓ₀ = τ₀ = c = 1 used throughout the black-hole definitions. Sibling declarations inside the module introduce RSBH, schwarzschildRadius, horizonArea, k_R, horizonCells, rs_entropy, and rs_hawkingTemp, all built directly on the J-cost primitives.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the black-hole primitives required for any RS-native treatment of gravity and entropy. It sits downstream of the J-cost core and the forcing chain (T5–T8) that fixes the phi-ladder and D = 3. No downstream theorems are recorded yet, so the definitions remain available for future gravity or cosmology results.

scope and limits

Does not derive the mass ladder from the phi fixed point.
Does not treat rotating or charged black holes.
Does not compute numerical values for specific masses.
Does not address dynamical evolution or mergers.

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