Holography Coefficient Bridge Closure Image Times Kernel

The closure map and its arithmetic

The declaration closure_image_times_kernel is a theorem about a specific finite map in the Recognition Science framework. The map, called closed, takes each of 16 possible face configurations and returns either true or false, indicating whether that configuration satisfies a closure constraint, a discrete record of which local arrangements are allowed. The theorem states a simple arithmetic fact about this map: the number of distinct outputs it can produce, multiplied by the number of configurations that map to the false value, equals the total number of configurations. In symbols, the image size times the kernel size equals the domain size, or 2 times 8 equals 16.

This is the rank-nullity theorem applied to a concrete, finite case. The rank, computed as the base-2 logarithm of the image size, is 1. The nullity, the base-2 logarithm of the kernel size, is 3. The total number of degrees of freedom, the base-2 logarithm of the domain size, is 4. The theorem verifies that 4 equals 1 plus 3, with each number computed independently from the actual configuration sets, not by hand-subtracting one from another. This arithmetic is the genuine content that pins the rank to 1 without any assumed subtraction.

In Recognition Science, this rank-nullity fact is the bridge that reduces a holographic entropy coefficient to a single binary choice. The coefficient in question is the factor relating pixel area to entropy, the "4" in the Bekenstein-Hawking formula S = A/4. The theorem proves both candidate ratios: the rank divided by the number of admissible sectors equals 1/4, and the nullity divided by the same equals 3/4. Both branches are proven; nothing is baked in. The coefficient is not a number to compute, but a physical selector to be named: does entropy attach to the closure rank (giving 1/4) or to the free-bit nullity (giving 3/4)?

What the theorem does not claim is the selector itself. The identification that one closed plaquette realizes exactly one recognition event, meaning its multiplicity equals the closure rank, is not proven. This is the single remaining physical input, the crux to which the whole gap reduces. Supplying this selector derives the Bekenstein-Hawking coefficient; refuting it, choosing multiplicity 3, gives the alternative 4/3. The reduction always lands; the coefficient's value is now a single crisp yes or no, not a lattice-model war.

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

theorem closureRank_eq_one : closureRank = 1 := by decide

theorem freeBits_eq_three : freeBits = 3 := 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 the entropy coefficient is 1/4 rather than 3/4. The theorem does not establish that one closed plaquette corresponds to exactly one recognition event. The theorem does not derive the Bekenstein-Hawking formula without the open selector.

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: