Holography Correlator Kms Spectral Kms Implies Reflection

Reflection and the KMS condition

In quantum field theory at finite temperature, the KMS condition is a precise way to say that a system is in thermal equilibrium. It relates the rates of forward and backward transitions: the probability of absorbing a quantum of energy ω is exp(−βω) times the probability of emitting it, where β is the inverse temperature. This Boltzmann-like ratio is the fingerprint of a thermal state.

The Recognition Science framework's machine-checked library of formal results proves that this thermal fingerprint follows from a purely geometric assumption. The key object is the Euclidean two-point correlator, a function G_E(τ) that describes how a quantum field at imaginary time τ correlates with itself at a later imaginary time. The assumption is reflection symmetry: G_E(β − τ) = G_E(τ) for all τ, meaning the imaginary time axis closes into a circle of circumference β with no distinguished direction.

The declaration spectralKMS_implies_reflection states that this reflection symmetry, together with the golden-rule form of transition rates (rate proportional to spectral weight at the energy released), forces the spectral weights into the Boltzmann ratio: g(−ω) = exp(−βω)·g(ω). This is the KMS spectral condition. The proof is elementary: evaluate the reflection identity at a single imaginary time τ = β/2 + 1/ω, and the identity factors into a product of a nonzero constant and the desired relation.

In Recognition Science, this result is Rung 4 of a premise ladder. Earlier rungs assumed the Boltzmann ratio directly; this rung derives it from the more geometric premise of reflection symmetry. The full assembly, bekenstein_bound_from_correlator, uses this to derive the Bekenstein bound S(p) ≤ 2πER for a system with energy E and size R, a statement about the maximum entropy a region can hold.

The result does not claim that reflection symmetry is a fundamental law of nature. It is a MODEL premise, a definitional choice about the analytic structure of the correlator at the seam. The result also does not claim that the Boltzmann ratio holds for all systems; it holds for those satisfying the stated premises: reflection symmetry, golden-rule rates, and detailed balance. The proof is conditional, not unconditional.

/-- **KMS implies reflection** (every ω, no nonvanishing needed): substituting
`g(−ω) = exp(−βω)·g(ω)` makes `G_E(β − τ) = G_E(τ)` an exponential identity. -/
theorem spectralKMS_implies_reflection {g : ℝ → ℝ} {beta omega : ℝ}
    (hkms : SpectralKMS g beta omega) : CorrelatorReflection g beta omega := by
  intro tau
  unfold pairCorrelator
  rw [hkms]
  have h1 : Real.exp (-(omega * (beta - tau)))
      = Real.exp (-(beta * omega)) * Real.exp (omega * tau) := by
    rw [← Real.exp_add]; congr 1; ring
  have h2 : Real.exp (omega * (beta - tau))
      = Real.exp (beta * omega) * Real.exp (-(omega * tau)) := by
    rw [← Real.exp_add]; congr 1; ring
  rw [h1, h2]
  have h3 : Real.exp (-(beta * omega)) * Real.exp (beta * omega) = 1 := by
    rw [← Real.exp_add, neg_add_cancel, Real.exp_zero]
  linear_combination g omega * Real.exp (-(omega * tau)) * h3

/-- **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

/-- Named MODEL premise (B2/B3 output shape): the Euclidean seam correlator is
reflection-symmetric in imaginary time at period β, `G_E(β − τ) = G_E(τ)` for all
τ. At the deficit-free period `β = 2π/κ` this says the correlator lives on the
smooth Euclidean cone: imaginary time closes into a circle of circumference β with
no distinguished direction across the seam. -/
def CorrelatorReflection (g : ℝ → ℝ) (beta omega : ℝ) : Prop :=
  ∀ tau : ℝ, pairCorrelator g omega (beta - tau) = pairCorrelator g omega tau

What this page does not claim

Reflection symmetry is a fundamental law; it is a modeling assumption. The Boltzmann ratio holds for all systems; it holds only under the stated premises. The result proves the Bekenstein bound without additional assumptions such as detailed balance and a positive spectral function.

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: