Holography Seam Cycle Carrier Holonomy Conj

The holonomy conjugation theorem

In mathematics, complex conjugation is the reflection of a complex number across the real axis: the number a + bi becomes a - bi. The theorem holonomy_conj states that for a specific one-parameter family of transformations called a holonomy (a rule that transports a value around a loop), applying the transformation for a negative amount of time is exactly the same as taking the complex conjugate of the transformation for the corresponding positive time. In symbols, the theorem proves that the conjugate of the holonomy at time t equals the holonomy at time -t.

This is a property of the standard exponential map on the unit circle. The holonomy is defined as multiplication by exp(i κ t), where κ is a positive constant and t is time. The theorem is proved by showing that the complex conjugate of exp(i κ t) is exp(-i κ t), which follows from the elementary fact that the conjugate of i is -i. The proof is a direct calculation using the additive property of the exponential function.

The statement is a theorem in the machine-checked library of formal theorems, meaning it is a proved result, not an assumption. It is one of several lemmas that establish the properties of a cycle flow, a mathematical structure representing a process that repeats exactly after a fixed period. The cycle flow is used to model the behavior of a seam correlator, a function that measures the correlation between two insertions in a physical system, and this conjugation property is a key step in showing that the correlator is symmetric under time reversal.

In Recognition Science, this theorem is part of a chain that derives the symmetry properties of a fundamental correlator from the structure of a cyclic process, rather than assuming them. The theorem itself only establishes the algebraic identity between conjugation and time reversal for this specific holonomy. It does not claim that this holonomy is the correct description of any particular physical system, nor does it prove that the correlator is symmetric; that is a separate theorem that uses this result as a lemma.

/-- Conjugation reverses the flow: `conj h(t) = h(−t)`. This is the U(1) form of the
stationarity/inversion property. -/
theorem holonomy_conj (kappa t : ℝ) :
    (starRingEnd ℂ) (holonomy kappa t) = holonomy kappa (-t) := by
  unfold DeficitFreePeriod.holonomy
  rw [← Complex.exp_conj]
  congr 1
  simp only [map_mul, Complex.conj_ofReal, Complex.conj_I]
  push_cast
  ring

What this page does not claim

The theorem does not prove that the holonomy describes any specific physical system. The theorem does not by itself establish the evenness or periodicity of the seam correlator. The theorem does not claim that complex conjugation is the only way to represent time reversal.

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: