Encyclopedia Holography Holography Correlator Kms Correlator Reflection Iff Spectral Kms

ARTICLE 4 claims 4 theorems

Holography Correlator Kms Correlator Reflection Iff Spectral Kms

A symmetry of a two-point function in imaginary time is exactly equivalent to a thermodynamic rate ratio, and the proof is a single line of algebra.

Verify this page

The reflection-KMS bridge

In quantum statistical mechanics, the Kubo-Martin-Schwinger (KMS) condition is the standard way to say that a system is in thermal equilibrium: it fixes the ratio of rates for a transition and its reverse as a Boltzmann factor exp(−βω), where β is inverse temperature and ω the energy gap. The condition is usually taken as an axiom about transition rates. This page reports a theorem that replaces that axiom with a geometric statement about a two-point function in imaginary time.

The object is the finite-temperature Euclidean two-point function of a pair of energy levels separated by ω, written as G_E(τ) = g(ω)·exp(−ωτ) + g(−ω)·exp(ωτ), where g(±ω) are spectral weights for emission and absorption. The geometric premise is reflection symmetry: G_E(β − τ) = G_E(τ) for all τ, meaning the imaginary-time circle closes with no distinguished direction. The theorem correlatorReflection_iff_spectralKMS states that, for ω ≠ 0, this reflection symmetry holds if and only if the spectral weights satisfy the KMS condition g(−ω) = exp(−βω)·g(ω). The proof is one line: evaluate the reflection identity at τ = β/2 + 1/ω, and the exponentials cancel to give the ratio.

The equivalence is a bridge from geometry to thermodynamics. Reflection symmetry is a smoothness statement about the Euclidean seam; the KMS ratio is a statement about rates. The theorem shows they are the same fact. It also gives a path to the Gibbs state: reflection symmetry plus the golden-rule form of rates plus detailed balance forces the reference state to be the Gibbs state, and from there the Bekenstein bound S(p) ≤ 2πER follows as a theorem. The framework's library proves all of this in a machine-checked setting, with the premises named as models and the forcing content as theorems.

The theorem does not claim that reflection symmetry is always true, nor that the golden-rule form of rates is always true. Those are model premises, chosen for the physical situations the framework targets. The equivalence itself is unconditional for ω ≠ 0; the zero mode ω = 0 satisfies the KMS condition trivially. The theorem also does not claim that the KMS condition is the only way to get a Gibbs state, only that within this premise set the two statements are interchangeable.

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 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 correlator_forces_gibbs_form · IndisputableMonolith/Holography/CorrelatorKMS.lean
correlator_forces_gibbs_form · IndisputableMonolith/Holography/CorrelatorKMS.lean:257 
/-- **Correlator symmetry forces the Gibbs form.** A normalized state stationary
under golden-rule rates whose seam correlator is reflection-symmetric at period β
IS the Gibbs state at inverse temperature β. -/
theorem correlator_forces_gibbs_form {n : ℕ} (hn : 0 < n) {q : Fin n → ℝ}
    {g : ℝ → ℝ} {beta : ℝ} {En : Fin n → ℝ}
    (href : ∀ omega, CorrelatorReflection g beta omega)
    (hg : ∀ x, 0 < g x)
    (hdb : DetailedBalance q (spectralRates g En))
    (hq1 : ∑ i, q i = 1) :
    q = gibbsState beta En := 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 kms_forces_gibbs_form hn (spectralRates_kms En hkms_spec) hdb
    (spectralRates_pos En hg) hq1
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

What this page does not claim

Reflection symmetry is not claimed to hold for all physical systems; it is a model premise. The golden-rule form of rates is not claimed to be universal; it is a model premise. The theorem does not claim that the KMS condition is the only route to a Gibbs state.

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