single_event_entropy_eq_H
plain-language theorem explainer
A single recognition event carries exactly the forced per-event Shannon entropy H. Anyone deriving the Bekenstein-Hawking 1/4 coefficient from the plaquette ledger cites this so pixel entropy equals H and cancels against capacity. The proof is a one-line unfolding of the model definition that accessible information across k events is k·H, specialized at k=1.
Claim. The information accessible across one recognition event equals the forced per-event Shannon entropy: if $A(k)$ denotes accessible information across $k$ events and $H$ is the Shannon entropy of the forced geometric measure $P(n)=(1-\rho)\rho^n$, then $A(1)=H$.
background
CoefficientBridge reduces the holographic area coefficient $\kappa$ in $a_{\mathrm{pix}}=\kappa\cdot H\cdot\ell_P^2$ (the "4" in Bekenstein-Hawking $S=A/4$) to a named physical selector. Rank-nullity of the landed ledger-closure map already yields rank 1, nullity 3, and total 4, so both candidate ratios $1/4$ and $3/4$ are proved; the open input is whether per-plaquette multiplicity attaches to closure rank or free-bit nullity.
Forced entropy $H$ is the Shannon entropy (nats) of the forced measure $P(n)=(1-\rho)\rho^n$: information per recognition event. Accessible information across $k$ events is the model definition $A(k)=k\cdot H$. As the upstream doc states, this linearity is definitional; substantive product-measure additivity via factorization remains open.
This identity is the $k=1$ specialization used when a single closed plaquette is treated as one recognition event on the Bekenstein branch.
proof idea
One-line wrapper. simp unfolds the definition $A(k):=k\cdot H$ at $k=1$, reducing the goal to $1\cdot H=H$ by ordinary real arithmetic. No entropy lemma, series identity, or measure-theoretic fact is applied; the equality is pure definitional linearity of the model access functional.
why it matters
Doc-comment payoff of the Bekenstein branch: a single-event plaquette carries $S_{\mathrm{pixel}}=H$, so $H$ cancels against per-event capacity and the pure geometric $1/4$ (closure rank over sector count) survives. The module already lands rank $=1$, nullity $=3$, total $=4$, the first-isomorphism check, and both ratios against recognition_sector_count = 4. The remaining GAP 1 input is the selector that multiplicity equals closure rank rather than nullity; once chosen, this identity is the entropy cancellation step. No recorded downstream uses yet; it is staged for discharges such as a Bekenstein-from-selector theorem. Framework link: holographic coefficient selection after the D=3 eight-tick ledger structure, not a new forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.