Holography Coefficient Bridge Bekenstein Branch

The Bekenstein branch

The Bekenstein-Hawking entropy formula says a black hole's entropy equals one quarter of its horizon area in Planck units. The factor 1/4 has resisted a simple derivation for decades. In the Recognition Science framework, a machine-checked library of formal theorems now isolates that factor as the result of a single counting operation on a small finite set of configurations.

The framework models a patch of horizon as a ledger, a discrete record of recognition events, where each event is a forced cost of maintaining the record consistent. The relevant map takes each of 16 possible face configurations and decides whether it is closed, meaning internally consistent. Counting the image of this map gives 2 configurations, its kernel gives 8, and the whole domain gives 16. The theorem bekenstein_branch proves, from these actual counts and nothing hand-typed, that the ratio of the rank (1) to the number of admissible sectors (4) equals 1/4. The same structure also proves the alternative branch: if entropy attached to the kernel instead, the ratio would be 3/4, giving a coefficient of 4/3. Both branches are proven; the framework does not choose between them.

The choice is the single remaining physical input, declared as an open selector. The framework proves that if one closed plaquette realizes exactly one recognition event, the Bekenstein 1/4 follows downstream. That identification, one closed plaquette corresponding to one event, is not proven. It is an unformalized physical assertion, the crux that the entire coefficient question now reduces to. Supplying it derives Bekenstein-Hawking; refuting it gives the 4/3 branch. The reduction always lands; the value is a crisp yes/no rather than a lattice-model war.

What the declaration does not claim is as important as what it proves. It does not prove that entropy actually attaches to the closure rank. It does not derive the Bekenstein-Hawking formula from first principles. It proves the arithmetic of the coefficient once the physical selector is named, and it isolates that selector as the one open question. A reader can now see the exact point where a full derivation would succeed or fail, which is more precise than any earlier statement of the problem.

/-- **Bekenstein branch.** Entropy attaches to the closure rank (`m = 1`) ⇒ ratio `1/4`. -/
theorem bekenstein_branch :
    (closureRank : ℚ) / (admissibleSectors.card : ℚ) = 1 / 4 := by
  rw [closureRank_eq_one, recognition_sector_count]; norm_num

/-- **`κ = 4/3` branch.** Entropy attaches to the free-bit nullity (`m = 3`) ⇒ ratio `3/4`
(the coefficient is then `4/3` of Bekenstein). -/
theorem kappa_four_thirds_branch :
    (freeBits : ℚ) / (admissibleSectors.card : ℚ) = 3 / 4 := by
  rw [freeBits_eq_three, recognition_sector_count]; norm_num

/-- **Bekenstein, downstream of the selector.** Given the open selector (multiplicity =
closure rank), the pixel-to-sector ratio is the Bekenstein `1/4`. Everything below the
selector is discharged; the selector itself is the sole remaining physical input. -/
theorem bekenstein_of_selector (m : ℕ)
    (h : selector_multiplicity_is_closure_rank m) :
    (m : ℚ) / (admissibleSectors.card : ℚ) = 1 / 4 := by
  unfold selector_multiplicity_is_closure_rank at h
  rw [h, closureRank_eq_one, recognition_sector_count]; norm_num

What this page does not claim

The declaration does not prove that entropy attaches to the closure rank. The declaration does not derive the full Bekenstein-Hawking formula from first principles. The declaration does not claim the physical identification of one closed plaquette with one recognition event.

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/Holography/CoefficientBridge.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: