Holography Circle Correlator Circle Correlator Cert

The circle certificate

In thermal quantum field theory, a two-point correlation function measures how strongly two disturbances at different times are related. When time is rotated into imaginary values, a standard technique called the Euclidean formalism, the function becomes periodic: the system repeats itself after a fixed interval known as the inverse temperature. A separate property, evenness, states that swapping the two disturbances leaves the correlation unchanged, which holds when the insertions are identical.

The Recognition Science framework's machine-checked library of formal theorems contains a declaration, circleCorrelatorCert, that bundles together a proof about these two properties. The central result, a theorem named periodic_even_reflection, shows that if a correlator is both periodic with period β and even, then it automatically satisfies a reflection symmetry: the value at β minus τ equals the value at τ. This is a purely mathematical consequence of the two premises, requiring no additional physical assumptions about thermodynamics or dynamics.

The proof works because the two properties together mean the correlator lives on a circle of circumference β. Periodicity identifies points separated by β, and evenness identifies τ with minus τ. Reflecting across the half-period β/2 is then just a combination of these two identifications, so the symmetry is forced by the circle topology itself. The framework's library also provides a concrete example, the cosine function cos(2πτ/β), which satisfies both premises and demonstrates that the result is not vacuous.

In Recognition Science, this certificate matters because it replaces a previously assumed premise. An earlier rung of the framework's derivation ladder treated reflection symmetry as a model assumption. This certificate derives it from the more primitive circle properties, meaning the assumption is now a proved consequence. The framework's own documentation describes this as the circle triviality, emphasizing that the result is a structural fact about periodicity and evenness, not a dynamical input.

What the certificate does not claim is also important. It does not assert that any specific physical system, such as a black hole or a quark-gluon plasma, actually has a correlator with these properties. It only states that if such a correlator exists, then reflection symmetry follows. The certificate also does not address the behavior of the two-mode spectral decomposition beyond the fundamental domain, where naive continuation can fail to be periodic. These limitations are explicit in the framework's honest accounting of its premises.

/-- **The circle triviality (THEOREM).** A correlator that is β-periodic (lives on the
Euclidean time circle) and even in the separation (identical insertions) is
reflection-symmetric about the half-period: `C(β − τ) = C(τ)` for all τ. No
thermodynamic input; this is pure circle topology + insertion identity. -/
theorem periodic_even_reflection {C : ℝ → ℝ} {beta : ℝ}
    (hper : Function.Periodic C beta) (heven : ∀ τ, C (-τ) = C τ) :
    ∀ τ, C (beta - τ) = C τ := by
  intro τ
  have hp : C (-τ + beta) = C (-τ) := hper (-τ)
  have hcomm : beta - τ = -τ + beta := by ring
  rw [hcomm, hp, heven]

/-- The `cos` witness assembled as a `SeamCorrelator`: circle topology + insertion
identity are both satisfiable by a genuinely τ-dependent correlator. -/
noncomputable def cosSeamCorrelator (beta : ℝ) (hbeta : beta ≠ 0) : SeamCorrelator beta where
  C := cosWitness beta
  periodic := cosWitness_periodic beta hbeta
  even' := cosWitness_even beta

/-- The Rung-5 certificate, fully proved. -/
theorem circleCorrelatorCert : CircleCorrelatorCert where
  reflection_forced := fun _ _ hper heven => periodic_even_reflection hper heven
  pair_from_circle := fun _ _ _ hper heven => correlatorReflection_of_circle hper heven
  witness_periodic := cosWitness_periodic
  witness_even := cosWitness_even

What this page does not claim

The certificate does not prove that any specific physical system has a correlator with the required periodicity and evenness properties. The certificate does not address the behavior of the two-mode spectral decomposition outside the fundamental domain. The certificate does not derive the value of the period β or the coupling constant κ from first principles.

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/CircleCorrelator.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: