Holography Correlator Kms Correlator Kmscert

The correlator certificate

In thermal physics, the KMS condition is a precise way to say a system is in equilibrium at a temperature. It relates the rates of forward and backward transitions between states: the rate of going from a lower energy to a higher one is exponentially suppressed compared to the reverse, with the suppression set by the inverse temperature β. This is the detailed balance that underlies the Boltzmann distribution.

The declaration correlatorKMSCert packages a machine-checked proof that this equilibrium condition is equivalent to a symmetry of a two-point correlation function. The correlator here is a two-mode exponential, G(τ) = g(ω)exp(−ωτ) + g(−ω)exp(ωτ), where g(±ω) are spectral weights for emission and absorption channels and τ is imaginary time. The symmetry is reflection symmetry, G(β − τ) = G(τ), meaning the Euclidean time circle closes with no preferred direction. The certificate proves that, for any nonzero frequency ω, this reflection symmetry holds if and only if the spectral weights satisfy the KMS condition g(−ω) = exp(−βω)g(ω). The zero-frequency mode is trivially KMS, so the equivalence holds at every frequency.

The certificate also shows that when transition rates are given by the golden rule, meaning the rate is the spectral weight at the energy released, the KMS spectral condition forces the rates to satisfy the KMS rate ratio. This is a derivation: the Boltzmann pricing of forward and backward rates is no longer assumed but follows from the reflection symmetry plus the golden-rule form. The certificate includes a witness, the function exp(βx/2), which is positive and satisfies the spectral condition at every frequency, demonstrating the premises are not empty.

In Recognition Science, this is Rung 4 of a premise ladder. Earlier rungs assumed the exponential form of the reference state or assumed the KMS rate ratio directly. This rung replaces those thermodynamic assumptions with a geometric one: reflection symmetry of the correlator at the deficit-free Euclidean period, which is β = 2π/κ for a horizon with surface gravity κ. The certificate is a theorem in the machine-checked library, meaning the forcing content is axiom-clean. The remaining model premises are reflection symmetry itself, the golden-rule form of the rates, detailed balance, and the condition Z ≤ 1 on the partition function.

What the certificate does not claim is that reflection symmetry is physically realized. It proves an equivalence and a derivation, not that any actual system obeys the symmetry. It also does not claim the golden-rule form of rates is forced; that remains a model choice. The certificate establishes the logical bridge from a geometric symmetry to a thermodynamic equilibrium condition, leaving the physical bridge as an open question.

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

/-- 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 kmsWitness_pos (beta x : ℝ) : 0 < kmsWitness beta x :=
  Real.exp_pos _

theorem kmsWitness_spectralKMS (beta omega : ℝ) :
    SpectralKMS (kmsWitness beta) beta omega := by
  unfold SpectralKMS kmsWitness
  rw [← Real.exp_add]; congr 1; ring

What this page does not claim

The certificate does not claim that any physical system actually exhibits the reflection symmetry. The certificate does not claim that the golden-rule form of rates is forced; it is a model premise. The certificate does not claim that the physical bridge from recognition to linking is established.

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: