Encyclopedia Holography Holography Seam Cycle Carrier Holonomy Flow Correlator

ARTICLE 2 claims 2 theorems

Holography Seam Cycle Carrier Holonomy Flow Correlator

A machine-checked proof derives the simplest possible correlation function for a cyclic process, and shows it is a cosine.

The closed-form correlator

A correlation function measures how strongly two events are related when separated by a certain time. In many physical settings, this function is a decaying exponential. The Recognition Science declaration holonomyFlow_correlator establishes that for a specific, forced cyclic process, the correlation function is not an exponential but a pure cosine: C(τ) = |z|² · cos(κτ). Here τ is the time separation, κ is a frequency, and z is a complex number encoding the state's amplitude.

The declaration is a theorem in the framework's machine-checked library of formal theorems. It proves this formula for a particular mathematical structure called a holonomy flow, which is a way of transporting a state around a closed cycle. The key point is that the cosine emerges from the structure itself, not from an assumption. The flow is defined by U(t)z = exp(iκt)·z, a rotation on the complex plane. The correlation function is then defined as the real part of the product of the state with its complex conjugate after time τ. The theorem computes this directly, using the group law of the flow and the properties of complex exponentials.

This result is significant because it shows that the lowest-frequency harmonic, the cosine, is not inserted by hand. It is a consequence of the cycle closing on itself. The period of the flow, β = 2π/κ, is the time for one full rotation. The theorem also proves a coherence check: when the state has unit magnitude (|z| = 1), the correlator exactly matches a previously defined witness function, confirming the internal consistency of the framework.

The declaration does not claim that this specific cosine correlator is the universal form for all physical systems. It applies to the specific U(1) holonomy flow. The deeper physical premise, that the real-world seam correlator is this mathematical pairing, remains a model choice, not a theorem. The framework proves the symmetry properties of any such flow, but identifying which flow describes nature is a separate step.

THEOREM holonomyFlow_correlator · IndisputableMonolith/Holography/SeamCycleCarrier.lean
/-- **Closed form of the holonomy correlator: `C(τ) = ‖z‖²·cos(κτ)`.** The lowest
Matsubara harmonic emerges from the flow. -/
theorem holonomyFlow_correlator (kappa : ℝ) (hk : 0 < kappa) (z : ℂ) (τ : ℝ) :
    (holonomyFlow kappa hk).correlator z τ
      = Complex.normSq z * Real.cos (kappa * τ) := by
  show (z * (starRingEnd ℂ) (holonomy kappa τ * z)).re = _
  have hmain : z * (starRingEnd ℂ) (holonomy kappa τ * z)
      = (starRingEnd ℂ) (holonomy kappa τ) * (z * (starRingEnd ℂ) z) := by
    rw [map_mul]; ring
  rw [hmain, Complex.mul_conj, holonomy_conj]
  simp only [Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, sub_zero]
  rw [holonomy_re, mul_neg, Real.cos_neg]
  ring
THEOREM holonomyFlow_correlator_cosWitness · IndisputableMonolith/Holography/SeamCycleCarrier.lean
holonomyFlow_correlator_cosWitness · IndisputableMonolith/Holography/SeamCycleCarrier.lean:285
/-- **Coherence with the Rung-5 witness.** At a unit insertion the holonomy-flow
correlator IS the Rung-5 `cosWitness` at the deficit-free period: the witness was
not ad hoc — it is what the forced carrier produces. -/
theorem holonomyFlow_correlator_cosWitness (kappa : ℝ) (hk : 0 < kappa) (τ : ℝ) :
    (holonomyFlow kappa hk).correlator 1 τ
      = CircleCorrelator.cosWitness (euclideanPeriod kappa) τ := by
  rw [holonomyFlow_correlator]
  unfold CircleCorrelator.cosWitness euclideanPeriod
  rw [Complex.normSq_one, one_mul]
  congr 1
  have hpi : Real.pi ≠ 0 := Real.pi_ne_zero
  have hkne : kappa ≠ 0 := ne_of_gt hk
  field_simp

What this page does not claim

The declaration does not prove that the physical seam correlator is this cosine function. The declaration does not establish the cosine form for any flow other than the specific U(1) holonomy flow. The declaration does not derive the Bekenstein bound; it only grounds a symmetry premise used in that larger argument.

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

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND