keystone_certificate
plain-language theorem explainer
Conditional on per-pixel additivity, the total-entropy Bekenstein bound, and horizon saturation A/4 = 2πER, the microstate reading of horizon entropy is inconsistent while the record reading saturates the bound. Anyone citing the factor-3 keystone or the discharge of HorizonEntropyIsRecordCost by exclusion within the two-reading dichotomy needs this certificate. The proof is a one-line pair of the two chain lemmas already proved in-module.
Claim. For all natural $m,N$ and reals $S,E,R$: if $N>0$, the horizon carries microstate cost $m$, $S=mN$, the pixel-area saturation $(\mathrm{rawBits}\cdot N)/4=2\pi E R$ holds, and the total-entropy Bekenstein bound $S\le 2\pi E R$ holds, then contradiction. And for all such $m,N,S,E,R$: if the horizon carries record cost $m$, $S=mN$, and the same saturation holds, then $S\le 2\pi E R$.
background
This module isolates the factor-3 keystone of Recognition holography. The rank/nullity selector leaves one physical premise for the Bekenstein–Hawking $1/4$: that horizon entropy is record cost (per-pixel multiplicity $m=1$), not microstate cost ($m=3$). The counterfactual microstate reading yields $S=3\cdot(A/4)$ at every horizon radius, machine-checked from the ledger floor.
TotalEntropyBekensteinBound S E R is the open LEG-B premise: $S\le 2\pi E R$ on a static total entropy in the same units as the area term (bits or nats), never a posted-information rate. Horizon saturation is the model input $(\mathrm{rawBits}\cdot N)/4=2\pi E R$ with $\mathrm{rawBits}=\log_2|\mathrm{FaceCfg}|=4$. LEG-A is per-pixel additivity $S=mN$ over $N\ge 1$ private pixels.
Upstream, microstate_chain_contradicts_bound assembles those premises under the microstate reading into $S=3N>N=2\pi ER$. record_chain_saturates_bound does the same under the record reading and gets equality $S=N=2\pi ER$.
proof idea
Term-mode pair constructor. The left conjunct is exactly microstate_chain_contradicts_bound applied to the microstate hypotheses (including $N>0$ and the bound). The right conjunct is exactly record_chain_saturates_bound applied to the record hypotheses and saturation. No extra algebra: the certificate is the conjunction of the two already-proved chains.
why it matters
This is the single-statement certificate of the factor-3 keystone. Conditional on LEG-A, LEG-B, and Schwarzschild saturation, the microstate reading is excluded and the record reading is the unique consistent choice in the proved dichotomy, so HorizonEntropyIsRecordCost (the $1/4$ premise) is discharged by exclusion modulo exactly those named open legs.
The module status is explicitly conditional: LEG-B remains open as a typed Prop, never asserted; saturation is a model input; LEG-A is a measured model premise for private pixels. The exclusion is scale-free and survives bits↔nats conversion, so unit choice cannot rescue the microstate side. No downstream consumers are wired yet; the declaration closes the module's certificate layer for Live Bet 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.