Holography Correlator Kms Kms Witness Spectral Kms

The witness function

In the mathematics of heat and equilibrium, a KMS condition (a precise way of stating that a system is in thermal equilibrium at a given temperature) usually comes with a question: does anything actually satisfy it? The declaration kmsWitness_spectralKMS answers that question with a concrete example. It defines a function, kmsWitness beta x = exp(beta * x / 2), and proves that this function satisfies the spectral KMS condition at every frequency. The proof is a direct computation: substituting the definition into the condition and simplifying the exponentials shows the identity holds. This is a theorem, checked by the machine, not an assumption.

The role of this witness is to show the framework's premises are not contradictory. The framework builds a ladder of assumptions about how a system in a box exchanges energy with its surroundings. At the top of the ladder sits a geometric statement about a Euclidean time circle being smooth and symmetric. The witness function demonstrates that the spectral condition, the mathematical heart of that ladder, is satisfiable. It is a non-vacuity result: the premise set is exhibited, not merely hoped for. The function is also strictly positive for all real inputs, which the theorem kmsWitness_pos proves using the fact that the exponential of any real number is positive.

The witness function is not a physical prediction. It does not describe any particular material or system. It is a mathematical existence proof, a way of showing that the framework's axioms are consistent enough to support the structure built on them. The framework uses this witness to certify that its entire chain of reasoning, from geometric symmetry to thermodynamic rates, has at least one concrete model. This is a foundational check, not a statement about the observable world.

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

theorem kmsWitness_pos (beta x : ℝ) : 0 < kmsWitness beta x :=
  Real.exp_pos _

What this page does not claim

This witness function describes a specific physical system or material. The existence of this witness function proves the full framework's assumptions are physically realized.

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: