eventCapacityCert
plain-language theorem explainer
Packages the four forced-measure access identities into a single certificate: per-event 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 event count. Anyone citing the rebuilt holographic access bound (replacing the deflated orbit count of 8) would reference this bundle. The proof is a pure structure inhabitant that wires four already-proved equalities.
Claim. There is a recognition-event capacity certificate asserting: the forced per-event entropy equals $(\varphi+2)\log\varphi$; the effective outcome count (perplexity) equals $\varphi^{\varphi+2}$; the bit rate equals $(\varphi+2)\log_2\varphi$; and for all natural numbers $j,k$, access over $j+k$ events equals the sum of the accesses 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: a single recognition event resolves into discrete $\varphi^{-n}$-weighted outcomes from the T9 forced measure in MeasureForcing, with $p_n=(1-\varphi^{-1})\varphi^{-n}$, mean depth $\varphi$, and partition $\varphi^2$.
The physical access law is then the Shannon entropy of that measure, not an orbit count. The keystone identity is forced entropy $H=(\varphi+2)\log\varphi$ nats ($\approx 1.741$), proved from mean depth $\varphi$ and normalization via the geometric-series entropy computation. Effective outcomes are the perplexity $e^H=\varphi^{\varphi+2}\approx 5.70$; the bit rate is $(\varphi+2)\log_2\varphi\approx 2.51$ bits. Access over $k$ events is defined as $k\cdot H$.
Critical framing: entropy bounds average information (channel capacity), not zero-error distinguishability. A forced readout can hard-distinguish infinitely many states, so the effective outcome count is a perplexity, not a hard cardinality ceiling.
proof idea
Term-mode structure inhabitant. The certificate is a Prop-valued structure with four fields; the proof supplies each field by naming the corresponding proved lemma:
entropy_valuefromforcedEntropy_eq(keystone Shannon-tsum evaluation),outcomes_valuefromeffectiveOutcomes_eq(exponentiate the entropy identity),bits_valuefrombitsPerEvent_eq(change of log base from the entropy identity),additivefromeventAccess_additive(definitional linearity of $k\mapsto k\cdot H$).
No new algebra is done here; the certificate is the packaging layer over those four results.
why it matters
This is the module's public certificate that the rebuilt access law is fully discharged at the theorem level: entropy value, effective outcomes, bit rate, and additive scaling. It closes the local story that supersedes the deflated eight-state orbit bound with a parameter-free forced-measure capacity ($\approx 2.51$ bits per event, effective outcomes $\approx 5.70$).
In the Recognition framework this sits downstream of MeasureForcing (T9 forced measure) and of the entropy keystone computation from mean rung $\varphi$ and normalization. It records the MODEL identification of "information per recognition event" with forced-measure entropy. The module doc flags what remains open: the Born bridge from the sub-Gaussian $L^2$ seed to recognition Hilbert space, and genuine product-measure additivity (the packaged additivity is only definitional scaling). No downstream consumers are wired yet; the certificate is the handoff point for later holographic or channel-capacity arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.