Holography Circle Correlator Correlator Reflection Of Circle

Reflection from the circle

A correlator measures how two events influence each other across a separation in time. In the Euclidean formalism of quantum field theory, time is treated as an imaginary coordinate, and thermal equilibrium corresponds to curling that imaginary time into a circle of circumference β. The object of study is a function C(τ) that assigns a number to each separation τ around that circle. The question is what symmetry such a function must have, not merely what symmetries one might choose to impose.

The answer, proved in the machine-checked library of formal theorems, is that two structural properties force a third. If C is β-periodic, meaning C(τ + β) = C(τ) so it genuinely lives on the circle, and if C is even, meaning C(−τ) = C(τ) because the two insertions are identical and only their separation matters, then C is reflection-symmetric about the half-period: C(β − τ) = C(τ) for every τ. The proof is a two-line calculation: periodicity at −τ gives C(−τ + β) = C(−τ), and evenness turns that into C(τ). No thermodynamics enters; the symmetry is pure circle topology plus the insertion identity.

The declaration correlatorReflection_of_circle packages this result for a specific two-mode correlator of the form g(ω)e^−ωτ + g(−ω)e^ωτ. It states that if this pair correlator is β-periodic and even, then the reflection property that an earlier rung of the derivation ladder had treated as a model premise follows as a theorem. The physical carrier, however, is the abstract SeamCorrelator: a function with the periodicity and evenness fields built in, whose reflection symmetry is the theorem SeamCorrelator.reflection. The two-mode form is a spectral decomposition valid inside one fundamental domain, and its naive extension to all real τ is not itself periodic, which is why the honest statement lives at the abstract level.

The result is not vacuous. The cosine function C(τ) = cos(2πτ/β), the lowest harmonic on the circle, is genuinely τ-dependent, even, and β-periodic, and it satisfies the forced reflection identity. This witness shows that the premise set admits nontrivial examples. The κ → 0 limit behaves correctly: as β → ∞ the circle decompactifies, periodicity degenerates, and the reflection identity carries no content, matching flat-space expectations.

What this changes is the ledger of assumptions. A symmetry that once stood as an analytic input is now a consequence of more primitive structural facts: the correlator lives on a circle, and its two insertions are identical. The framework's derivation ladder now bottoms at periodicity, the same deficit-free period β = 2π/κ that the holonomy argument forces at the geometry layer. The reflection symmetry is not an extra postulate; it is what the circle already says.

/-- **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 reflection premise, discharged from circle premises.** If the two-mode
Euclidean correlator `pairCorrelator g ω` is β-periodic and even in τ, then the
Rung-4 premise `CorrelatorReflection g β ω` holds. (Honest scope, see the module
docstring: for the *two-mode* form periodicity is restrictive — the physical carrier
is the abstract `SeamCorrelator`, whose reflection is `SeamCorrelator.reflection`. This
corollary is the formal statement that reflection is *implied by* the circle premises,
independent of which representation carries them.) -/
theorem correlatorReflection_of_circle {g : ℝ → ℝ} {beta omega : ℝ}
    (hper : Function.Periodic (CorrelatorKMS.pairCorrelator g omega) beta)
    (heven : ∀ τ, CorrelatorKMS.pairCorrelator g omega (-τ)
        = CorrelatorKMS.pairCorrelator g omega τ) :
    CorrelatorKMS.CorrelatorReflection g beta omega :=
  periodic_even_reflection hper heven

/-- The witness is reflection-symmetric (as forced), and nontrivially so. -/
theorem cosWitness_reflection (beta : ℝ) (hbeta : beta ≠ 0) :
    ∀ τ, cosWitness beta (beta - τ) = cosWitness beta τ :=
  (cosSeamCorrelator beta hbeta).reflection

What this page does not claim

No claim that the two-mode correlator is β-periodic for all ω; the honest statement lives at the abstract SeamCorrelator level. No claim that reflection symmetry implies thermodynamics; the theorem is pure circle topology plus insertion identity. No claim that the physical carrier is the two-mode decomposition; it is the abstract periodic even 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/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: