holonomy
plain-language theorem explainer
The per-cycle holonomy is the U(1) phase-return map $h(\kappa,T)=e^{i\kappa T}$ for a clocked recognition cycle at rate $\kappa$ over duration $T$. Anyone citing the LEG-B deficit-free period chain, eight-tick circle embedding, or the cost of imperfect phase closure uses this carrier. The body is a one-line complex exponential; no proof content beyond the definition.
Claim. For real rate $\kappa$ and real duration $T$, the per-cycle holonomy is the complex number $h(\kappa,T) := \exp(i\kappa T) \in \mathbb{C}$.
background
This module formalizes the LEG-B core chain: deficit-free period forced by holonomy closure. The setting is a clocked recognition cycle whose phase lives on the circle. The eight-tick foundation supplies discrete phases $k\pi/4$ for $k=0,\ldots,7$, which embed into U(1); the continuous per-cycle return target is this exponential map.
Upstream, recognition cost is the J-cost on ratios (observer forcing, multiplicative recognizer), and evolution operators are matrix exponentials of generators. Here the analogous object is scalar: a pure U(1) phase factor rather than a full Hamiltonian step. RS-native units fix $c=1$ and a unit tick, so $\kappa$ and $T$ are already in the calibrated clock.
The next sibling objects build the deficit-cost $C(\delta)=1-\cos\delta$ of imperfect return and prove that the least positive deficit-free period is $\beta=2\pi/\kappa$.
proof idea
Pure definition: evaluate the complex exponential $\mathrm{Complex.exp}(\kappa\cdot T\cdot i)$. No lemmas, no tactics, no hypotheses. Downstream theorems (lattice characterization of exact return, deficit-cost identities) unpack the analytic consequences of this formula.
why it matters
This is step 1 of the LEG-B chain in the module doc: the holonomy carrier that the eight-tick clock embeds into, tied to accepted derive step derive_20260702_065112. Exact return $h=1$ iff $\kappa T\in 2\pi\mathbb{Z}$ is proved next; the deficit cost is the J-form quadratic on this U(1) carrier; the minimal positive zero forces Euclidean period $2\pi/\kappa$.
Downstream uses include normalized bit cost in the $\lambda_{\mathrm{rec}}$ derivation, flat-interior holonomy-triviality on simplices (identity holonomy when the interior is flat), and Regge/Bianchi gravity scaffolding where deficit angles are the geometric cousins of phase deficit. Framework landmarks: T7 eight-tick octave as the discrete source of the circle period, and the unique J-cost (T5) as the quadratic form measuring failure of $h=1$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.