Holography Coefficient Bridge Closure Rank Eq One

The closure rank

The Bekenstein-Hawking entropy formula for a black hole, S = A/4, carries a factor of 1/4 that has puzzled physicists for decades. In the Recognition Science framework, this factor is not a free parameter but the output of a counting problem: how many independent constraints does a small patch of holographic surface impose on its internal degrees of freedom? The declaration closureRank_eq_one answers that counting question for one specific map.

The map in question, called the ledger-closure map, takes each possible configuration of a surface plaquette and decides whether it is closed, meaning it satisfies the framework's local consistency rule. The theorem states that this map has rank 1: among all 16 possible configurations, the closure condition can only distinguish two outcomes, closed or not closed. This is computed as the base-2 logarithm of the image size, log2(2) = 1, rather than by subtracting one number from another, which the framework's developers explicitly avoid as a potential failure mode.

The rank of 1 is one half of a rank-nullity decomposition. The kernel of the map, the set of closed configurations, has size 8, giving a nullity of 3. Together with the rank, these sum to the total of 4 bits of raw configuration space, and the product of image and kernel sizes equals the domain size, 2 × 8 = 16, both verified by direct computation. This decomposition is what pins the entropy coefficient to exactly two possible values: if entropy attaches to the closure event itself, the ratio is 1/4, reproducing Bekenstein; if it attaches to the free internal states, the ratio is 3/4, giving a coefficient of 4/3.

In Recognition Science, the declaration closureRank_eq_one is a proved theorem in the machine-checked library of formal theorems, established by exhaustive case analysis. It does not, however, decide which of the two branches is physically correct. That choice rests on an open question, the selector: whether one closed plaquette realizes exactly one recognition event or three. The theorem reduces the entire coefficient problem to this single yes/no physical input, and everything downstream of that choice is already proved.

theorem closureRank_eq_one : closureRank = 1 := by decide

theorem freeBits_eq_three : freeBits = 3 := by decide

/-- **Rank-nullity (additive form).** `rawBits = closureRank + freeBits` (`4 = 1 + 3`),
with each side computed independently from the actual sets. -/
theorem rank_nullity_add : rawBits = closureRank + freeBits := by decide

/-- **Rank-nullity (first-isomorphism form) of the ACTUAL map.**
`|image closed| · |kernel closed| = |domain|` (`2 · 8 = 16`). This is the genuine content
that pins the rank to 1 without any hand-typed subtraction. -/
theorem closure_image_times_kernel :
    (Finset.univ.image (fun c : FaceCfg => closed c)).card * closedConfigs.card
      = (Finset.univ : Finset FaceCfg).card := by decide

/-- **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

What this page does not claim

The theorem does not prove that entropy attaches to the closure rank rather than the free-bit nullity. The theorem does not derive the Bekenstein-Hawking formula from first principles; it only pins the coefficient to two rational values. The theorem does not claim that the rank-nullity decomposition is unique or that the closure map is the only physically relevant one.

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: