Holography Circle Correlator Cos Witness Reflection

The cosine witness

The cosine function cos(2πτ/β) is the simplest nontrivial example of a function on a circle of circumference β. It repeats every β, so it lives naturally on the circle, and it is even: cos(−θ) = cos(θ), so it treats the two directions around the circle the same way. The Recognition Science declaration cosWitness_reflection establishes that this cosine also has a third property: it is symmetric about the halfway point, meaning cos(2π(β−τ)/β) = cos(2πτ/β). This is not a new assumption; it follows from the periodicity and evenness already present.

The general principle at work is a theorem in the framework's machine-checked library of formal theorems. If any function on the real line is β-periodic and even, then it is automatically reflection-symmetric about the half-period: C(β−τ) = C(τ) for every τ. The proof is a short algebraic step: periodicity lets you shift the argument by β, and evenness lets you flip its sign. No thermodynamic input, no dynamics, no additional physics enters. The cosine witness shows the premise set is not empty: a genuinely τ-dependent function satisfies both conditions, so the theorem is not about a trivial constant function.

In the framework's account, this matters because a reflection symmetry that earlier work treated as a separate assumption can instead be derived from more primitive facts. The cosine witness is the concrete demonstration that those primitive facts are consistent and non-vacuous. The declaration itself, however, claims nothing about the physical correlator of any specific theory. It establishes a property of one particular cosine function, not a statement about quantum fields, black holes, or thermodynamics. Those connections live in other declarations that build on this one.

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

The declaration does not claim anything about the physical correlator of any specific quantum field theory. It does not establish that any actual thermal system satisfies the periodicity and evenness premises. It does not derive the reflection symmetry from thermodynamics or from any dynamical law.

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: