Encyclopedia Holography Holography Gibbs Casini Bound Bekenstein Bound Nonvacuous

ARTICLE 2 claims 2 theorems

Holography Gibbs Casini Bound Bekenstein Bound Nonvacuous

A machine-checked proof shows the Bekenstein bound is not an empty statement: a simple two-record system saturates it exactly.

Verify this page

A concrete witness

The Bekenstein bound is a famous physics conjecture: the entropy inside a region, measured in natural units, cannot exceed 2π times the region's energy times its radius. For decades it has been a statement about black holes and quantum gravity, tested in special cases but not derived from a general principle. The Recognition Science framework, which models physical reality as a discrete ledger of recognition events, has been working toward a proof of this bound. A key worry for any such proof is vacuity: if the bound only held for states that never occur, it would be a hollow theorem.

The declaration bekenstein_bound_nonvacuous in the framework's machine-checked library of formal theorems addresses that worry directly. It exhibits a concrete, finite system: two records, each equally likely, with a total energy of log 2 divided by 2π and a radius of 1. For this system, the theorem proves that the entropy, which is log 2, exactly equals 2π times the energy times the radius. The bound is not merely satisfied; it is saturated. This shows the entropy functional is not identically zero and that the bound is a real constraint on actual states, not a statement about nothing.

The proof rests on the Gibbs inequality, a classical result in information theory: for any probability distribution p and any positive reference distribution q, the Shannon entropy of p is at most the cross entropy of p against q. In the framework's finite setting, this is proved from a single tangent-line bound, log x ≤ x − 1, summed over the records. The reference distribution is chosen to be a Gibbs state at a specific period, and the modular Hamiltonian then prices each record linearly in its energy. The 2π in the bound comes from the deficit-free period, a separate theorem in the framework.

What the declaration does not claim is just as important. It does not prove the Bekenstein bound for all states; that is a separate, conditional theorem that assumes the reference state is thermal. The non-vacuity witness only shows the bound can be met. It does not claim that the reference state's thermality is derived; that remains an open problem in the framework. And it does not extend to the continuum limit of quantum field theory, where the argument would require operator algebras rather than finite sums. The witness is a sanity check, a concrete proof that the framework's path to the Bekenstein bound is not vacuous.

THEOREM bekenstein_bound_nonvacuous · IndisputableMonolith/Holography/GibbsCasiniBound.lean
bekenstein_bound_nonvacuous · IndisputableMonolith/Holography/GibbsCasiniBound.lean:252 
/-- End-to-end non-vacuity witness: a concrete two-record seam (uniform delivered
state, matching Gibbs reference at `κ = 1`, `R = 1`, `β = 2π`, record energies
`log 2 / 2π`) satisfies every hypothesis of the assembly and SATURATES the bound:
`S = log 2 = 2πER`. -/
theorem bekenstein_bound_nonvacuous :
    KeystoneFactorThree.TotalEntropyBekensteinBound
      (shannonEntropy (fun _ : Fin 2 => (1 : ℝ) / 2))
      (Real.log 2 / (2 * Real.pi)) 1 := by
  refine bekenstein_bound_from_gibbs_reference
    (fun _ => (1 : ℝ) / 2) (fun _ => (1 : ℝ) / 2)
    (fun _ => Real.log 2 / (2 * Real.pi))
    (2 * Real.pi) 1 (Real.log 2 / (2 * Real.pi)) 1
    (fun _ => by norm_num) ?_ ?_ ?_ ?_ one_pos ?_ ?_
  · rw [Fin.sum_univ_two]; norm_num
  · intro i
    have hval : 2 * Real.pi * (Real.log 2 / (2 * Real.pi)) = Real.log 2 := by
      have h2pi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
      field_simp
    show (1 : ℝ) / 2 = Real.exp (-(2 * Real.pi * (Real.log 2 / (2 * Real.pi))))
    rw [hval, Real.exp_neg, Real.exp_log (by norm_num : (0 : ℝ) < 2), one_div]
  · rw [Fin.sum_univ_two]; norm_num
  · show (1 : ℝ) = 1 / 1
    norm_num
  · show (2 : ℝ) * Real.pi = DeficitFreePeriod.euclideanPeriod 1
    unfold DeficitFreePeriod.euclideanPeriod
    norm_num
  · exact le_of_eq (by rw [Fin.sum_univ_two]; ring)
THEOREM gibbs_inequality · IndisputableMonolith/Holography/GibbsCasiniBound.lean
gibbs_inequality · IndisputableMonolith/Holography/GibbsCasiniBound.lean:100 
/-- **Gibbs inequality.** For a probability vector `p` and a positive reference `q`
with `∑ q ≤ 1` (subnormalized allowed): `S(p) ≤ ⟨K_q⟩_p`. This is relative-entropy
positivity, the finite form of Casini's bound. The entire proof reduces to the
tangent-line bound `log x ≤ x − 1` applied per record at `x = q i / p i`. -/
theorem gibbs_inequality {n : ℕ} (p q : Fin n → ℝ)
    (hp : ∀ i, 0 ≤ p i) (hq : ∀ i, 0 < q i)
    (hp1 : ∑ i, p i = 1) (hq1 : ∑ i, q i ≤ 1) :
    shannonEntropy p ≤ crossEntropy p q := by
  -- Per-record tangent bound: p·(log q − log p) ≤ q − p.
  have key : ∀ i : Fin n, p i * (Real.log (q i) - Real.log (p i)) ≤ q i - p i := by
    intro i
    rcases eq_or_lt_of_le (hp i) with h0 | hpi
    · rw [← h0]
      simpa using (hq i).le
    · have hdiv : 0 < q i / p i := div_pos (hq i) hpi
      have hlog : Real.log (q i / p i) ≤ q i / p i - 1 :=
        Real.log_le_sub_one_of_pos hdiv
      have hlogdiv : Real.log (q i / p i) = Real.log (q i) - Real.log (p i) :=
        Real.log_div (ne_of_gt (hq i)) (ne_of_gt hpi)
      have hmul : p i * Real.log (q i / p i) ≤ p i * (q i / p i - 1) :=
        mul_le_mul_of_nonneg_left hlog hpi.le
      have hpne : p i ≠ 0 := ne_of_gt hpi
      have hpq : p i * (q i / p i) = q i := by
        field_simp
      have hcancel : p i * (q i / p i - 1) = q i - p i := by
        calc p i * (q i / p i - 1) = p i * (q i / p i) - p i := by ring
          _ = q i - p i := by rw [hpq]
      calc p i * (Real.log (q i) - Real.log (p i))
          = p i * Real.log (q i / p i) := by rw [hlogdiv]
        _ ≤ p i * (q i / p i - 1) := hmul
        _ = q i - p i := hcancel
  -- Sum the per-record bounds; the mass difference is ≤ 0.
  have hsum : ∑ i, p i * (Real.log (q i) - Real.log (p i)) ≤ ∑ i, (q i - p i) :=
    Finset.sum_le_sum fun i _ => key i
  have hmass : ∑ i, (q i - p i) ≤ 0 := by
    rw [Finset.sum_sub_distrib, hp1]
    linarith
  have hexpand : ∑ i, p i * (Real.log (q i) - Real.log (p i))
      = (∑ i, p i * Real.log (q i)) - ∑ i, p i * Real.log (p i) := by
    rw [← Finset.sum_sub_distrib]
    exact Finset.sum_congr rfl fun i _ => by ring
  have hdiff : (∑ i, p i * Real.log (q i)) - (∑ i, p i * Real.log (p i)) ≤ 0 := by
    rw [← hexpand]
    linarith
  simp only [shannonEntropy, crossEntropy, modularHamiltonian]
  have hneg : (∑ i, p i * -Real.log (q i)) = -(∑ i, p i * Real.log (q i)) := by
    simp [mul_neg]
  rw [hneg]
  linarith

What this page does not claim

The declaration does not prove the Bekenstein bound for all states. The declaration does not derive the thermality of the reference state. The declaration does not cover the continuum (type-III algebra) version of Casini's argument.

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/GibbsCasiniBound.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