Holography Keystone Factor Three

The factor-3 keystone

The Bekenstein bound is a physical limit: the total entropy of a system cannot exceed twice pi times its energy times its radius, written S ≤ 2πER. For a black hole, this bound is saturated, meaning the entropy sits exactly at the limit. The famous Bekenstein-Hawking formula says that entropy equals one quarter of the horizon's area, A/4. The question is what that quarter means. One reading treats it as a record of events on the horizon itself, a kind of ledger of what has happened there. Another reading treats it as a count of the internal microstates, the hidden configurations of the hole's interior.

In Recognition Science, these two readings are distinguished by a machine-checked library of formal theorems. The framework proves that the cost of recognizing a closed face on the horizon is exactly three times larger under the microstate reading than under the record reading. The theorem factor_three_is_ledger_forced states this as a strict equality: microstateCost = 3 · recordCost. This factor of three is not an assumption; it is computed by the proof checker from the definition of the cost itself. At the density level, the same ratio appears: the free bits are three times the closure rank, out of four raw bits per pixel.

The keystone result assembles this factor with two other premises. The first is per-pixel additivity, meaning the total entropy is the sum over individual pixels. The second is the Bekenstein bound itself, stated as a hypothesis about total thermodynamic entropy, not about an information rate. Given these, the record reading saturates the bound exactly: A/4 = 2πER. The microstate reading, by contrast, gives 3·(A/4), which strictly violates the bound. The theorem keystone_selects_record_reading proves this separation: record passes with equality, microstate fails by the fixed factor of three. The violation is scale-free, holding at every horizon radius, and it survives a change of units from bits to nats.

This is a conditional exclusion, not an unconditional proof. The Bekenstein bound for total entropy is an open hypothesis, stated as a typed premise and never asserted. The saturation condition A/4 = 2πER is a model input from Schwarzschild geometry. Given those two named inputs plus additivity, the microstate reading is inconsistent, not merely disfavored. The value of this result is the exclusion structure: it shows that the 1/4 in the entropy formula cannot be a microstate count, because that count would violate a fundamental limit by exactly three times. The record reading is the only one consistent with the bound at a saturated horizon.

What this changes is the status of the 1/4 coefficient. It is no longer a bare identification. Inside the holographic program, with the bound and saturation in place, the microstate reading is ruled out by a machine-checked contradiction. The record reading remains, and it saturates the bound exactly. The factor of three is the sharp edge of that exclusion: it is the precise amount by which the wrong reading fails.

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

/-- **The keystone package.** Under saturation, the two readings are separated by the
bound itself: record passes (with equality), microstate fails (strictly). Conditional on
LEG-B this is the selector discharge. -/
theorem keystone_selects_record_reading (A E R : ℝ) (hA : 0 < A)
    (hSat : A / 4 = 2 * Real.pi * E * R) :
    TotalEntropyBekensteinBound (A / 4) E R
      ∧ ¬ TotalEntropyBekensteinBound (3 * (A / 4)) E R :=
  ⟨record_reading_saturates A E R hSat, microstate_reading_violates A E R hA hSat⟩

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

/-- **The unit choice cannot rescue the microstate reading.** A strict violation in bits
stays a strict violation in nats (multiplying both sides by `ln 2 > 0`), so the exclusion
is invariant under the `EntropyCandidateAudit.bitsToNats` conversion. -/
theorem violation_survives_unit_conversion (S bound : ℝ) (h : bound < S) :
    bound * Real.log 2 < S * Real.log 2 :=
  mul_lt_mul_of_pos_right h (Real.log_pos (by norm_num))

What this page does not claim

This does not prove the Bekenstein bound itself; it is consumed as an open hypothesis. This does not derive the 1/4 coefficient unconditionally; it only excludes the microstate reading conditional on the named premises. This does not claim the microstate reading is physically impossible, only that it is inconsistent with the bound and saturation within the framework's dichotomy.

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: