eventAccess
plain-language theorem explainer
Defines the information accessible across k recognition events as k times the forced per-event Shannon entropy H ≈ (φ+2) log φ. Holography and Bekenstein-coefficient arguments cite it as the rebuilt access rate replacing the deflated orbit-count bound. The body is pure definitional scaling: cast k to ℝ and multiply by forcedEntropy; it records the linear shape, not product-measure additivity.
Claim. For each natural number $k$, the accessible information across $k$ recognition events is defined by $\mathrm{eventAccess}(k) := k \cdot H$, where $H$ is the Shannon entropy (nats) of the forced geometric measure $P(n)=(1-\rho)\rho^n$ with $\rho=\varphi^{-1}$.
background
This module rebuilds the holographic access bound after the deflation test killed the naive "eight states per site" orbit count. The physical content is continuum-valued; the right bound is forced-measurement outcome quantization under the T9 forced measure from MeasureForcing: $P(n)=(1-\varphi^{-1})\varphi^{-n}$, normalized, mean depth $\varphi$, partition $\varphi^2$.
The central scalar is the Shannon entropy of that measure, forcedEntropy $= \sum_n P(n)(-\log P(n))$, proved equal to $(\varphi+2)\log\varphi$ nats (effective outcomes $\varphi^{\varphi+2}\approx 5.70$, about $2.51$ bits per event). Entropy here is average information / channel capacity, not a hard distinguishability ceiling: a forced readout can hard-distinguish infinitely many states, so the rebuilt law is a mutual-information rate.
Upstream, the cost algebra's shifted cost $H(x)=J(x)+1$ is a different $H$; here the symbol is overloaded for the forced-measure entropy. The definition simply scales that entropy by the event count $k$.
proof idea
Definitional, not a proved equality. The body is the one-line product $(k:\mathbb{R})\cdot\mathrm{forcedEntropy}$. No lemmas are applied; linearity in $k$ is true by construction. The sibling theorem eventAccess_additive only unfolds this definition and rings; the doc-comment stresses that product-measure additivity (entropy of $k$ independent events equals $k\cdot H$ via Factorizes) remains open and is not what this def establishes.
why it matters
Supplies the scaled access rate that replaces the old $|R|\log_2|\alpha|$ bound (uniform alphabet special case) inside the Recognition Event Capacity package. Downstream, single_event_entropy_eq_H in CoefficientBridge uses the $k=1$ case so a single-event plaquette carries exactly forcedEntropy, letting $H$ cancel against per-event capacity and leave the pure geometric $1/4$ on the Bekenstein branch.
eventAccess_additive and the EventCapacityCert structure package the definitional additivity together with the closed forms for entropy, effective outcomes, and bit rate. Framework role: after T5–T8 force $J$, $\varphi$, the eight-tick octave and $D=3$, MeasureForcing forces the geometric weights; this def turns that per-event entropy into the multi-event access law. Open next target (explicitly not claimed here): substantive product-measure additivity and the Born bridge from the sub-Gaussian $L^2$ seed to recognition Hilbert space.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.