forcedEntropy
plain-language theorem explainer
Shannon entropy (nats) of the forced geometric measure P(n)=(1-ρ)ρ^n, read as information content of one recognition event. Holography and coefficient-bridge results cite it as the per-event capacity H. The declaration is a definitional tsum of p(-log p) over the forced masses from MeasureForcing.
Claim. Define the forced entropy $H\in\mathbb{R}$ by the Shannon series $H=\sum_{n=0}^{\infty} P(n)\,(-\log P(n))$, where $P(n)=(1-\rho)\rho^n$ is the normalized forced probability mass at depth $n$.
background
This module rebuilds the physical access bound after the deflation test killed naive eight-states-per-site orbit counting. The working hypothesis is forced-measurement outcome quantization: a recognition event resolves into discrete $\varphi^{-n}$-weighted outcomes given by the T9 forced measure from MeasureForcing.
That measure is $P(n)=(1-\rho)\rho^n$ with $\rho=\varphi^{-1}$, written here as probMass. It is normalized, has mean depth $\varphi$, and partition factor $\varphi^2$. The access law is then not an orbit count but the information content of one event: the Shannon entropy of this forced weighting, additive over independent events.
Upstream, probMass supplies the normalized geometric masses. The closed-form value $H=(\varphi+2)\log\varphi$ is proved separately as the keystone identity; this declaration only names the entropy functional itself.
proof idea
Definitional, not a proof. The body is the standard Shannon entropy tsum $\sum_n P(n)(-\log P(n))$ with $P=$ probMass. No tactics or lemmas fire at this site; downstream identities evaluate or rewrite the tsum.
why it matters
Central scalar of RecognitionEventCapacity: information per recognition event under the forced measure. Downstream, forcedEntropy_eq pins $H=(\varphi+2)\log\varphi$; effectiveOutcomes is the perplexity $e^H=\varphi^{\varphi+2}\approx 5.70$ (replacing the spurious 8); bitsPerEvent converts to $(\varphi+2)\log_2\varphi\approx 2.51$ bits; eventAccess k=k\cdot H scales the rate.
EventCapacityCert packages the entropy value, outcome count, bit rate, and definitional additivity. In CoefficientBridge, single_event_entropy_eq_H equates one-event access to $H$, so $H$ cancels in the Bekenstein branch and the pure geometric $1/4$ survives under the selector hypothesis.
Framework role: average channel capacity of forced readout, not a hard distinguishability ceiling (hard count is infinite). Open residual: the Born bridge identifying this entropy with a forced-measurement outcome law on recognition Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.