bandwidth
plain-language theorem explainer
Recognition bandwidth supplies the maximum rate of recognition events R_max(A) permitted inside a holographic region of boundary area A. Analysts of information throughput in unified models cite it when bounding ledger processing in complexity or astrophysical settings. The definition is a direct algebraic assembly of the area term, Planck area, recognition cost k_R, and eight-tick period.
Claim. The recognition bandwidth for a region of boundary area $A$ is $R_*(A) = A / (4 ell_P^2 k_R 8 tau_0)$, where $k_R = ln phi$ is the cost per ledger bit and $8 tau_0$ is the eight-tick cadence period.
background
The module RecognitionBandwidth links the holographic bound on information capacity to the per-event recognition cost and the fixed processing cadence. It defines recognition bandwidth as the maximum rate of recognition events inside a region whose boundary area is $A$. Key imported definitions are k_R := ln(phi) from Constants.BoltzmannConstant, planckArea from Quantum.BekensteinHawking, and eightTickCadence from the eight-tick foundation.
proof idea
The definition is a one-line arithmetic expression that divides the supplied area by the product of four times planckArea, k_R, and eightTickCadence.
why it matters
This definition supplies the core quantity referenced by BernsteinBound in Analysis, nuclear_tier_local in Astrophysics, and the PvsNPFromBIT certification in Complexity. It realizes the module goal of connecting holographic capacity, k_R, and the eight-tick cadence, which aligns with the eight-tick octave (T7) in the forcing chain. The module doc-comment notes that five previously disconnected elements are now formally joined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.