deficitFreePeriodCert
plain-language theorem explainer
Bundled certificate that the deficit-cost chain is complete: nonnegative cost vanishing exactly on 2πℤ, deficit-free return identical to U(1) holonomy closure, least positive period β = 2π/κ, and (under two named model premises) static-horizon entropy saturating at S = 2πER. Anyone citing the LEG-B holography derive would point here. Proof is a pure structure assembly of five already-proved component lemmas.
Claim. There exists a certificate packing five facts: (i) the deficit cost $C(\delta)=1-\cos\delta$ satisfies $C(\delta)\ge 0$ for all real $\delta$; (ii) $C(\delta)=0$ if and only if $\delta\in 2\pi\mathbb{Z}$; (iii) $C(\kappa T)=0$ if and only if the holonomy $h(\kappa,T)=e^{i\kappa T}$ equals $1$; (iv) for every $\kappa>0$, the least positive $T$ with $C(\kappa T)=0$ is the Euclidean period $\beta=2\pi/\kappa$; (v) if the horizon rate is $\kappa=1/R$ and the Clausius form $S=\beta E$ holds at that period, then $S=2\pi E R$.
background
This module is the canonical LEG-B core chain: holonomy closure forces the Euclidean period $2\pi/\kappa$, which then bridges (conditionally) to Bekenstein saturation. The carrier is the U(1) phase-return map $h(T)=\exp(i\kappa T)$ of a clocked recognition cycle; exact return holds precisely when $\kappa T\in 2\pi\mathbb{Z}$.
The deficit cost $C(\delta)=1-\cos\delta=\tfrac12|1-e^{i\delta}|^2$ is the squared chord distance from perfect closure, i.e. the J-cost quadratic form on that carrier. It is nonnegative, vanishes exactly on the lattice $2\pi\mathbb{Z}$, and has a strict quadratic minimum at closure. For $\kappa>0$ the positive zero set of $C(\kappa T)$ therefore has least element $\beta=2\pi/\kappa$ (the Euclidean period).
The physics bridge is conditional on two named model premises: HorizonRate ($\kappa=1/R$ at a static horizon of radius $R$) and ClausiusForm ($S=\beta E$ evaluated at the deficit-free period). Under those, entropy saturates at the Bekenstein/Casini value $S=2\pi ER$.
proof idea
Term-mode structure inhabitation: each field of DeficitFreePeriodCert is discharged by the corresponding already-proved lemma.
cost_nonneg←deficitCost_nonneg(nonnegativity of $1-\cos\delta$ via $\cos\le 1$).cost_zero_iff←deficitCost_eq_zero_iff(zero set exactly $2\pi\mathbb{Z}$).holonomy_iff←holonomy_deficit_free_iff(deficit-free return iff holonomy equals 1).minimal_period←euclideanPeriod_isLeast(least positive zero is $2\pi/\kappa$).saturation←bekenstein_saturation_from_deficit_free_period(conditional bridge under HorizonRate and ClausiusForm).
No new algebra is performed; the certificate is the packaging.
why it matters
This is the single auditable landing point for the LEG-B derive captain's accepted chain (journal entries derive_20260702_*, all ACCEPT): holonomy carrier, deficit-cost functional, minimal positive period, and the conditional Clausius-to-Bekenstein bridge, promoted from banked scratch leaves into one Prop.
In the Recognition framework it sits on the holography side of the forcing story. The period $2\pi/\kappa$ is not postulated; it is the least positive zero of the unique J-form on the forced U(1) carrier, tying the eight-tick octave embedding into the continuous circle. The saturation field is the place where the static-horizon entropy hits $S=2\pi ER$, the saturating Bekenstein/Casini bound under the two named model premises.
No downstream consumers are wired yet (used_by is empty); the certificate is the export surface for later holography and thermodynamics modules that need the full LEG-B package in one hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.