keystone_selects_record_reading
plain-language theorem explainer
Under horizon saturation $A/4=2\pi ER$ with $A>0$, record-reading entropy $A/4$ meets the total-entropy Bekenstein bound with equality, while the microstate reading $3\cdot(A/4)$ strictly violates it. Cited by anyone discharging the RS ledger's record-cost reading of Bekenstein-Hawking $1/4$ against the microstate $3/4$ alternative. Proof is a one-line pair of the saturation and violation lemmas.
Claim. Let $A,E,R\in\mathbb{R}$ with $A>0$ and $A/4=2\pi E R$. Then the total-entropy Bekenstein bound $S\le 2\pi E R$ holds at $S=A/4$, and fails at $S=3\cdot(A/4)$.
background
This module packages the factor-3 keystone: a conditional exclusion of the microstate reading of horizon entropy. The rank/nullity selector leaves one physical premise for Bekenstein-Hawking $1/4$, namely that horizon entropy is record cost. The counterfactual microstate-cost premise yields $S=3\cdot(A/4)$ at every horizon, because the ledger floor forces microstateCost $=3=$ $3\cdot$recordCost.
The open hypothesis LEG-B is the Casini-form bound typed on total static thermodynamic entropy $S:\mathbb{R}$ in the same units as the area term (bits or nats, fixed consistently). Explicitly, TotalEntropyBekensteinBound S E R means $S\le 2\pi E R$. It must not be typed on a posted-information rate. Horizon saturation $A/4=2\pi E R$ is a model input (Schwarzschild $R=2GE$ in RS units), consumed as a hypothesis, never derived here.
Local setting: nothing in the module is unconditional physics. Value is the exclusion structure. Conditional on LEG-B, saturation, and per-pixel additivity (LEG-A), the record reading is discharged by exclusion inside the proved two-reading dichotomy.
proof idea
Term-mode pair constructor. Left conjunct is record_reading_saturates: given $A/4=2\pi E R$, the record entropy $A/4$ meets the bound with equality (rewrite saturation into $\le$). Right conjunct is microstate_reading_violates: under $A>0$ and the same saturation, $3\cdot(A/4)=3\cdot(2\pi E R)>2\pi E R$, so the microstate reading fails the bound strictly. No further algebra; the factor-3 gap is inherited from those two siblings.
why it matters
This is the keystone package named in the module doc: under saturation the two readings are separated by the bound itself (record passes with equality, microstate fails strictly). Conditional on LEG-B it is the selector discharge for HorizonEntropyIsRecordCost inside the record-versus-microstate dichotomy forced by the ledger floor.
No downstream consumers are wired yet (used_by empty); sibling certificates (keystone_certificate, record_chain_saturates_bound, microstate_chain_contradicts_bound, scale-free and unit-conversion invariance) sit beside it as the rest of Live Bet 2. Framework role is holographic: it pins why RS prefers $S=A/4$ over $S=3A/4$ without volume scaling, bulk maps, or large-$R$ limits. The open question it leaves untouched is LEG-B itself (Casini-form bound as a theorem about RS total entropy), still an explicit typed premise.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.