eventAccess_additive
plain-language theorem explainer
Access scales linearly with event count: the information available from j+k recognition events equals the sum of the j-event and k-event access rates. Anyone assembling the recognition-event capacity certificate cites this. The proof is definitional: unfold the rate as k times forced entropy, then finish by ring arithmetic.
Claim. For all natural numbers $j,k$, the recognition-event access rate satisfies $A(j+k)=A(j)+A(k)$, where $A(n)=n\cdot H$ and $H=(\varphi+2)\log\varphi$ is the Shannon entropy (nats) of the forced geometric measure on outcomes.
background
This module rebuilds the holographic access bound after the orbit-count deflation test. Physical per-carrier content is continuum-valued, so hard orbit cardinality is not the right ceiling. The working hypothesis is forced-measurement outcome quantization: one recognition event resolves into discrete $\varphi^{-n}$-weighted outcomes from the T9 forced measure (`probMass n = (1-\varphi^{-1})\varphi^{-n}$), whose Shannon entropy is the physical per-event information.
The central forced numbers are $H=(\varphi+2)\log\varphi$ nats per event (about 1.741), effective outcome count (perplexity) $\varphi^{\varphi+2}\approx 5.70$, and bit rate $(\varphi+2)\log_2\varphi\approx 2.51$. Access over $k$ events is defined by scaling: $A(k)=k\cdot H$. Entropy here is average information / channel capacity, not zero-error distinguishability; a forced readout can hard-distinguish infinitely many states, so perplexity is an effective count, not a hard cardinality bound.
The doc-comment flags this lemma as MODEL definitional linearity, not the open substantive product-measure additivity theorem.
proof idea
One-line tactic proof. Unfold the definition $A(n)=n\cdot H$ on both sides, push natural-number casts into the reals, and close with ring. No external lemmas are required; additivity is the bilinearity of scalar multiplication by the fixed real $H$.
why it matters
Feeds the package theorem eventCapacityCert, which records four facts: the closed-form forced entropy, the effective outcome count $\varphi^{\varphi+2}$, the bit-rate identity, and this additivity. Together they certify the rebuilt access law as forced-measure entropy per event, scaled over event count, replacing the deflated $|R|\log_2|\alpha|$ orbit bound.
In the Recognition framework this is the information-theoretic half of the holography access story after MeasureForcing: the geometric weights and mean depth $\varphi$ are already proved; identifying per-event information with that entropy is the MODEL step recorded here. The open Born bridge (entropy of a forced-measurement outcome distribution in recognition Hilbert space) and the residual $U(1)$ phase sector remain separate. The doc-comment is explicit that product-measure additivity of independent events is still open; this lemma only locks the linear scaling shape $A(k)=kH$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.