Encyclopedia Holography Holography Keystone Factor Three Record Chain Saturates Bound

ARTICLE 6 claims 6 theorems

Holography Keystone Factor Three Record Chain Saturates Bound

A machine-checked theorem shows one way of counting a black hole horizon's entropy hits the Bekenstein bound exactly, while a rival counting misses it by a fixed factor of three.

Verify this page

The record chain and its bound

Entropy, in thermodynamics, is a count of the possible microscopic arrangements behind a system's gross state. For a black hole, the famous Bekenstein-Hawking formula sets that entropy to one quarter of the horizon's area in Planck units, the A/4 that appears throughout modern gravity. A long-standing question is what that quarter actually counts: the quantum states of the horizon itself, or something more abstract. Recognition Science offers a machine-checked answer to that question, but only inside a carefully labeled conditional argument.

The framework's ledger, a discrete record of events, supplies two ways to count the horizon's degrees of freedom. The record reading assigns each pixel of the horizon one unit of entropy; the microstate reading assigns three. A proved theorem, factor_three_is_ledger_forced, establishes that the microstate cost is exactly three times the record cost, a ratio fixed by the framework's internal arithmetic rather than chosen by hand. At the density level, the same theorem gives free bits at 3/4 versus closure rank at 1/4, again a strict factor of three.

The declaration record_chain_saturates_bound assembles the record reading with two further premises. First, the horizon's total entropy is the per-pixel sum over N pixels. Second, the horizon saturates the Bekenstein bound: A/4 equals 2πER for a Schwarzschild black hole of energy E and radius R. Given those, the theorem proves the record-reading entropy S satisfies the bound, S ≤ 2πER, with equality. The record chain is consistent: it lands exactly on the bound, not above it.

The companion theorem microstate_chain_contradicts_bound shows the rival reading fails the same test. Under the microstate reading, S equals 3N, and with saturation this becomes 3·(A/4), which strictly exceeds 2πER. The violation is scale-free: at every horizon radius, the microstate entropy is exactly three times the bound, with no volume scaling, no bulk-to-boundary map, and no large-radius limit needed. Unit conversion from bits to nats cannot rescue it, since multiplying both sides by ln 2 preserves the strict inequality.

What the keystone does not do is prove the Bekenstein bound itself. The bound appears as an explicit typed premise, TotalEntropyBekensteinBound, consumed as a hypothesis and never asserted. The saturation condition A/4 = 2πER is likewise a model input, not a theorem. Conditional on those two named legs plus per-pixel additivity, the framework discharges the record reading by exclusion: within the proved dichotomy, it is the unique reading consistent with a saturated horizon. The exclusion is a conditional discharge, not an unconditional derivation of A/4.

THEOREM factor_three_is_ledger_forced · IndisputableMonolith/Holography/KeystoneFactorThree.lean
factor_three_is_ledger_forced · IndisputableMonolith/Holography/KeystoneFactorThree.lean:64 
/-- **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
THEOREM record_chain_saturates_bound · IndisputableMonolith/Holography/KeystoneFactorThree.lean
record_chain_saturates_bound · IndisputableMonolith/Holography/KeystoneFactorThree.lean:167 
/-- **The record chain is consistent (saturation).** The same assembly under the RECORD
reading (`m = 1`) yields `S = N = 2πER`: the bound is saturated, not violated. Together
with `microstate_chain_contradicts_bound` this is the conditional discharge of
`HorizonEntropyIsRecordCost`: within the proved dichotomy, it is the unique reading
consistent with the (hypothesized) total-entropy Bekenstein bound at a saturated
horizon. -/
theorem record_chain_saturates_bound
    (m N : ℕ) (S E R : ℝ)
    (hRec : HorizonEntropyIsRecordCost m)
    (hAdd : S = (m : ℝ) * N)
    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R) :
    TotalEntropyBekensteinBound S E R := by
  have hm : m = 1 := by
    unfold HorizonEntropyIsRecordCost at hRec
    rw [hRec]; exact recordCost_closed
  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
  rw [hA] at hSat
  unfold TotalEntropyBekensteinBound
  rw [hAdd, hm]
  push_cast
  linarith [le_of_eq hSat]
