DeficitFreePeriodCert
plain-language theorem explainer
Bundled Prop certificate for the LEG-B deficit-free period chain: phase-deficit cost is nonnegative with zero set exactly 2πℤ, deficit-free return equals holonomy closure, the least positive free period is 2π/κ, and under two named model premises static-horizon entropy saturates at S = 2πER. Cite it when packaging the holonomy-to-Bekenstein bridge. The structure is pure packaging; a downstream witness fills each field from prior lemmas.
Claim. A certificate is a proposition asserting five claims: (1) the deficit cost $C(\delta)\ge 0$ for all real $\delta$; (2) $C(\delta)=0$ iff $\delta=n\cdot 2\pi$ for some $n\in\mathbb{Z}$; (3) $C(\kappa T)=0$ iff the holonomy at rate $\kappa$ and time $T$ equals $1$; (4) if $\kappa>0$, the least positive $T$ with $C(\kappa T)=0$ is the Euclidean period $2\pi/\kappa$; (5) if the horizon rate premise $\kappa=1/R$ and the Clausius form $S=\beta E$ at that period both hold, then $S=2\pi E R$.
background
This module is the canonical LEG-B chain: holonomy closure forces the Euclidean period $2\pi/\kappa$, then a conditional physics bridge reaches Bekenstein saturation. Status is theorem for the mathematical spine; the entropy step carries two named model premises.
The holonomy carrier is the U(1) return map $h(T)=\exp(i\kappa T)$, exact iff $\kappa T\in 2\pi\mathbb{Z}$. The deficit cost is the chord-distance J-form $C(\delta)=1-\cos\delta=\tfrac12|1-\exp(i\delta)|^2$ on that carrier: nonnegative, zero exactly on the lattice, with a strict quadratic minimum at closure. For $\kappa>0$ the least positive free return time is $\beta=2\pi/\kappa$.
The two model premises are: horizon rate $\kappa=1/R$ (surface-gravity convention in ledger units), and Clausius form $S=\beta E$ (first-law/KMS thermality at the Euclidean period). The last certificate field is the conditional bridge that multiplies these into $S=2\pi ER$.
proof idea
No proof body: this is a structure-as-Prop, a five-field bundle. Each field is a named assertion, not a derivation.
The witness theorem constructs an instance by assigning prior results fieldwise: nonnegativity and zero-set from the deficit-cost lemmas; holonomy equivalence from the deficit-free/holonomy iff; least positive period from the Euclidean-period least-element theorem; saturation from the conditional Bekenstein bridge that consumes the two model premises. Packaging only; all mathematical work lives in those upstream lemmas.
why it matters
This is the auditable interface for the LEG-B derive captain chain (holonomy lattice, deficit cost as U(1) J-form, forced minimal period $2\pi/\kappa$, then Clausius-to-Bekenstein). Downstream, the witness theorem asserts the certificate holds by wiring those lemmas into the five fields.
In the broader Recognition framework it sits on the holographic side of the forcing story: the eight-tick octave embeds into the U(1) carrier whose unique J-cost quadratic form has smallest positive zero $2\pi$, so the period is not an input. The saturation field is the conditional physics bridge to $S=2\pi ER$; the open captain targets remain kernel-derivability of the horizon-rate premise and uniqueness of the KMS window behind Clausius form. The first four fields are unconditional; only the last is model-gated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.