EventCapacityCert
plain-language theorem explainer
Packages four equalities that certify the forced recognition-event capacity: Shannon entropy equals $(\varphi+2)\log\varphi$ nats, effective outcomes equal $\varphi^{\varphi+2}$, bit rate equals $(\varphi+2)\log_2\varphi$, and access scales additively in the event count. Anyone citing the rebuilt holographic access bound against the deflated eight-state orbit count uses this certificate. It is a pure Prop bundle; the inhabitant is assembled elsewhere from the closed-form lemmas.
Claim. A recognition-event capacity certificate is a proposition asserting four facts: the Shannon entropy of the forced geometric measure equals $(\varphi+2)\log\varphi$; the effective outcome count (perplexity) equals $\varphi^{\varphi+2}$; the information per event in bits equals $(\varphi+2)\log_2\varphi$; and accessible information over $j+k$ events equals the sum of the accessibles over $j$ and over $k$.
background
This module rebuilds the holographic access bound after the deflation test killed the naive "eight states per site" orbit count. Physical per-carrier content is continuous, so orbit cardinality is not the right ceiling. The replacement hypothesis is forced-measurement outcome quantization: one recognition event resolves into discrete $\varphi^{-n}$-weighted outcomes from the T9 forced measure $P(n)=(1-\varphi^{-1})\varphi^{-n}$ (normalized, mean depth $\varphi$, partition $\varphi^2$), proved in MeasureForcing.
The Shannon entropy of that measure is the information per event: $\sum_n P(n)(-\log P(n))$. Its exponential is the effective outcome count (perplexity), not a hard distinguishability ceiling; hard readout can separate infinitely many states. Bits per event are that entropy converted by $\log 2$. Access over $k$ events is defined as $k$ times the per-event entropy, so additivity in $k$ is definitional linearity of that scaling, not yet product-measure independence.
The golden identity $1-\varphi^{-1}=\varphi^{-2}$ drives the closed forms. Numerically one gets roughly $1.741$ nats, perplexity $\approx 5.70$ (genuinely different from $8$), and $\approx 2.51$ bits per event.
proof idea
No proof body: this is a structure of type Prop whose four fields are named equalities (and one $\forall$-statement). Inhabitation is deferred to the downstream constructor, which fills the fields by the already-proved identities for forced entropy, effective outcomes, bits per event, and definitional additivity of event access. Treat it as a certificate interface, not a derivation.
why it matters
This is the named Prop that the module's certificate theorem inhabits, bundling the four forced numbers that replace the spurious orbit-count access law. Downstream, the single theorem eventCapacityCert supplies all four witnesses at once, so later holography or channel-capacity arguments can depend on one object rather than four scattered lemmas.
In the Recognition framework it records the physical access rate as forced-measure entropy: average information / channel capacity per recognition event, additive over events. That supersedes the deflated $|R|\log_2|\alpha|$ bound (the uniform-alphabet special case). It sits on the T9 forced measure from MeasureForcing and on $\varphi$ from the forcing chain (T5–T6). Framing caution from the module: entropy is not zero-error distinguishability; effective outcomes are perplexity, not a hard cardinality ceiling.
Open next to the certificate itself: substantive product-measure additivity for independent events, and the Born bridge identifying this entropy with a forced-measurement outcome distribution on recognition Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.