THEOREM record_chain_saturates_bound · IndisputableMonolith/Holography/KeystoneFactorThree.lean
record_chain_saturates_bound · IndisputableMonolith/Holography/KeystoneFactorThree.lean:167 
/-- **The record chain is consistent (saturation).** The same assembly under the RECORD
reading (`m = 1`) yields `S = N = 2πER`: the bound is saturated, not violated. Together
with `microstate_chain_contradicts_bound` this is the conditional discharge of
`HorizonEntropyIsRecordCost`: within the proved dichotomy, it is the unique reading
consistent with the (hypothesized) total-entropy Bekenstein bound at a saturated
horizon. -/
theorem record_chain_saturates_bound
    (m N : ℕ) (S E R : ℝ)
    (hRec : HorizonEntropyIsRecordCost m)
    (hAdd : S = (m : ℝ) * N)
    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R) :
    TotalEntropyBekensteinBound S E R := by
  have hm : m = 1 := by
    unfold HorizonEntropyIsRecordCost at hRec
    rw [hRec]; exact recordCost_closed
  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
  rw [hA] at hSat
  unfold TotalEntropyBekensteinBound
  rw [hAdd, hm]
  push_cast
  linarith [le_of_eq hSat]
THEOREM microstate_chain_contradicts_bound · IndisputableMonolith/Holography/KeystoneFactorThree.lean
microstate_chain_contradicts_bound · IndisputableMonolith/Holography/KeystoneFactorThree.lean:140 
/-- **The microstate chain is inconsistent (the keystone, fully typed).** Assemble the
named premises: the horizon carries per-pixel multiplicity `m` under the MICROSTATE
reading (`HorizonEntropyIsMicrostateCost`, so `m = 3` by `decide`); total entropy is
per-pixel additive over `N ≥ 1` private pixels (LEG-A, `hAdd`); the horizon area in pixel
units is `rawBits · N = 4N` and saturates `A/4 = 2πER` (`hSat`); and the total-entropy
Bekenstein bound holds (LEG-B, `hBound`). CONTRADICTION: `S = 3N > N = 2πER`. So within
the dichotomy, conditional on LEG-A + LEG-B + saturation, the microstate reading is
excluded and `HorizonEntropyIsRecordCost` is forced. -/
theorem microstate_chain_contradicts_bound
    (m N : ℕ) (S E R : ℝ) (hN : 0 < N)
    (hMicro : HorizonEntropyIsMicrostateCost m)
    (hAdd : S = (m : ℝ) * N)
    (hSat : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) / 4 = 2 * Real.pi * E * R)
    (hBound : TotalEntropyBekensteinBound S E R) :
    False := by
  have hm : m = 3 := by
    unfold HorizonEntropyIsMicrostateCost at hMicro
    rw [hMicro]; decide
  have hA : ((CoefficientBridge.rawBits * N : ℕ) : ℝ) = 4 * N := by
    rw [CoefficientBridge.rawBits_eq_four]; push_cast; ring
  rw [hA] at hSat
  unfold TotalEntropyBekensteinBound at hBound
  rw [hAdd, hm, ← hSat] at hBound
  have hNpos : (0 : ℝ) < N := by exact_mod_cast hN
  push_cast at hBound
  linarith
THEOREM violation_is_scale_free · IndisputableMonolith/Holography/KeystoneFactorThree.lean
violation_is_scale_free · IndisputableMonolith/Holography/KeystoneFactorThree.lean:123 
/-- **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]
THEOREM TotalEntropyBekensteinBound · IndisputableMonolith/Holography/KeystoneFactorThree.lean
TotalEntropyBekensteinBound · IndisputableMonolith/Holography/KeystoneFactorThree.lean:84 
/-- **LEG-B, total-entropy-typed (OPEN; a premise, never proved here).** The Casini-form
Bekenstein bound on the TOTAL static thermodynamic horizon entropy `S` (same units as the
area term; bits or nats, fixed consistently on both sides). This is the reading the panel
demanded: `S` is a static count (candidates C3/C6 of `EntropyCandidateAudit`), NOT the
posted-information RATE `accessibleInfo` (nats·tick⁻¹), which has the wrong type to appear
here. -/
def TotalEntropyBekensteinBound (S E R : ℝ) : Prop :=
  S ≤ 2 * Real.pi * E * R

What this page does not claim

The Bekenstein bound itself is not proved, only assumed as a premise. The microstate reading is excluded only conditional on the named premises, not unconditionally. The record reading is not derived from first principles; it is selected by exclusion within a dichotomy. No claim is made about the physical correctness of the framework's ledger model for real black holes.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND