Holography Coefficient Bridge

The coefficient bridge

The Bekenstein-Hawking formula gives black holes an entropy proportional to their surface area, with the constant 1/4. In Recognition Science, that 1/4 is not a free parameter: it is a ratio that a ledger, a discrete record of recognition events, must produce from its own internal structure. The holography coefficient bridge is the module that pins that ratio down to exactly two possible values, and isolates the single physical choice between them.

The framework models a surface as a collection of 16 possible plaquette configurations. A closure constraint selects which configurations are physically allowed. The module computes three numbers directly from this constraint map: the rank (1), the nullity (3), and the total degrees of freedom (4). These satisfy the rank-nullity theorem: 1 + 3 = 4, verified by brute-force computation on the actual configurations, not by hand-written subtraction. The ratio of either rank or nullity to the number of admissible sectors (4) gives exactly 1/4 or 3/4.

The remaining question is which ratio nature chooses. If one closed plaquette realizes exactly one recognition event, the ratio is 1/4 and the Bekenstein-Hawking coefficient follows. If it realizes three events, the coefficient becomes 4/3. The module proves both branches rigorously; it does not decide between them. That decision is the open crux, reduced to a single integer: the multiplicity of recognition events per plaquette.

The practical payoff is a sharpened research target. Instead of a lattice-model war over the coefficient, the framework now faces one crisp question: does entropy attach to the closure event itself, or to the free microstates? Answering that question, with either value, completes the bridge and derives the black hole entropy formula from the ledger structure.

theorem closureRank_eq_one : closureRank = 1 := by decide

theorem freeBits_eq_three : freeBits = 3 := by decide

theorem rawBits_eq_four : rawBits = 4 := 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

/-- **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 module does not prove that the Bekenstein-Hawking coefficient is 1/4; it proves both 1/4 and 3/4 are possible. The module does not derive the physical selector that chooses between the two branches. The module does not claim the rank-nullity result applies to any ledger other than the specific D=3 plaquette configuration.

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: