Encyclopedia Holography Holography Correlator Kms Bekenstein Bound From Correlator

ARTICLE 4 claims 4 theorems

Holography Correlator Kms Bekenstein Bound From Correlator

A symmetry of a quantum correlator, not a thermodynamic assumption, is enough to force the Bekenstein bound on entropy.

Verify this page

The correlator's bound

The Bekenstein bound is a physical limit that says the total entropy S of a system with energy E and size R cannot exceed 2πER (in units where the speed of light and Boltzmann's constant are 1). The declaration bekenstein_bound_from_correlator proves, in the machine-checked library of formal theorems, that this bound follows from a purely geometric premise: a two-point correlator's symmetry in imaginary time. The proof is a chain of implications that starts with a reflection symmetry of a Euclidean correlator and ends with the entropy bound.

The central object is a correlator, a function that measures how two events are related. The relevant one here is a two-mode exponential: G_E(τ) = g(ω)·exp(−ωτ) + g(−ω)·exp(ωτ), where τ is imaginary time and g(±ω) are spectral weights for emission and absorption channels. The premise is that this correlator is reflection-symmetric at period β: G_E(β − τ) = G_E(τ) for all τ. This symmetry says Euclidean time closes into a circle of circumference β with no distinguished direction, a statement about the smoothness of a geometric seam, not about thermodynamics.

The theorem reflection_implies_spectralKMS shows this reflection symmetry forces the spectral weights into the Boltzmann ratio: g(−ω) = exp(−βω)·g(ω). The proof evaluates the reflection identity at a single imaginary time τ = β/2 + 1/ω, clears exponentials, and the identity factors as (exp 2 − 1)·(g(ω) − g(−ω)·exp(βω)) = 0 with exp 2 ≠ 1. The converse also holds, so for nonzero frequencies reflection symmetry and the KMS spectral condition are equivalent. The zero mode ω = 0 is trivially KMS.

With the golden-rule form of transition rates, where a rate is the spectral weight at the energy released, the KMS spectral condition makes the rates satisfy the detailed-balance ratio. This forces the reference state to be the Gibbs state, and the full assembly yields the Bekenstein bound: every delivered record distribution obeys S(p) ≤ 2πER. The premise set is not merely hoped for; a witness function kmsWitness β = exp(βx/2) is positive, satisfies the spectral condition at every frequency, and its pair correlator is reflection-symmetric at period β.

In Recognition Science, this declaration shifts the premise ledger. Before, the Boltzmann pricing of forward and backward rates was a thermodynamic assumption at the rate level. After, that pricing is derived from a geometric smoothness statement plus the golden-rule rate form and detailed balance. The framework models the correlator's reflection symmetry as the analytic shadow of seam smoothness, and the thermodynamic rate ratio becomes a theorem rather than a postulate.

THEOREM reflection_implies_spectralKMS · IndisputableMonolith/Holography/CorrelatorKMS.lean
reflection_implies_spectralKMS · IndisputableMonolith/Holography/CorrelatorKMS.lean:131 
/-- **Reflection forces KMS.** If the pair correlator is reflection-symmetric at
period β and ω ≠ 0, the spectral weights satisfy `g(−ω) = exp(−βω)·g(ω)`. Proof:
evaluate the reflection identity at the single point `τ = β/2 + 1/ω`; after
clearing exponentials the identity factors as
`(exp 2 − 1)·(g(ω) − g(−ω)·exp(βω)) = 0`, and `exp 2 > 1`. -/
theorem reflection_implies_spectralKMS {g : ℝ → ℝ} {beta omega : ℝ}
    (homega : omega ≠ 0) (href : CorrelatorReflection g beta omega) :
    SpectralKMS g beta omega := by
  have h := href (beta / 2 + 1 / omega)
  unfold pairCorrelator at h
  -- Normalize the two exponent arguments using ω·(1/ω) = 1.
  have harg1 : omega * (beta - (beta / 2 + 1 / omega)) = omega * beta / 2 - 1 := by
    have hb : beta - (beta / 2 + 1 / omega) = beta / 2 - 1 / omega := by ring
    rw [hb, mul_sub, mul_one_div, div_self homega, ← mul_div_assoc]
  have harg2 : omega * (beta / 2 + 1 / omega) = omega * beta / 2 + 1 := by
    rw [mul_add, mul_one_div, div_self homega, ← mul_div_assoc]
  rw [harg1, harg2] at h
  set s := omega * beta / 2 with hs
  set a := g omega with ha
  set b := g (-omega) with hb
  -- Product identities collapsing the four exponentials onto exp 2 and exp (2s).
  have e1 : Real.exp (-(s - 1)) * Real.exp (s + 1) = Real.exp 2 := by
    rw [← Real.exp_add]; congr 1; ring
  have e2 : Real.exp (s - 1) * Real.exp (s + 1) = Real.exp (2 * s) := by
    rw [← Real.exp_add]; congr 1; ring
  have e3 : Real.exp (-(s + 1)) * Real.exp (s + 1) = 1 := by
    rw [← Real.exp_add, neg_add_cancel, Real.exp_zero]
  have e4 : Real.exp (s + 1) * Real.exp (s + 1) = Real.exp (2 * s) * Real.exp 2 := by
    rw [← Real.exp_add, ← Real.exp_add]; congr 1; ring
  -- Multiply the evaluated reflection identity through by exp (s + 1).
  have key : a * Real.exp 2 + b * Real.exp (2 * s)
      = a + b * (Real.exp (2 * s) * Real.exp 2) := by
    linear_combination Real.exp (s + 1) * h - a * e1 - b * e2 + a * e3 + b * e4
  have factored : (Real.exp 2 - 1) * (a - b * Real.exp (2 * s)) = 0 := by
    linear_combination key
  have hexp2 : (1 : ℝ) < Real.exp 2 := Real.one_lt_exp_iff.mpr (by norm_num)
  have hne : Real.exp 2 - 1 ≠ 0 := sub_ne_zero.mpr (ne_of_gt hexp2)
  have hfac : a - b * Real.exp (2 * s) = 0 := (mul_eq_zero.mp factored).resolve_left hne
  have hab : a = b * Real.exp (2 * s) := sub_eq_zero.mp hfac
  -- Convert exp (2s) = exp (βω) into the Boltzmann ratio.
  have hprod : Real.exp (-(beta * omega)) * Real.exp (2 * s) = 1 := by
    rw [← Real.exp_add]
    have harg : -(beta * omega) + 2 * s = 0 := by rw [hs]; ring
    rw [harg, Real.exp_zero]
  show b = Real.exp (-(beta * omega)) * a
  linear_combination -Real.exp (-(beta * omega)) * hab - b * hprod
THEOREM correlatorReflection_iff_spectralKMS · IndisputableMonolith/Holography/CorrelatorKMS.lean
correlatorReflection_iff_spectralKMS · IndisputableMonolith/Holography/CorrelatorKMS.lean:196 
/-- **Equivalence** (ω ≠ 0): reflection symmetry of the two-mode Euclidean
correlator at period β IS the KMS spectral condition. -/
theorem correlatorReflection_iff_spectralKMS {g : ℝ → ℝ} {beta omega : ℝ}
    (homega : omega ≠ 0) :
    CorrelatorReflection g beta omega ↔ SpectralKMS g beta omega :=
  ⟨reflection_implies_spectralKMS homega, spectralKMS_implies_reflection⟩
THEOREM bekenstein_bound_from_correlator · IndisputableMonolith/Holography/CorrelatorKMS.lean
bekenstein_bound_from_correlator · IndisputableMonolith/Holography/CorrelatorKMS.lean:275 
/-- **CONDITIONAL Bekenstein bound for ALL states, from correlator symmetry.**
Identical conclusion to the Rung-3 assembly (`S(p) ≤ 2πER` for every delivered
record distribution), with the rate-level KMS premise replaced by its geometric
source: the Euclidean seam correlator is reflection-symmetric at the deficit-free
period `β = 2π/κ`, the rates have golden-rule form, and the reference is stationary
under them. The chain: reflection forces the KMS spectral condition at every
frequency (THEOREM), golden-rule rates then satisfy the rate ratio (THEOREM), KMS +
detailed balance force the Gibbs form (THEOREM), the Gibbs inequality prices the
delivered state (THEOREM), `Z ≤ 1` converts the offset into slack (premise), and
the deficit-free period supplies `β = 2πR` (THEOREM given `HorizonRate`). -/
theorem bekenstein_bound_from_correlator {n : ℕ}
    (p q En : Fin n → ℝ) (g : ℝ → ℝ) (beta kappa E R : ℝ)
    (hp : ∀ i, 0 ≤ p i) (hp1 : ∑ i, p i = 1)
    (href : ∀ omega, CorrelatorReflection g beta omega)
    (hg : ∀ x, 0 < g x)
    (hdb : DetailedBalance q (spectralRates g En))
    (hq1 : ∑ i, q i = 1)
    (hZ : partitionFunction beta En ≤ 1)
    (hR : DeficitFreePeriod.HorizonRate kappa R) (hkappa : 0 < kappa)
    (hbeta : beta = DeficitFreePeriod.euclideanPeriod kappa)
    (hE : ∑ i, p i * En i ≤ E) :
    KeystoneFactorThree.TotalEntropyBekensteinBound (shannonEntropy p) E R := by
  have hkms_spec : ∀ omega, SpectralKMS g beta omega := by
    intro omega
    by_cases homega : omega = 0
    · subst homega; exact spectralKMS_zero g beta
    · exact reflection_implies_spectralKMS homega (href omega)
  exact bekenstein_bound_from_kms p q En (spectralRates g En) beta kappa E R hp hp1
    (spectralRates_kms En hkms_spec) hdb (spectralRates_pos En hg) hq1 hZ hR hkappa
    hbeta hE
THEOREM kmsWitness_reflection · IndisputableMonolith/Holography/CorrelatorKMS.lean
kmsWitness_reflection · IndisputableMonolith/Holography/CorrelatorKMS.lean:249 
/-- The witness's pair correlator is reflection-symmetric at period β for every
frequency: the correlator premise set is satisfiable. -/
theorem kmsWitness_reflection (beta omega : ℝ) :
    CorrelatorReflection (kmsWitness beta) beta omega :=
  spectralKMS_implies_reflection (kmsWitness_spectralKMS beta omega)

What this page does not claim

The declaration does not prove that any real physical system satisfies the correlator reflection premise. It does not derive the value of the period β from first principles; β = 2π/κ is a separate theorem. It does not claim the golden-rule rate form is derived rather than assumed; that is a MODEL premise.

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