deficitCost_critical_at_zero

In the Deficit-Free Period module (LEG-B core chain), a clocked recognition cycle at rate $\kappa$ has holonomy $h(T)=\exp(i\kappa T)$. Exact return holds iff $\kappa T\in 2\pi\mathbb{Z}$. Off the lattice the phase deficit $\delta$ carries recognition cost $C(\delta)=1-\cos\delta$, equal to half the squared chord length between the returned phase and perfect closure: the J-cost quadratic form on the forced U(1) carrier.

Module facts already record that $C$ is nonnegative, vanishes exactly on $2\pi\mathbb{Z}$, and is strictly positive off that lattice. The local-minimum package needs two calculus facts at closure: a critical point ($C'(0)=0$) and positive second derivative ($C''(0)=\cos 0=1$). This declaration is the critical-point half. Upstream cost constructions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsen totals) supply the broader meaning of "recognition cost"; here the carrier is specialized to the circle holonomy.

One-line wrapper. A sibling derivative lemma already shows that $C$ has derivative $\sin\delta$ at every real $\delta$ (because $\frac{d}{d\delta}(1-\cos\delta)=\sin\delta$). Instantiate that lemma at $\delta=0$ and simplify with $\sin 0=0$ to obtain $\mathrm{HasDerivAt},C,0,0$. No fresh differentiation is performed here.

Fills the critical-point step in the LEG-B chain that forces the Euclidean period $\beta=2\pi/\kappa$ from holonomy closure rather than by postulate. With nonnegativity, the exact zero set on $2\pi\mathbb{Z}$, and the companion second-derivative positivity at zero, it shows closure is a strict quadratic minimum of the deficit cost (accepted derive step derive_20260702_090702: local convexity $C''(0)=1$).

That minimum package underwrites the least-positive-period theorem: for $\kappa>0$, the set ${T>0:C(\kappa T)=0}$ has least element $2\pi/\kappa$. In Recognition landmarks this is the continuous U(1) target into which the eight-tick octave (T7) embeds; $2\pi$ is the smallest positive zero of the unique J-form on that carrier, not an input. No Lean dependents are recorded yet. The physics bridge onward to Bekenstein remains conditional on two named HorizonRate model premises outside this pure calculus fact.