microstate_reading_violates
plain-language theorem explainer
Under horizon saturation A/4 = 2πER with A > 0, the microstate-reading entropy 3·(A/4) strictly violates the total-entropy Bekenstein bound S ≤ 2πER. Anyone citing the factor-3 keystone exclusion of HorizonEntropyIsMicrostateCost needs this half of the dichotomy. The proof is a four-line term/tactic reduction: unfold the bound, substitute saturation, and finish by linear arithmetic.
Claim. Let $A,E,R\in\mathbb{R}$ with $A>0$ and horizon saturation $A/4=2\pi E R$. Then the microstate-reading total entropy $3\cdot(A/4)$ fails the Casini-form Bekenstein bound: it is not the case that $3\cdot(A/4)\le 2\pi E R$.
background
This module isolates a conditional exclusion structure for holographic entropy readings in Recognition Science. Two candidate readings of horizon entropy compete: the record reading $S=A/4$ and the microstate reading $S=3\cdot(A/4)$, the factor 3 coming from the ledger identity microstateCost $=3=$ $3\cdot$recordCost. The rank/nullity selector leaves one physical premise for the Bekenstein–Hawking $1/4$: HorizonEntropyIsRecordCost.
The open hypothesis LEG-B is packaged as TotalEntropyBekensteinBound: a static total thermodynamic entropy $S$ (same units as the area term; bits or nats) obeys $S\le 2\pi E R$. It is deliberately not 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 rather than derived here.
The local claim is scale-free: the microstate excess is exactly the fixed factor 3 at every radius, with no bulk-to-boundary map or large-$R$ asymptotics required.
proof idea
Unfold the bound definition to the inequality $3\cdot(A/4)\le 2\pi E R$. Rewrite the right-hand side via the saturation hypothesis, obtaining the goal $\neg\bigl(3\cdot(A/4)\le A/4\bigr)$. Introduce that inequality as a hypothesis and discharge the contradiction by linarith, using $A>0$ to get the strict factor-of-three excess. No external lemmas are required beyond the definition of the bound and elementary real arithmetic.
why it matters
This is the failing half of the keystone package. Downstream, keystone_selects_record_reading pairs it with record_reading_saturates to obtain the conjunction: under saturation the record reading meets the bound with equality while the microstate reading fails strictly. Conditional on LEG-B (and the model premises of saturation and per-pixel additivity), that conjunction discharges HorizonEntropyIsRecordCost by exclusion inside the proved two-reading dichotomy.
The module status is explicitly conditional: LEG-B remains open and is never asserted. The value is the exclusion structure itself, panel-greenlit as Live Bet 2. Related siblings (violation_is_scale_free, violation_survives_unit_conversion) confirm the factor-3 gap is invariant under radius and under bits↔nats conversion, so unit choice cannot rescue the microstate reading.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.