Gravity Black Hole Horizon States N Horizon Succ Patch

The doubling law

The declaration N_horizon_succ_patch states a simple counting rule for the quantum states on a black hole's horizon. In the framework's model, the horizon of area A carries A/4 patches, each of unit Planck area, and each patch holds two possible microstates. The total number of horizon microstates is therefore 2^(A/4). The theorem proves that adding four units of area to the horizon doubles the number of microstates: N_horizon(A + 4) = N_horizon(A) × 2. This is the discrete, exponential growth law for horizon states.

This doubling law is the combinatorial heart of the framework's derivation of black hole entropy. The leading entropy S_lead = A/4 equals the base-2 logarithm of the microstate count, so the famous one-quarter-area entropy formula emerges from counting states rather than being assumed. The framework's library proves this bridge theorem, along with the positivity of the state count for any positive area. The doubling law itself is a purely formal statement about the exponential function; it does not by itself assert anything about physics.

In Recognition Science, the horizon is modeled as a discrete ledger: a record of recognition events, each patch a two-state qubit. The framework proves the microstate count is positive, that the leading entropy is the log of that count, and that the leading-log quantum correction coefficient c_RS lies in the band (-0.25, 0), strictly excluding the loop-quantum-gravity value -0.5 and the string-theory value -1.5. The doubling law is one clause in the master certificate for these horizon states.

The theorem does not claim that real black holes have exactly this many states, nor that the area is quantized in units of four Planck areas. It establishes a relation within a specific discrete model. The physical bridge from recognition events to actual spacetime geometry remains open. The value of the theorem is internal: it shows the exponential counting law is consistent and self-contained, and it provides the combinatorial scaffolding for the entropy derivation.

/-- The horizon microstate count is exponential in patch count. -/
theorem N_horizon_succ_patch (A : ℝ) :
    N_horizon (A + 4) = N_horizon A * 2 := by
  unfold N_horizon horizon_patch_count
  have h_eq : (A + 4) / 4 = A / 4 + 1 := by ring
  rw [h_eq]
  rw [Real.rpow_add (by norm_num : (0 : ℝ) < 2)]
  rw [Real.rpow_one]

/-- Each Q₃-orbit patch carries 2 microstates (SU(2) projection
gives 2-orbit). Total horizon microstate count is `2^(A/4)`. -/
def N_horizon (A : ℝ) : ℝ := (2 : ℝ) ^ horizon_patch_count A

/-- **THEOREM.** The leading entropy `S_lead = A/4` equals the
log-base-2 of the horizon microstate count: `S_lead = log_2 N_horizon`,
in the Boltzmann normalization. -/
theorem S_lead_eq_log2_N_horizon {A : ℝ} (h : 0 < A) :
    S_lead A * Real.log 2 = Real.log (N_horizon A) := by
  unfold S_lead N_horizon horizon_patch_count
  rw [Real.log_rpow (by norm_num : (0 : ℝ) < 2)]

/-- **NUMERICAL BAND.** `c_RS ∈ (−0.25, 0)`, with the upper end being
the LQG value `−0.5/2 = −0.25` strictly excluded by `log φ < 0.5`. -/
theorem c_RS_band : -0.25 < c_RS ∧ c_RS < 0 := by
  refine ⟨?_, c_RS_neg⟩
  unfold c_RS
  have h_lt := log_phi_lt_half
  linarith

What this page does not claim

The theorem does not assert that real black hole horizons have exactly 2^(A/4) microstates. The theorem does not claim the horizon area is quantized in units of four Planck areas. The physical bridge from recognition events to spacetime geometry is not established by this declaration.

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/BlackHoleHorizonStates.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: