effectiveOutcomes
plain-language theorem explainer
Defines the effective outcome count of one recognition event as the perplexity exp(H) of the forced measure. Numerically this is φ^{φ+2} ≈ 5.70, the channel-capacity replacement for the deflated orbit count of 8. Anyone citing the rebuilt holographic access bound or EventCapacityCert uses this quantity. The body is a one-line exponential of forcedEntropy.
Claim. The effective outcome count per recognition event is $\mathrm{e}^{H}$, where $H$ is the Shannon entropy of the forced geometric measure on rungs (nats). Equivalently, once $H=(\varphi+2)\log\varphi$ is inserted, the count equals $\varphi^{\varphi+2}$.
background
This module rebuilds the holographic access bound after ThetaAccessDeflation killed the naive “eight states per site” orbit count. Physical per-carrier content is continuous, so the right bound is forced-measurement outcome quantization: a recognition event resolves into discrete $\varphi^{-n}$-weighted outcomes from the T9 forced measure (Foundation.MeasureForcing), with $p_n=(1-\varphi^{-1})\varphi^{-n}$, mean depth $\varphi$, and partition $\varphi^2$.
The information content of one event is the Shannon entropy of that measure, forcedEntropy. The present definition is its perplexity: $\mathrm{e}^{H}$. Module framing is explicit that entropy is average information / channel capacity, not zero-error distinguishability; hard readout can still separate infinitely many states.
Upstream, the closed form of the measure and the entropy keystone $H=(\varphi+2)\log\varphi$ come from MeasureForcing (via forcedEntropy_eq, neglog_probMass, meanRung_eq_phi). Related scaffolding names (rung counts, measurement outcomes, defect entropy) sit in the dependency graph but do not enter the body of this def.
proof idea
Definitional one-liner: effectiveOutcomes is Real.exp forcedEntropy. No tactics, no lemmas. The nontrivial identity effectiveOutcomes = φ^{φ+2} is proved downstream by unfolding this def, rewriting with forcedEntropy_eq, commuting the product, and applying Real.exp_mul / Real.exp_log.
why it matters
Supplies the central perplexity number of the recognition-event capacity story: $\varphi^{\varphi+2}\approx 5.70$ replaces the spurious orbit count 8 as the effective alphabet size per event. Downstream, effectiveOutcomes_eq pins the closed form modulo the entropy keystone, and EventCapacityCert packages it with entropy value, bit rate $(\varphi+2)\log_2\varphi$, and additivity of eventAccess over events.
In the broader RS chain this sits after measure forcing (geometric rung weights) and after the holography deflation that removed hard orbit ceilings. It is a channel-capacity quantity, consistent with T6 $\varphi$ as the self-similar scale and with the eight-tick octave as a temporal period rather than an outcome alphabet. Open (documented, not faked): the Born bridge identifying this entropy with a forced-measurement outcome law on recognition Hilbert space; residual phase lives in the elliptic $U(1)$ sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.