Sending a primitive p^nth root of unity to a primitive p^nth root of unity gives an isomorphism \chi_n : \Gal(F_n/\Q) \xrightarrow{\sim} (\Z/p^n\Z)^{\times}, characterised by \sigma(\xi) = \xi^{\chi_n(\sigma)} for any \xi \in \mu_{p^n}. Taking the inverse limit yields the cyclotomic character \chi := \varprojlim_n \chi_n : \GCal := \Gal(F_\infty/\Q) \xrightarrow{\sim} \Zpx, an isomorphism of profinite groups, where F_\infty := \Q(\mu_{p^\infty}). It induces \GCal^+ := \Gal(F_\infty^+/\Q) \cong \Zpx/\{\pm 1\}.

We fix once and for all a compatible system of roots of unity (\xi_{p^n})_{n \in \N}: each \xi_{p^n} is a primitive p^nth root of unity with \xi_{p^{n+1}}^p = \xi_{p^n}. Put \pi_n := \xi_{p^n} - 1, a uniformiser of K_n. The infinite-level local units are \sU_\infty := \varprojlim_n \sU_n, the inverse limit taken with respect to the norm maps N_{n,n-1} : K_n \to K_{n-1}. Together with its norm-1 submodule \sU_{\infty,1} := \varprojlim_n \sU_{n,1} (where \sU_{n,1} = \{u \in \sU_n : u \equiv 1 \pmod{\mathfrak p_n}\}) it is a compact \Zp-module carrying a continuous action of \GCal, hence of the Iwasawa algebra \Lam(\GCal). This Definition 9.1.1 \GCal-action is the main reason for passing to infinite level.

In the formalisation the tower lives inside ℂ_[p] (matching the B(0,1)-framing below): the compatible system is zetaSys (built by recursion from algebraic closedness), K n is the intermediate field ℚ_p(ξ_{p^n}) with [K n : ℚ_p] = φ(p^n) proved by an Eisenstein argument, O n its norm-unit-ball, levelNorm the relative norm N_{n+1,n} (with the collapse N(ξ^b_{p^{n+1}} − 1) = ξ^b_{p^n} − 1), and 𝒰_∞ is the structure NormCompatUnits of norm-compatible unit families. The 𝒢-action and 𝒰_{∞,1} are deferred to the §11 pass (plan.md); the cyclotomic-character node above stays prose for the same reason.