Encyclopedia Holography Holography Correlator Kms Reflection Implies Spectral Kms

ARTICLE 5 claims 5 theorems

Holography Correlator Kms Reflection Implies Spectral Kms

A symmetry of a two-point function at finite temperature forces the Boltzmann factor, without assuming it.

Verify this page

The reflection theorem

In thermal physics, the two-point function measures how a disturbance at one time correlates with a disturbance at another. At finite temperature, this function is not symmetric in time: the emission and absorption channels of a transition pair carry different weights, and their ratio encodes the temperature. The standard derivation of that ratio, the Kubo-Martin-Schwinger (KMS) condition, assumes the system is in a thermal state. The Recognition Science declaration reflection_implies_spectralKMS replaces that thermodynamic assumption with a geometric one: if the two-point function is symmetric under reflection in imaginary time at period β, then the Boltzmann ratio follows.

Concretely, for a transition pair with energy gap ω, the Euclidean two-point function is a sum of two exponentials, one growing and one decaying, weighted by the spectral weights g(ω) and g(−ω). Reflection symmetry means the function at time τ equals the function at time β − τ for all τ, which states that Euclidean time closes into a circle with no distinguished direction. The theorem proves that this symmetry alone forces the weights into the Boltzmann ratio g(−ω) = exp(−βω)·g(ω). The proof is short: evaluate the symmetry at a single time τ = β/2 + 1/ω, clear the exponentials, and the identity factors into a nonzero constant times the desired relation. The zero-frequency case is trivially satisfied, so the condition holds at every frequency.

The declaration is part of a ladder that builds the Bekenstein bound from weaker premises. Earlier rungs assumed the exponential reference state, then derived it from free-energy minimality, then from a rate-level KMS ratio. This rung assumes only the reflection symmetry of the correlator, plus the golden-rule form of transition rates (rate proportional to spectral weight at the energy released). From those, the theorem derives the rate-level KMS ratio, which earlier rungs had taken as a premise. The full assembly, bekenstein_bound_from_correlator, then delivers the bound S(p) ≤ 2πER for every delivered record distribution.

The theorem is machine-checked in the framework's library of formal theorems. Its premises are named models: the reflection symmetry itself (the analytic shadow of seam smoothness), the golden-rule rate form, detailed balance, and the partition function bound. The theorem proves the implication, not the premises. A witness function kmsWitness β = exp(βx/2) is exhibited to show the premise set is non-vacuous: it is positive, satisfies the spectral condition at every frequency, and its pair correlator is reflection-symmetric at period β.

What the declaration does not claim is as important as what it proves. It does not prove that physical correlators are reflection-symmetric; that is a geometric model premise. It does not derive the value of β; that comes from a separate theorem fixing β = 2π/κ as the deficit-free Euclidean period. And it does not establish the Bekenstein bound by itself; the bound requires the additional premises of detailed balance, a positive spectral function, and the partition function bound. The theorem's contribution is narrower and cleaner: given the symmetry, the Boltzmann pricing is derived, not assumed.

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 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 spectralRates_kms · IndisputableMonolith/Holography/CorrelatorKMS.lean
spectralRates_kms · IndisputableMonolith/Holography/CorrelatorKMS.lean:213 
/-- Golden-rule rates from a KMS spectral function satisfy the Rung-3 rate ratio:
`W i j · exp(β·En j) = W j i · exp(β·En i)`. The Rung-3 premise `KMSRateRatio` is
now a THEOREM downstream of the correlator symmetry. -/
theorem spectralRates_kms {n : ℕ} {g : ℝ → ℝ} {beta : ℝ} (En : Fin n → ℝ)
    (hkms : ∀ omega, SpectralKMS g beta omega) :
    KMSRateRatio (spectralRates g En) beta En := by
  intro i j
  unfold spectralRates
  have h := hkms (En i - En j)
  have hji : En j - En i = -(En i - En j) := by ring
  rw [hji, h]
  have hexp : Real.exp (-(beta * (En i - En j))) * Real.exp (beta * En i)
      = Real.exp (beta * En j) := by
    rw [← Real.exp_add]; congr 1; ring
  linear_combination (-(g (En i - En j))) * hexp
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

The reflection symmetry of physical correlators is a model premise, not a derived theorem. The value of the Euclidean period β is fixed by a separate theorem, not by this declaration. The Bekenstein bound requires additional premises beyond reflection symmetry, including detailed balance and the partition function bound.

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