ClausiusForm
plain-language theorem explainer
Names the Clausius/KMS model premise: static-horizon entropy equals thermal entropy S = βE at the Euclidean period β. Horizon and holography arguments cite it as the first-law thermality input to the LEG-B bridge. It is a one-line propositional abbreviation, not a derived theorem.
Claim. The Clausius form holds for entropy $S$, energy $E$, and inverse temperature $\beta$ when $S = \beta E$. In the module this is the named model premise that static-horizon entropy is thermal entropy at the deficit-free Euclidean period $\beta$.
background
The module formalizes the LEG-B deficit-free period chain: holonomy on a U(1) carrier $h(T)=\exp(i\kappa T)$, a deficit cost $C(\delta)=1-\cos\delta$ (the J-cost chord form), and the theorem that the least positive deficit-free return time is the Euclidean period $\beta=2\pi/\kappa$.
Two named MODEL premises bridge that mathematics to horizon thermodynamics. One is the horizon-rate convention $\kappa=1/R$. The other is this Clausius form: entropy equals $\beta$ times energy at that Euclidean period. The module doc frames both as physics inputs, not as proved RS theorems; the intended derivation path is the still-open KMS-window uniqueness target.
Sibling material defines holonomy, deficit cost and its critical-point calculus, and the least-period theorem. This definition only packages the thermal identity $S=\beta E$ for use as a hypothesis.
proof idea
Definitional abbreviation: the proposition is literally the equality $S = \beta E$. No lemmas, tactics, or reduction. Downstream proofs unfold or pattern-match on it and substitute the Euclidean period $\beta=2\pi/\kappa$.
why it matters
This is the first-law/KMS thermality premise in the LEG-B physics bridge. With horizon rate $\kappa=1/R$ and Clausius form at $\beta=2\pi/\kappa$, the conditional theorem yields exact Bekenstein saturation $S=2\pi E R$, and the saturating case meets the KeystoneFactorThree total-entropy bound with equality.
It is bundled into the deficit-free-period certificate as the conditional half of the chain (the cost, zero-set, holonomy, and minimal-period fields remain unconditional theorems). Framework-wise it sits on the holography side of the eight-tick/U(1) period story, not on T5–T8 forcing itself.
Honest gap: the form is assumed, not derived here. Closing it is the open captain target on unique KMS windows; until then every Bekenstein-saturation citation from this module remains conditional on the two model premises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.