TotalEntropyBekensteinBound
plain-language theorem explainer
Defines the Casini-form Bekenstein bound as a typed proposition: total static thermodynamic horizon entropy S satisfies S ≤ 2πER. Cited throughout the Factor-3 Keystone as LEG-B, the open physical premise that separates record from microstate horizon readings. Pure definition of a Prop; no proof content.
Claim. The predicate $\mathrm{TotalEntropyBekensteinBound}(S,E,R)$ holds if and only if the total static thermodynamic entropy $S$ obeys the Bekenstein inequality $S \le 2\pi E R$, for energy $E$ and radius $R$ (same units on both sides: bits or nats, fixed consistently).
background
In the Factor-3 Keystone module the rank/nullity selector leaves two candidate readings of horizon entropy: record cost (yielding the Bekenstein–Hawking $1/4$) and microstate cost (yielding $3/4$, i.e. a fixed factor-3 excess). The module’s exclusion structure is conditional on three named inputs: per-pixel additivity (LEG-A), this total-entropy Bekenstein bound (LEG-B), and Schwarzschild saturation $A/4 = 2\pi ER$.
LEG-B is deliberately typed on a static count $S:\mathbb{R}$ in the same units as the area term (candidates C3/C6 of the entropy audit: bits, or nats via $\ln 2$). It must not be confused with the posted-information rate accessibleInfo (nats per tick), which has the wrong type. The module doc states the bound as an OPEN hypothesis: a premise consumed downstream, never asserted as a theorem about RS total entropy.
Upstream entropy and area scaffolding (configuration defect entropy, horizon area ledgers, saturation fractions) supply the ambient language; none of those objects prove the inequality itself.
proof idea
Definitional wrapper only. The body is the single inequality $S \le 2\pi E R$ packaged as a Prop on three real parameters. No tactics, no lemmas, no reduction.
why it matters
This is the typed LEG-B hinge of Live Bet 2. Downstream, record_reading_saturates shows $A/4$ meets the bound with equality under horizon saturation; microstate_reading_violates shows $3\cdot(A/4)$ strictly exceeds it at every radius. Those two facts assemble into keystone_selects_record_reading, the chain-level contradictions microstate_chain_contradicts_bound / record_chain_saturates_bound, and the package certificate keystone_certificate, which discharges HorizonEntropyIsRecordCost by exclusion inside the proved two-reading dichotomy—modulo LEG-A, LEG-B, and saturation only.
A sibling use in DeficitFreePeriod.totalEntropyBound_saturating_case checks that a Clausius saturating thermal state meets this same bound form (honestly scoped: not a general proof of LEG-B). Within Recognition Science holography this is the panel-demanded total-entropy typing of the Casini-form bound; the factor-3 violation is scale-free and unit-conversion invariant, so neither large-$R$ limits nor bits↔nats rescue the microstate reading. LEG-B itself remains OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.