holonomy_eq_one_iff_lattice
plain-language theorem explainer
Exact U(1) holonomy closure h(κ,T)=exp(iκT)=1 holds if and only if the accumulated phase κT lies on the lattice 2πℤ. Holography and Bekenstein-chain arguments cite this as the lattice characterization of perfect phase return. The proof unfolds the holonomy definition and applies Complex.exp_eq_one_iff, then cancels the nonzero factor i in both directions.
Claim. For real rate $\kappa$ and duration $T$, the holonomy $h(\kappa,T):=\exp(i\kappa T)$ equals $1$ if and only if there exists an integer $n$ such that $\kappa T = 2\pi n$.
background
This module formalizes the LEG-B core chain: deficit-free return periods forced by holonomy closure on the U(1) carrier of a clocked recognition cycle. The holonomy is the per-cycle phase-return map $h(T)=\exp(i\kappa T)$ at rate $\kappa$. Exact return means the phase lands back at the identity in U(1).
The eight-tick structure embeds into this same circle: EightTick phases are $k\pi/4$ for $k=0,\ldots,7$, periodic with period $2\pi$. Downstream, the recognition deficit cost of an imperfect return is the chordal J-form $C(\delta)=1-\cos\delta=\tfrac12|1-e^{i\delta}|^2$, which vanishes exactly on the same lattice.
The present statement is the pure complex-analytic lattice criterion: $e^{i\theta}=1$ iff $\theta\in 2\pi\mathbb{Z}$, specialized to $\theta=\kappa T$. It is the first link in the module chain before deficit-cost identification and the minimal positive period $\beta=2\pi/\kappa$.
proof idea
Unfold the definition of holonomy to $\exp(i\kappa T)$. Rewrite the goal via Mathlib's Complex.exp_eq_one_iff, which states $\exp z=1$ iff $z=2\pi i, n$ for some $n\in\mathbb{Z}$.
Both directions are elementary complex arithmetic. Forward: from $i\kappa T=2\pi i, n$, cancel the nonzero factor $i$ (mul_right_cancel₀ Complex.I_ne_zero) and cast back to reals. Reverse: cast the real lattice equation into $\mathbb{C}$, multiply by $i$, and rearrange by ring to match the form required by exp_eq_one_iff. No Recognition-specific lemmas are needed beyond the holonomy definition.
why it matters
This is step 1 of the LEG-B deficit-free period chain: the holonomy carrier theorem that pins exact return to the $2\pi\mathbb{Z}$ lattice. It feeds two immediate parents in the same module. holonomy_deficit_free_iff equates vanishing deficit cost with holonomy equal to 1, by rewriting through deficitCost_eq_zero_iff and this lattice criterion. holonomy_eq_one_iff rescales (for $\kappa\neq 0$) to the canonical period lattice $T\in(2\pi/\kappa)\mathbb{Z}$, the banked legb_exp_period_lattice form.
Framework-wise it is the U(1) target into which the eight-tick octave (T7) embeds, and the reason $2\pi$ is not an external choice: it is the generator of the kernel of the exponential on the forced circle carrier. Later links extract the least positive deficit-free period $\beta=2\pi/\kappa$ and bridge (conditionally) to horizon rate and Bekenstein structure. The pure math here is fully proved; physics premises enter only downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.