deficitCost_eq_zero_iff
plain-language theorem explainer
The recognition deficit cost C(δ) = 1 − cos δ vanishes if and only if the phase deficit δ lies on the lattice 2πℤ. Anyone citing the LEG-B holonomy-closure chain or the forced Euclidean period β = 2π/κ needs this exact zero-set characterization. The proof unfolds the cost to 1 − cos δ and applies the classical cosine-equals-one lattice criterion both ways.
Claim. For every real phase deficit $\delta$, the deficit cost $C(\delta) := 1 - \cos\delta$ satisfies $C(\delta) = 0$ if and only if there exists an integer $n$ such that $\delta = 2\pi n$.
background
This module formalizes the LEG-B core chain: deficit-free return periods forced by holonomy closure on a U(1) carrier. A clocked recognition cycle at rate $\kappa$ has per-cycle holonomy $h(T) = \exp(i\kappa T)$; exact return means $h(T) = 1$.
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, i.e. the J-cost quadratic form on the forced U(1) carrier. Nonnegativity $C(\delta)\ge 0$ is already proved upstream in the same module.
The classical real-analysis fact $\cos\delta = 1 \Leftrightarrow \delta\in 2\pi\mathbb{Z}$ is the only external lattice input. Geometry-side deficit notions (hinge angle sum $2\pi - \sum\theta$) share the same $2\pi$ normalization but are not invoked here; the argument is purely about the U(1) cost.
proof idea
Unfold $C(\delta)$ to $1 - \cos\delta$. Split the biconditional.
Forward: $C(\delta)=0$ rearranges by linear arithmetic to $\cos\delta = 1$. Mathlib's Real.cos_eq_one_iff supplies an integer $n$ with $\delta = 2\pi n$.
Reverse: substitute $\delta = 2\pi n$ and apply Real.cos_int_mul_two_pi to get $\cos(2\pi n) = 1$, hence $C = 0$ again by linear arithmetic.
No Recognition-specific lemmas beyond the definition of the cost are required.
why it matters
This is step 2 of the module's four-step LEG-B chain: the deficit cost vanishes exactly on the closure lattice. Downstream, deficitCost_pos_of_not_period turns the characterization into strict positivity off-lattice (accepted derive step derive_20260702_090702). holonomy_deficit_free_iff equates vanishing cost with exact holonomy return $h=1$. The headline theorem euclideanPeriod_isLeast uses the zero set to prove that for $\kappa>0$ the least positive deficit-free return time is $\beta = 2\pi/\kappa$, so $2\pi$ is forced rather than chosen.
The certificate deficitFreePeriodCert packages this zero-set fact as cost_zero_iff. In the broader Recognition framework the cost is the J-form on the U(1) carrier that the eight-tick octave embeds into (T7); the lattice forces the Euclidean period that later bridges, under named model premises, toward Bekenstein saturation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.