Holography Circle Correlator Cos Witness Periodic

The cosine witness

The cosine function is the simplest periodic wave, repeating its shape every time its input advances by 2π. In the Recognition Science framework, a ledger (a discrete record of events) on a circle uses a Euclidean time coordinate τ that wraps around with period β. The declaration cosWitness_periodic proves that the function cos(2πτ/β) is indeed β-periodic: shifting τ by β leaves the value unchanged. This is a THEOREM, verified in the machine-checked library of formal theorems.

The point of this witness is to show that the framework's premises are not vacuous. The framework models a physical seam correlator, a function describing how two identical insertions on the circle relate, as being both periodic and even. Periodicity means the function lives on the circle; evenness means swapping the two identical insertions does nothing. The theorem cosWitness_periodic, together with its companion cosWitness_even, constructs a concrete function satisfying both conditions while still depending on τ. This proves the premise set is genuinely satisfiable by something that is not constant.

In Recognition Science, this witness completes a logical step. The framework proves that any periodic, even function on the circle is automatically reflection-symmetric about the half-period: C(β − τ) = C(τ). The cosine witness demonstrates this forced reflection in action, since cos(2π(β − τ)/β) equals cos(2πτ/β). The witness is the lowest non-constant harmonic on the circle, the first overtone that fits exactly once around the circumference.

What the declaration does not claim is broader significance. It does not assert that the actual physical correlator of any real system is a cosine. It only provides a mathematical example showing the framework's assumptions are consistent. It does not derive the reflection symmetry from dynamics; that symmetry is already forced by the circle topology and insertion identity alone. The cosine witness is a certificate of non-vacuity, not a physical prediction.

theorem cosWitness_periodic (beta : ℝ) (hbeta : beta ≠ 0) :
    Function.Periodic (cosWitness beta) beta := by
  intro τ
  unfold cosWitness
  have harg : 2 * Real.pi * (τ + beta) / beta = 2 * Real.pi * τ / beta + 2 * Real.pi := by
    field_simp
  rw [harg, Real.cos_add_two_pi]

theorem cosWitness_periodic (beta : ℝ) (hbeta : beta ≠ 0) :
    Function.Periodic (cosWitness beta) beta := by
  intro τ
  unfold cosWitness
  have harg : 2 * Real.pi * (τ + beta) / beta = 2 * Real.pi * τ / beta + 2 * Real.pi := by
    field_simp
  rw [harg, Real.cos_add_two_pi]

theorem cosWitness_even (beta τ : ℝ) : cosWitness beta (-τ) = cosWitness beta τ := by
  unfold cosWitness
  rw [show 2 * Real.pi * (-τ) / beta = -(2 * Real.pi * τ / beta) by ring, Real.cos_neg]

/-- **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 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 actual physical correlator of any real system is a cosine function. The reflection symmetry is derived from dynamical equations rather than from circle topology and insertion identity. The cosine witness predicts any measurable experimental outcome.

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: