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 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 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:
- How does the framework's entropy definition connect to the Bekenstein-Hawking formula in general relativity?
- What empirical evidence could confirm or falsify the entropy scaling law for real black holes?
- Does the framework's no-singularity theorem hold for all masses, and what does it imply for the interior structure?
- How does the framework derive the fundamental length ℓ₀ from its constants?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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 bhIn 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 ℓ₀. rs_entropy · IndisputableMonolith/Gravity/UltramassiveBH.leanTHEOREM entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean
/-- 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] ringThe 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. entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.leanTHEOREM 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]The same library proves that the Hawking temperature halves when mass doubles. temp_halves_on_double · IndisputableMonolith/Gravity/UltramassiveBH.leanTHEOREM entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean
/-- 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] ringThe 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. entropy_quadruples_on_double · IndisputableMonolith/Gravity/UltramassiveBH.lean