deficitCost_hasDerivAt
plain-language theorem explainer
The deficit cost C(δ)=1−cos δ is differentiable on ℝ with derivative sin δ. Anyone citing the LEG-B holonomy-closure chain (quadratic minimum at perfect return) needs this derivative identity. The proof is a one-line Mathlib reduction: subtract the constant 1 from the cosine derivative and unfold the definition of C.
Claim. For every real phase deficit $\delta$, the deficit-cost map $C(\delta)=1-\cos\delta$ is differentiable at $\delta$ with derivative $\sin\delta$: $\frac{d}{d\delta}C(\delta)=\sin\delta$.
background
This module formalizes the LEG-B core chain: holonomy closure on a U(1) carrier forces the Euclidean period $2\pi/\kappa$. The per-cycle return map is $h(T)=\exp(i\kappa T)$; exact return means $\kappa T\in 2\pi\mathbb{Z}$.
The deficit cost $C(\delta)=1-\cos\delta$ is the recognition cost of an imperfect return with phase deficit $\delta$. Module text identifies it with the squared chord $\tfrac12|1-\exp(i\delta)|^2$, i.e. the J-cost quadratic form on the U(1) carrier. Sibling lemmas already record nonnegativity, vanishing exactly on $2\pi\mathbb{Z}$, and strict positivity off the lattice.
Differentiability of $C$ is the analytic step that turns those algebraic facts into a strict local minimum at closure, which later pins the least positive deficit-free period.
proof idea
Term-mode, essentially a one-line wrapper. Start from Mathlib's Real.hasDerivAt_cos δ (derivative of $\cos$ at $\delta$ is $-\sin\delta$). Apply HasDerivAt.const_sub with constant $1$ to obtain the derivative of $1-\cos$ at $\delta$, which is $\sin\delta$. Then simpa [deficitCost] rewrites the goal through the definition $C(\delta)=1-\cos\delta$.
why it matters
This is step 2 of the LEG-B chain in the module doc: the deficit-cost functional has a strict quadratic minimum at closure. The sole downstream consumer is deficitCost_critical_at_zero, which specializes to $\delta=0$ and gets derivative $0$, so closure is a critical point. The next sibling then shows the second derivative is $\cos 0=1>0$ (accepted derive step derive_20260702_090702).
Together these feed the least-element theorem for positive deficit-free return times: for $\kappa>0$, $\beta=2\pi/\kappa$ is the minimal $T>0$ with $C(\kappa T)=0$. In the broader Recognition picture this is the continuous U(1) target that the eight-tick octave embeds into; $2\pi$ is not postulated but is the smallest positive zero of the unique J-form on that carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.