deficitCost_nonneg
plain-language theorem explainer
The phase-deficit recognition cost C(δ) = 1 − cos δ is nonnegative for every real deficit δ. Anyone citing the LEG-B holonomy chain or the deficit-free period certificate needs this as the base inequality before zero-set and strict-positivity lemmas. The proof unfolds the definition and applies cos δ ≤ 1 via linear arithmetic.
Claim. For every real phase deficit $\delta$, the deficit cost $C(\delta) := 1 - \cos\delta$ satisfies $C(\delta) \ge 0$.
background
This module formalizes the LEG-B core chain: holonomy closure on a clocked recognition cycle forces the minimal positive deficit-free period $2\pi/\kappa$. The per-cycle phase-return map is $h(T) = \exp(i\kappa T)$, exact return iff $\kappa T \in 2\pi\mathbb{Z}$.
The deficit-cost functional measures imperfect return. For phase deficit $\delta$ one sets $C(\delta) = 1 - \cos\delta$, equivalently $\tfrac12|1 - \exp(i\delta)|^2$: the squared chord distance from the returned phase to perfect closure. Module text identifies this as the J-cost quadratic form on the forced U(1) carrier (the same nonnegative cost shape that appears as recognition cost of events and ratio comparators upstream).
Nonnegativity is the first structural fact about $C$ before characterizing its zero set, strict positivity off the lattice, and the quadratic minimum at closure.
proof idea
One-step tactic proof. Unfold $C(\delta) = 1 - \cos\delta$, then apply linarith with the standard bound $\cos\delta \le 1$ (Real.cos_le_one). No further lemmas are required.
why it matters
Base inequality of the deficit-cost block in the LEG-B derive chain (accepted steps derive_20260702_*). Downstream, deficitCost_pos_of_not_period splits on this nonnegativity plus the zero-set characterization to get strict positivity off $2\pi\mathbb{Z}$. The package certificate deficitFreePeriodCert records cost_nonneg := deficitCost_nonneg as a field, feeding the minimal-period theorem $\beta = 2\pi/\kappa$ and the conditional Bekenstein saturation bridge.
In framework terms this is the U(1) instance of J-cost nonnegativity on the holonomy carrier that the eight-tick clock embeds into (T7 octave / period lattice). It does not itself force $\phi$ or $D=3$; it locks the cost geometry that makes $2\pi$ the least positive zero rather than an input constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.