Encyclopedia Holography Holography Correlator Kms

ARTICLE 5 claims 5 theorems

Holography Correlator Kms

A symmetry of thermal fluctuations in imaginary time forces the Boltzmann factor, turning a geometric smoothness condition into a thermodynamic law.

Verify this page

The Correlator Bridge

In thermal physics, the KMS condition is a precise statement about how a system in equilibrium relates its ability to absorb and emit energy. For a transition between two states with an energy gap ω, the ratio of the rate of going forward to the rate of going backward is the Boltzmann factor exp(−βω), where β is the inverse temperature. This is the detailed balance condition that underpins the Gibbs state, the canonical distribution of statistical mechanics.

The holography correlator kms module in the Recognition Science framework derives this Boltzmann ratio from a much simpler and more geometric premise. The framework models a system's thermal fluctuations through a two-point function in imaginary time, a mathematical object that describes how correlations decay. The module assumes this correlator is reflection-symmetric: G_E(β − τ) = G_E(τ). This means that the imaginary time axis closes into a circle of circumference β with no distinguished direction, a statement about the smoothness of the underlying geometry, not a thermodynamic assertion.

The central theorem, proved in the machine-checked library of formal theorems, shows that this reflection symmetry forces the spectral weights of the emission and absorption channels into the Boltzmann ratio: g(−ω) = exp(−βω)·g(ω). The proof is direct. Evaluating the reflection identity at a single imaginary time τ = β/2 + 1/ω, clearing exponentials, and factoring gives (exp 2 − 1)·(g(ω) − g(−ω)·exp(βω)) = 0, and since exp 2 ≠ 1, the KMS spectral condition follows. The converse also holds, so for non-zero frequencies, reflection symmetry and the KMS condition are equivalent.

The framework then connects this to transition rates. It models rates as being proportional to the spectral weight at the energy released, a golden-rule form. With the KMS spectral condition, these rates satisfy the detailed balance ratio, turning a previously assumed thermodynamic premise into a derived theorem. The module assembles the full chain: reflection symmetry plus the golden rule plus detailed balance forces the reference state to be the Gibbs state, and from there the framework derives the Bekenstein bound on entropy, S(p) ≤ 2πER.

This bridge matters because it relocates the origin of thermodynamic behavior. The Boltzmann factor is not an independent assumption about rates; it is a consequence of a geometric property of the system's fluctuations in imaginary time. The module also exhibits a non-vacuous witness, a specific spectral function that satisfies all the premises, proving the assumptions are consistent and not merely hoped for.

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 correlator_forces_gibbs_form · bekenstein_bound_from_correlator · 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
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 · kmsWitness_pos · 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)
kmsWitness_pos · IndisputableMonolith/Holography/CorrelatorKMS.lean:241 
theorem kmsWitness_pos (beta x : ℝ) : 0 < kmsWitness beta x :=
  Real.exp_pos _

What this page does not claim

This module does not derive the value of the inverse temperature β; it takes the deficit-free period β = 2π/κ as a separate theorem. It does not prove that any arbitrary correlator is reflection-symmetric; reflection symmetry is a named MODEL premise. It does not claim that the golden-rule form of transition rates is derived; it is another named 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