holonomy_eq_one_iff
plain-language theorem explainer
Exact phase return of the clocked holonomy exp(i κ T) holds precisely when T lies on the lattice (2π/κ)ℤ, for any nonzero rate κ. LEG-B / holography workers cite this as the canonical both-directions form of the banked period lattice. The proof rewrites through the κT ∈ 2πℤ characterization and finishes by real-field rearrangement under κ ≠ 0.
Claim. For real $\kappa \neq 0$ and real $T$, one has $\exp(i\kappa T) = 1$ if and only if there exists an integer $n$ such that $T = n\cdot(2\pi/\kappa)$.
background
The Deficit-Free Period module formalizes the LEG-B core chain: holonomy carrier, deficit-cost functional, and minimal positive deficit-free return time. A clocked recognition cycle at rate $\kappa$ has per-cycle phase-return map $h(T)=\exp(i\kappa T)$ on the forced U(1) carrier. Exact return means $h(T)=1$.
The sibling lattice form states that holonomy equals 1 iff $\kappa T\in 2\pi\mathbb{Z}$. That is the covering-space winding characterization. The present statement rewrites the same zeros as $T\in(2\pi/\kappa)\mathbb{Z}$, the form needed when one solves for return times at fixed nonzero rate.
Deficit cost on a phase deficit $\delta$ is $C(\delta)=1-\cos\delta=\tfrac12|1-e^{i\delta}|^2$, the J-cost quadratic form on U(1). It vanishes exactly on $2\pi\mathbb{Z}$. The module promotes banked scratch leaves (period lattice, Clausius-to-Bekenstein, eight-tick circle period) into one auditable chain; physics bridging to horizons remains conditional on two named model premises.
proof idea
One-line rewrite through the lattice form (holonomy equals 1 iff $\kappa T\in 2\pi\mathbb{Z}$). Both directions are pure real arithmetic under $\kappa\neq 0$.
Forward: from $\kappa T=2\pi n$, multiply/divide to obtain $T=n(2\pi/\kappa)$ via eq_div_of_mul_eq and mul_div_assoc (linarith supplies the intermediate product identity). Converse: substitute $T=n(2\pi/\kappa)$ and clear the denominator with field_simp. No analysis beyond the lattice characterization is used.
why it matters
Step 1 of the LEG-B deficit-free period chain: the holonomy carrier in the return-time presentation. The module doc identifies this U(1) target as what the eight-tick clock embeds into (legb_eight_tick_circle_period; discrete subperiod exclusion is separate). Same-module siblings on deficit cost (nonnegativity, zeros exactly on $2\pi\mathbb{Z}$, strict quadratic minimum at closure) and the headline least positive period $\beta=2\pi/\kappa$ rest on knowing the exact zeros are this lattice.
Framework landmarks: T5 J-uniqueness supplies the cost form $1-\cos\delta$ on the carrier; T7 eight-tick octave is the discrete clock that embeds here. 2π is not chosen by hand: it is the smallest positive zero of that forced cost. No external used_by edges yet; the declaration lands the banked legb_exp_period_lattice leaf into the canonical auditable chain toward the conditional holography/Bekenstein bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.