Holography Seam Cycle Carrier Seam Cycle Carrier Cert

The cycle carrier certificate

In physics, a correlation function measures how strongly two events or insertions are related as a function of their separation. A common example is the thermal Green's function, which describes how a particle at one imaginary time relates to one at another. Two properties of such functions are frequently assumed: periodicity, meaning the function repeats after a fixed interval, and evenness, meaning it is symmetric under reversing the separation. These are often taken as axioms because they are convenient.

The declaration seamCycleCarrierCert, from the framework's machine-checked library of formal theorems, is a certificate that these two properties are not independent assumptions. It establishes that both follow from a single structural object: a cycle flow, a one-parameter translation along a closed loop that returns to its starting point after a full period. Within this structure, periodicity is a consequence of the loop closing, and evenness is a consequence of the pairing being unordered and stationary under the flow. The certificate proves these implications formally, with no gaps.

The certificate also shows that this structure is not vacuous. It provides a concrete example: a flow on the complex plane where translation is multiplication by a phase, closing at the deficit-free period. For this flow, the correlation function evaluates in closed form to a cosine, which is exactly the lowest harmonic of a Matsubara frequency. This means the cosine witness, a previously inserted by hand, emerges from the flow itself.

In Recognition Science, this certificate is Rung 6 of a premise ladder. It grounds the reflection symmetry of the seam correlator, which underpins the KMS spectral condition, the Gibbs form, and the Bekenstein bound assembly. The certificate's honest boundary is that the carrier identification itself remains a model premise: that the physical seam two-point function is indeed this pairing correlator. This is a statement about which mathematical object carries the physics, not about its symmetries.

/-- The Rung-6 certificate, fully proved. -/
theorem seamCycleCarrierCert : SeamCycleCarrierCert where
  periodicity_forced := fun _ F f x => F.observable_periodic f x
  evenness_forced := fun _ F x τ => F.correlator_even x τ
  reflection_forced := fun _ F x τ => F.reflection x τ
  jcost_even := Jcost_exp_even
  holonomy_closes := holonomy_euclideanPeriod
  witness_coherence := holonomyFlow_correlator_cosWitness

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

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

/-- A paired cycle flow: a cycle flow together with a SYMMETRIC pairing that the flow
moves through by inversion. `pair_symm` is the insertion identity (the two seam
insertions are identical, so the pair is unordered); `stationary` says translating
one insertion forward along the cycle equals translating the other backward — the
pairing sees only the separation. Inversion invariance is the carrier form of T5
reciprocity `J(x) = J(1/x)` (see `Jcost_exp_even`). -/
structure PairedCycleFlow (α : Type*) (beta : ℝ) extends CycleFlow α beta where
  /-- The seam pairing between two insertions. -/
  pair : α → α → ℝ
  /-- Insertion identity: the pair is unordered. -/
  pair_symm : ∀ x y, pair x y = pair y x
  /-- Stationarity: the flow moves through the pairing by inversion. -/
  stationary : ∀ t x y, pair (U t x) y = pair x (U (-t) y)

What this page does not claim

The certificate does not prove that the physical seam correlator is a pairing correlator of a cycle flow. The certificate does not derive the Bekenstein bound itself. The certificate does not claim that all correlation functions are even and periodic.

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: