deficitCost
plain-language theorem explainer
Defines the recognition cost of a phase deficit δ as C(δ) = 1 − cos δ on the real line. Anyone working the LEG-B holonomy/period chain cites this as the U(1) carrier cost whose zeros force the Euclidean period β = 2π/κ. The body is a one-line definitional assignment, not a derived identity.
Claim. For a real phase deficit $\delta$, the deficit-cost functional is $C(\delta) := 1 - \cos\delta$. Equivalently, $C(\delta) = \tfrac12\|1 - e^{i\delta}\|^2$, the squared chord distance from perfect $U(1)$ closure.
background
This module formalizes the LEG-B core chain: a clocked recognition cycle at rate $\kappa$ has holonomy $h(T) = \exp(i\kappa T)$, and exact return $h(T)=1$ holds iff $\kappa T\in 2\pi\mathbb{Z}$. The deficit cost measures imperfect return on that $U(1)$ carrier.
In Recognition Science the unique cost compatible with the Recognition Composition Law is the $J$-form $J(x)=(x+x^{-1})/2-1$. On the unit circle the quadratic form of that cost reduces to $1-\cos\delta$, i.e. half the squared chord length between $1$ and $e^{i\delta}$. Geometric "deficit" notions elsewhere in the repo (hinge angle $2\pi-\sum\theta$, ledger cell sums) are analogous bookkeeping of unmatched comparison cost; here the unmatched object is phase closure.
The local goal is to force the least positive deficit-free period $\beta=2\pi/\kappa$ from zeros and convexity of $C$, without inserting $2\pi$ by hand.
proof idea
Definitional: the body is the assignment $C(\delta)=1-\cos\delta$. No lemmas are applied. Downstream identities (nonnegativity via $\cos\le 1$, zero set via $\cos\delta=1\Leftrightarrow\delta\in 2\pi\mathbb{Z}$, derivative $\sin\delta$, and the chord-norm form) unfold this definition and invoke standard real/complex analysis.
why it matters
This is step 2 of the LEG-B chain (accepted derive derive_20260702_082715): the cost whose lattice of zeros and strict quadratic minimum at closure force the Euclidean period. Immediate consumers prove $C\ge 0$, $C(\delta)=0\Leftrightarrow\delta\in 2\pi\mathbb{Z}$, strict positivity off-lattice, $C'=\sin$, criticality at $0$ with $C''(0)=1$, the half-norm-squared identity, the certificate bundle, and that $\beta=2\pi/\kappa$ is the least positive deficit-free return time.
Framework link: $C$ is the $J$-cost quadratic form on the forced $U(1)$ carrier that the eight-tick octave embeds into (T5/T7 landmarks). The physics bridge to Bekenstein/horizon rate remains conditional on named model premises; the mathematical period extraction from this cost is theorem-grade.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.