microstate_chain_contradicts_bound
plain-language theorem explainer
Assembling the microstate reading of horizon entropy with per-pixel additivity, Schwarzschild area saturation, and the total-entropy Bekenstein bound yields a contradiction: total entropy is three times the saturated bound. Anyone citing the factor-3 keystone exclusion of the microstate reading needs this lemma. The proof unfolds the microstate cost to three, substitutes four raw bits per pixel, and finishes by linear arithmetic on N>0.
Claim. For $m,N\in\mathbb{N}$ with $N>0$ and $S,E,R\in\mathbb{R}$: if the horizon carries the microstate per-pixel multiplicity (forcing $m=3$), if total entropy is additive as $S=m\cdot N$, if the horizon area in pixel units saturates $A/4=2\pi E R$ with $A=4N$, and if the total-entropy Bekenstein bound $S\le 2\pi E R$ holds, then contradiction.
background
This module is the factor-3 keystone: a conditional exclusion of the microstate reading of horizon entropy inside a proved two-reading dichotomy (record vs microstate). The rank/nullity selector leaves one physical premise for the Bekenstein-Hawking factor $1/4$: that horizon entropy is record cost. The counterfactual microstate reading instead yields factor $3/4$, i.e. $S=3\cdot(A/4)$, machine-checked from the ledger floor (microstate cost $=3$ times record cost).
The bound hypothesis is total-entropy-typed: a static count $S$ in the same units as the area term (bits or nats), not a posted-information rate. Explicitly, TotalEntropyBekensteinBound is the open Casini-form premise $S\le 2\pi E R$, never proved here. Saturation $A/4=2\pi E R$ is a Schwarzschild model input. Per-pixel additivity over $N\ge 1$ private pixels is the other named model leg.
The local claim is structural: IF additivity, the bound, and saturation hold, THEN the microstate branch is inconsistent at every radius, with no bulk map or large-$R$ limit required.
proof idea
Tactic proof, short and algebraic. Unfold the microstate-cost hypothesis and decide to pin $m=3$. Rewrite the saturation hypothesis using the bridge fact that raw bits per pixel equal four, so the left-hand side becomes $N$ after cancelling the factor of four. Unfold the Bekenstein bound, substitute $S=3N$ and the rewritten saturation $N=2\pi E R$, cast $N>0$ to reals, and close by linarith: $3N\le N$ is impossible for positive $N$.
why it matters
This is the inconsistency half of the keystone. Its sole downstream consumer is keystone_certificate, which packages the pair: microstate chain contradicts the bound; record chain saturates it. Together they discharge the $1/4$ premise by exclusion inside the dichotomy, modulo exactly the named open legs (additivity, total-entropy Bekenstein bound, horizon saturation).
In the holography story this is Live Bet 2 structure, not unconditional physics. The factor is exactly three at every horizon radius because it is the ledger ratio of microstate cost to record cost; the violation is scale-free and survives bits-to-nats conversion. LEG-B remains open: the bound is consumed as a typed hypothesis, never asserted. The module's value is the exclusion architecture that forces the record reading once those inputs are granted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.