Holography Keystone Factor Three Microstate Reading Violates

The factor-three keystone

The Bekenstein bound is a physical limit stating that the total entropy of a system cannot exceed a constant times its energy and size. For a black hole horizon, the famous Bekenstein-Hawking formula says the entropy equals one quarter of the horizon's area. A long-standing question is what that quarter actually counts: the number of microstates, the quantum states of the horizon's constituents, or something else. The Recognition Science framework models this as a choice between two readings of the same geometric data, and a machine-checked library of formal theorems has now established a sharp consequence of that choice.

Within the framework, the ledger, a discrete record of events, assigns a cost to each reading. The record reading, which counts the horizon's information as a set of recorded bits, assigns a cost of one unit per pixel. The microstate reading, which counts the underlying quantum states, assigns a cost of exactly three units per pixel. This factor of three is not an approximation; it is proved by computation from the ledger floor. The theorem microstate_reading_violates then shows that if the horizon area saturates the Bekenstein bound, meaning A/4 equals 2πER, then the microstate reading's entropy of 3·(A/4) strictly exceeds that bound. The record reading, by contrast, satisfies the bound with equality.

This exclusion is scale-free. The violation is exactly the constant factor 3 at every horizon radius, with no dependence on volume, bulk geometry, or a large-radius limit. The result also survives a change of entropy units from bits to nats, since the violation is a strict ratio statement. The framework's library proves this in violation_is_scale_free and violation_survives_unit_conversion.

The keystone is conditional. It does not prove that the Bekenstein bound holds for total horizon entropy; that is an open hypothesis, stated as a typed premise. It does not prove that the horizon saturates the bound; that is a model input from Schwarzschild geometry. It does not prove per-pixel additivity; that is a model premise. What the theorem establishes is the exclusion structure: given those two named hypotheses and additivity, the microstate reading is inconsistent with the bound, and the record reading is the only one that survives. This is a conditional discharge, not an unconditional derivation of the 1/4 factor.

The practical consequence is that the framework's holographic program no longer treats the 1/4 as a bare identification. Inside the program, the microstate reading is not merely disfavored; it is ruled out by contradiction. The remaining work is to prove the open legs, especially the total-entropy Bekenstein bound, which would turn the conditional exclusion into a full derivation.

/-- **Microstate reading violates the saturated bound — at every radius.** Given the same
saturation and a nondegenerate horizon (`0 < A`), the microstate-reading entropy `3·(A/4)`
strictly exceeds the bound. The violation is the fixed factor 3: no volume scaling, no
bulk-to-boundary map, no asymptotics. -/
theorem microstate_reading_violates (A E R : ℝ) (hA : 0 < A)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    ¬ TotalEntropyBekensteinBound (3 * (A / 4)) E R := by
  unfold TotalEntropyBekensteinBound
  rw [← hSat]
  intro h
  linarith

/-- **Record reading saturates the bound.** Given horizon saturation `A/4 = 2πER`, the
record-reading entropy `A/4` satisfies the bound with equality. -/
theorem record_reading_saturates (A E R : ℝ)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    TotalEntropyBekensteinBound (A / 4) E R :=
  le_of_eq hSat

/-- **The factor 3 is ledger-forced, not hand-typed.** The kernel-side (microstate) cost of
the one-face closure map is exactly three times its image-side (record) cost: `3 = 3 · 1`.
Both sides are computed by `decide` on the actual map; the `3` in "the microstate reading
assigns `3·(A/4)`" is THIS `3`. -/
theorem factor_three_is_ledger_forced :
    microstateCost (fun c : PixelLocal.FaceCfg => PixelLocal.closed c) true
      = 3 * recordCost (fun c : PixelLocal.FaceCfg => PixelLocal.closed c) := by
  decide

/-- **Scale-freeness of the violation.** The excess is exactly the constant 3 at every
saturated horizon: `3·(A/4) = 3·(2πER)` whenever `A/4 = 2πER`. This is what distinguishes
the keystone from a `δ`-shell or large-`R` correction argument. -/
theorem violation_is_scale_free (A E R : ℝ)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    3 * (A / 4) = 3 * (2 * Real.pi * E * R) := by
  rw [hSat]

What this page does not claim

The Bekenstein bound itself is not proved; it is an open hypothesis. The horizon saturation condition is not derived; it is a model input. The framework does not claim that the microstate reading is physically impossible in all circumstances, only that it is inconsistent within the stated conditional program. The theorem does not prove the Bekenstein-Hawking 1/4 factor; it discharges one premise conditionally.

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