forcedEntropy_eq
plain-language theorem explainer
A single recognition event carries $(\varphi+2)\log\varphi$ nats under the forced geometric measure. Access-bound and holography arguments cite this as the physical per-event information content that replaces the deflated eight-state orbit count. The proof rewrites each entropy summand by the closed-form log-weight, splits the tsum into mean-depth and normalization pieces, and closes with mean rung $\varphi$ and unit total mass.
Claim. The Shannon entropy $H=-\sum_n P(n)\log P(n)$ of the forced recognition measure equals $(\varphi+2)\log\varphi$, where $\varphi$ is the golden ratio and $P(n)=(1-\varphi^{-1})\varphi^{-n}$ on rungs $n\in\mathbb{N}$.
background
This module rebuilds the physical access bound after the orbit-count deflation test. The naive "eight states per site" quotient fails because the physical per-carrier content is a continuum; the hard distinguishability count is infinite. The replacement hypothesis is forced-measurement outcome quantization: one recognition event resolves into discrete $\varphi^{-n}$-weighted outcomes, the T9 forced measure from MeasureForcing.
That measure is geometric: $P(n)=(1-\rho)\rho^n$ with $\rho=\varphi^{-1}$, normalized so $\sum P(n)=1$, with mean occupied rung $\langle n\rangle=\sum n,P(n)$ equal to $\varphi$ exactly (meanRung_eq_phi). The per-term identity neglog_probMass gives $-\log P(n)=(n+2)\log\varphi$. The module identifies the physical access rate with the Shannon entropy of this forced weighting (cost-sufficiency: it is the only intrinsic measure), not with an orbit cardinality.
Critical framing: entropy is average information / channel capacity, not a zero-error ceiling. Effective outcome count is perplexity $\mathrm{e}^H$, not a hard bound.
proof idea
Tactic proof of the standard entropy-of-geometric computation. First establish summability: $|\rho|<1$ from positivity and $\rho<1$; $\sum P(n)$ from the geometric series times $(1-\rho)$; $\sum n,P(n)$ from summable_pow_mul_geometric_of_norm_lt_one 1 times $(1-\rho)$; and $\sum 2,P(n)$ by scaling.
Unfold the entropy definition. Rewrite each summand via neglog_probMass so $P(n)(-\log P(n))=\log\varphi\cdot((n+2)P(n))$. By tsum_congr and additive tsum split, the series factors as $\log\varphi$ times $(\sum n,P(n)+\sum 2,P(n))$. Feed meanRung_eq_phi ($\sum n,P(n)=\varphi$) and probMass_tsum_one ($\sum P(n)=1$, so the second sum is $2$), then ring yields $(\varphi+2)\log\varphi$.
why it matters
Keystone of the rebuilt access law. Downstream, effectiveOutcomes_eq obtains the perplexity $\varphi^{\varphi+2}\approx 5.70$ (replacing the spurious $8$), bitsPerEvent_eq converts to $(\varphi+2)\log_2\varphi\approx 2.51$ bits, and eventCapacityCert packages entropy value, outcomes, bit rate, and additivity of eventAccess over $k$ events.
In the Recognition framework this is the physical content of one recognition event under the forced measure (mean depth $\varphi$, partition $\varphi^2$), with no free alphabet. It supersedes the deflated orbit count: that was a false hard ceiling; this is the true average rate. Open and documented (not faked): the Born bridge from the sub-Gaussian $L^2$ seed in MeasureForcing to recognition Hilbert space, so that this entropy is literally a forced-measurement outcome entropy. The residual phase lives in the elliptic $U(1)$ sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.