totalEntropyBound_saturating_case
plain-language theorem explainer
Under horizon rate κ = 1/R and Clausius thermality S = βE at the Euclidean period β = 2π/κ, the static-horizon entropy saturates the Keystone Factor Three Bekenstein form as S = 2πER. Cite this for the LEG-B holography bridge and the deficit-free-period certificate. Proof: apply the saturation lemma, unfold the bound predicate, close by linear arithmetic.
Claim. Let $S,E,R,\kappa\in\mathbb{R}$ with $R>0$. Assume the horizon-rate premise $\kappa=1/R$ and the Clausius form $S=\beta E$ at the Euclidean period $\beta=2\pi/\kappa$. Then the Keystone Factor Three total-entropy Bekenstein bound holds for $(S,E,R)$ (with equality $S=2\pi ER$).
background
This module formalizes the LEG-B core chain: holonomy closure on the U(1) carrier forces a unique minimal positive deficit-free period. The per-cycle return map is $h(T)=\exp(i\kappa T)$; exact return holds iff $\kappa T\in 2\pi\mathbb{Z}$. The deficit cost $C(\delta)=1-\cos\delta=\tfrac12|1-e^{i\delta}|^2$ is the chord-distance J-form on that carrier: nonnegative, zero exactly on $2\pi\mathbb{Z}$, with a strict quadratic minimum at closure. For $\kappa>0$ the least positive zero of $C(\kappa T)$ is the Euclidean period $\beta=2\pi/\kappa$.
Two named MODEL premises bridge math to static-horizon thermodynamics. Horizon rate asserts $\kappa=1/R$ (surface-gravity convention in ledger units). Clausius form asserts thermal entropy $S=\beta E$ at that Euclidean period (first-law/KMS input). Under both, the chain targets saturation $S=2\pi ER$.
The Keystone Factor Three total-entropy Bekenstein bound is the inequality form that this saturating state is asked to meet. The doc-comment stresses honest scope: only the Clausius state is treated here.
proof idea
Term-mode, three steps. First obtain equality $S=2\pi ER$ from bekenstein_saturation_from_deficit_free_period, feeding positivity of $R$, the horizon-rate premise, and Clausius form at euclideanPeriod kappa. That upstream lemma multiplies $S=\beta E$ by $\beta=2\pi/\kappa$ and substitutes $\kappa=1/R$. Next unfold KeystoneFactorThree.TotalEntropyBekensteinBound to expose the inequality predicate on $(S,E,R)$. Finally linarith turns the equality into the required bound.
why it matters
Closes the physics-bridge leg of the deficit-free-period certificate: after unconditional theorems on holonomy, deficit cost, and minimal period $2\pi/\kappa$, this shows the Clausius state meets the Keystone Factor Three Bekenstein form with equality $S=2\pi ER$. It lands the derive-captain steps banked under rs-bekenstein-legb-loop (accepted journal entries on the Clausius-to-Bekenstein bridge).
Framework contact: the deficit cost is the J-cost quadratic on the forced U(1) carrier; the $2\pi$ period is not inserted by hand but is the least positive zero of that cost, tying the eight-tick octave embedding into the circle. No downstream Lean users yet (used_by empty); the consumer is the bundled certificate and any later LEG-B assembly.
Open remainder (explicit in the doc-comment): this is saturation for the Clausius state only, not the general Bekenstein bound for arbitrary states. LEG-B proper and the KMS-window uniqueness target remain open with the derive captain. Horizon rate itself is still a named model premise (Live Bet 2 on kernel-derivability).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.