deficitCost_second_deriv_pos_at_zero
plain-language theorem explainer
At phase deficit zero, sine (the first derivative of the deficit cost C(δ)=1−cos δ) has slope 1. Anyone citing the strict quadratic minimum of recognition deficit cost at holonomy closure needs this local-convexity fact. The proof is a one-line appeal to the standard derivative of sine at the origin, recording C''(0)=cos 0=1>0.
Claim. The real sine function satisfies $\mathrm{HasDerivAt}(\sin,1,0)$, i.e. $\frac{d}{dx}\sin x\big|_{x=0}=1$. In the deficit-cost chain this is the statement that $C''(0)=\cos 0=1>0$ for $C(\delta)=1-\cos\delta$.
background
This module formalizes the LEG-B core chain: holonomy closure forces a deficit-free Euclidean period. The per-cycle phase-return map at rate $\kappa$ is $h(T)=\exp(i\kappa T)$, and exact return $h(T)=1$ holds iff $\kappa T\in 2\pi\mathbb{Z}$.
The recognition cost of an imperfect return with phase deficit $\delta$ is the deficit-cost functional $C(\delta)=1-\cos\delta=\tfrac12|1-\exp(i\delta)|^2$: the squared chord distance to perfect U(1) closure, i.e. the J-cost quadratic form on the carrier. Sibling results already show $C\ge 0$, $C=0$ exactly on $2\pi\mathbb{Z}$, and that $C$ is differentiable with a critical point at $\delta=0$ (first derivative $\sin$ vanishes there).
The present claim supplies the missing second-derivative sign: the slope of $\sin$ at $0$ is $1$, so $C''(0)=\cos 0=1>0$. That is the accepted derive step for local convexity at closure.
proof idea
One-line wrapper. Apply the Mathlib fact Real.hasDerivAt_sin at argument $0$, which states that sine has derivative $\cos 0=1$ at the origin; simpa aligns the goal HasDerivAt Real.sin 1 0 with that lemma. No deficit-cost unfolding is needed: the chain treats the first derivative of $C$ as $\sin$, so positivity of $C''(0)$ is exactly this slope statement.
why it matters
Closes the local-convexity leg of the deficit-cost package in the LEG-B derive captain chain (accepted step derive_20260702_090702: $C''(0)=1$). Together with nonnegativity, lattice zeros, and the critical-point fact at zero, it certifies that holonomy closure is a strict quadratic minimum of the recognition cost on the U(1) carrier.
That minimum underwrites the minimal positive deficit-free period $\beta=2\pi/\kappa$: $2\pi$ is not inserted by hand but is the smallest positive zero of the unique J-form cost on the forced circle. The same carrier is the U(1) target into which the eight-tick clock embeds (T7 octave landmark; discrete subperiod exclusion lives nearby). No downstream Lean users are wired yet (used_by empty); the consumer is the module's own least-period theorem and the conditional physics bridge (HorizonRate / Clausius) that sits on top of the mathematical chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.