Encyclopedia Gravity Gravity Ultramassive Bh Entropy Quadruples On Double

ARTICLE 4 claims 3 theorems 1 model

Gravity Ultramassive Bh Entropy Quadruples On Double

For ultramassive black holes, the framework proves a simple rule: double the mass, and the entropy quadruples.

The entropy scaling law

In the Recognition Science framework, a black hole's entropy is defined as a constant times the number of horizon cells, where each cell is a patch of the event horizon with area set by the fundamental length ℓ₀. The framework's library of machine-checked formal theorems proves that if you take any two black holes whose masses are in a 2:1 ratio, the heavier one has exactly four times the entropy of the lighter one. This is the statement of the declaration entropy_quadruples_on_double: a proved theorem, not a numerical fit.

The proof is a short algebraic consequence of the definitions. The horizon area scales with the square of the Schwarzschild radius, which in turn scales linearly with mass. Doubling the mass quadruples the area, and since entropy is proportional to area, it quadruples as well. The theorem holds for all positive masses, so it applies to ultramassive black holes like TON 618, whose mass is about 66 billion solar masses, as well as to stellar-mass holes.

This scaling law is one of several results the framework derives for black holes. The same library proves that the Hawking temperature halves when mass doubles, and that the temperature decreases monotonically with mass. The entropy law is noteworthy because it is a clean, testable relation that follows from the framework's core assumptions, but it does not by itself confirm those assumptions against observation.

What the theorem does not claim: it does not say that real black holes obey this law, because that would require matching the framework's definitions to measured entropy, which remains open. It does not claim that entropy is finite in all cases, though the framework does prove that the cost function is finite on positive reals. And it does not claim that the entropy law is unique to Recognition Science; the same area scaling appears in conventional black hole thermodynamics.

MODEL rs_entropy · IndisputableMonolith/Gravity/UltramassiveBH.lean
/-- RS Bekenstein-Hawking entropy: S = k_R · A/(4ℓ₀²).
    Each Planck-area cell supports one recognition event costing k_R = ln φ. -/
noncomputable def rs_entropy (bh : RSBH) : ℝ :=
  k_R * horizonCells bh
THEOREM entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean
entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean:152
/-- Entropy scales as M². Doubling mass quadruples entropy. -/
theorem entropy_quadruples_on_double (bh₁ bh₂ : RSBH)
    (h : bh₂.mass = 2 * bh₁.mass) :
    rs_entropy bh₂ = 4 * rs_entropy bh₁ := by
  unfold rs_entropy horizonCells horizonArea schwarzschildRadius
  rw [h]
  ring
THEOREM temp_halves_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean
/-- Doubling mass halves the temperature. -/
theorem temp_halves_on_double (bh₁ bh₂ : RSBH)
    (h : bh₂.mass = 2 * bh₁.mass) :
    rs_hawkingTemp bh₂ = rs_hawkingTemp bh₁ / 2 := by
  unfold rs_hawkingTemp
  rw [h]
  have hM : bh₁.mass > 0 := bh₁.mass_pos
  have hpi : Real.pi > 0 := Real.pi_pos
  have hdenom : 8 * Real.pi * bh₁.mass ≠ 0 := by positivity
  field_simp [hdenom]
THEOREM entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean
entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean:152
/-- Entropy scales as M². Doubling mass quadruples entropy. -/
theorem entropy_quadruples_on_double (bh₁ bh₂ : RSBH)
    (h : bh₂.mass = 2 * bh₁.mass) :
    rs_entropy bh₂ = 4 * rs_entropy bh₁ := by
  unfold rs_entropy horizonCells horizonArea schwarzschildRadius
  rw [h]
  ring

What this page does not claim

Does not claim that real black holes obey this entropy law, since the bridge to measured entropy is open. Does not claim that the entropy law is unique to Recognition Science. Does not claim that the theorem covers cases where mass is zero or negative.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/UltramassiveBH.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND