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-ρ)ρⁿ as information per recognition event, plus derived quantities: effective outcomes, bits per event, and additive event access. Holography and coefficient-bridge work cite it when converting recognition multiplicity into an area-law coefficient. The module is mostly closed-form algebra on the geometric series forced by 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) as information per recognition event, the effective outcome count $e^H$, bits per event $H/\log 2$, and an additive event-access functional built from those quantities, with equality lemmas tying each back to closed forms in $\rho$.

background

The T0–T8 forcing chain fixes cost $J$, scale $\varphi$, the eight-tick period, and $D=3$, but not the weighting over allowed recognition states. MeasureForcing (T9) closes that gap: the unique consistent measure on those states is the geometric law $P(n)=(1-\rho)\rho^n$.

This holography module takes that forced measure as given and extracts its information content. Shannon entropy in nats is the natural scalar: how much information is carried by one recognition event drawn from $P$. Sibling definitions package the same content as effective outcome count, bits per event, and an additive access functional suitable for stacking events on a holographic screen.

Notation follows the upstream measure module: $\rho$ is the forced decay parameter of the geometric series; probability mass and $-\log P$ identities are the algebraic fuel for the entropy closed form.

proof idea

Definition-and-identity module, not a deep existence proof. Probability-mass and $-\log P$ lemmas reduce the geometric series to elementary powers of $\rho$. Entropy is then evaluated in closed form; effective outcomes and bits-per-event are rewrites of that scalar. Event access is defined so additivity is immediate from the entropy expression. A certificate bundle packages the equalities for downstream import.

why it matters in Recognition Science

Feeds CoefficientBridge, which treats the count-to-area coefficient $\kappa$ in $a_{\mathrm{pix}}=\kappa\cdot H\cdot\ell_P^2$ (the “4” in Bekenstein–Hawking $S=A/4$) as a named physical selector rather than a number for decide to pick. Per-event information and multiplicity from this module are the ledger-side inputs that selector must attach to (rank vs. other integer labels already present in the stack).

In the broader RS chain this sits after T9 measure forcing and before holographic coefficient identification: once the measure is forced, entropy per recognition event is the bridge quantity between discrete ledger ticks and continuum area law. It does not itself pick $\kappa$; it supplies the information-theoretic side of that choice.

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)