Pith. sign in
module module moderate

IndisputableMonolith.Holography.RecognitionEventCapacity

show as:
view Lean formalization →

Defines the Shannon entropy of the forced geometric measure P(n)=(1-ρ)ρ^n as the information carried by one recognition event, then converts that entropy into effective outcome count, bits per event, and an additive event-access capacity. Holography and coefficient-bridge arguments cite these quantities when tying ledger multiplicity to area. The module is mostly closed-form algebra on the forced measure from MeasureForcing (T9).

claimFor the forced geometric law $P(n)=(1-\rho)\rho^n$ on recognition states, the module defines the Shannon entropy $H=-\sum_n P(n)\log P(n)$ (nats), the effective outcome count $e^H$, the bit capacity $H/\log 2$, and an additive event-access functional built from that capacity.

background

MeasureForcing (T9) closes the weighting gap left by the T0–T8 forcing chain: once J-cost, φ, the eight-tick period, and D=3 are fixed, the unique normalizable weight on discrete recognition ranks is the geometric law $P(n)=(1-\rho)\rho^n$. That measure is the sole probabilistic input here.

Recognition-event capacity treats one draw from $P$ as one atomic recognition event. Shannon entropy in nats is the mean surprise of that draw; exponentiating yields an effective number of equiprobable outcomes; dividing by $\log 2$ yields bits per event. An additive access functional packages those bits so multi-event ledgers accumulate capacity linearly.

The local setting is holography: these scalars are the information-theoretic side of plaquette or horizon counting, not a new dynamical law.

proof idea

Algebraic identities on the geometric series. Probability masses are rewritten as inverse powers of a fixed base; $1-\rho$ is tied to a square identity used in closed forms; negative log-masses become linear in the rank $n$. Entropy then collapses to an explicit function of $\rho$ (no series left). Effective outcomes and bits-per-event are definitional rewrites of that closed form. Event-access additivity is the corresponding homomorphism property under disjoint union of events. A certificate bundle packages the equalities for downstream import.

why it matters in Recognition Science

CoefficientBridge imports this module when reducing GAP 1: the count-to-area factor $\kappa$ in $a_{\mathrm{pix}}=\kappa,H,\ell_P^2$ (the “4” in Bekenstein–Hawking $S=A/4$) is framed as a physical selector among integer multiplicities already present in the ledger, not a number for decide to invent. Per-event entropy and bits supply the information side of that selector: whether multiplicity attaches to ledger-closure rank or to recognition-event capacity.

In the broader RS chain this sits after T9 (forced measure) and feeds holographic bookkeeping that must stay consistent with φ-ladder masses, eight-tick structure, and the native constants. Without a named event capacity, area-law coefficients remain ambiguous labels rather than derived selectors.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (13)