bandwidthKernel
plain-language theorem explainer
bandwidthKernel supplies the ratio of demanded recognition rate to available bandwidth as the ILG time kernel w_t. Workers deriving the transition between Newtonian and saturated regimes from holographic bounds cite this ratio when linking throughput limits to gravitational amplification. The definition is a direct quotient of the two real inputs.
Claim. Let $w_t(R_d, R_b) = R_d / R_b$, where $R_d$ is the recognition event rate demanded by Newtonian gravitational dynamics of mass $M$ at dynamical time $T$ and $R_b$ is the maximum recognition bandwidth permitted by the holographic bound on area $A$.
background
The module treats bandwidth saturation as the mechanism by which ILG gravity emerges: when Newtonian dynamics demand more recognition events per unit time than the holographic bound allows, the recognition operator compensates by batching multiple dynamical times into each 8-tick cycle. This batching is exactly the time kernel $w_t > 1$ that amplifies gravity. The upstream definition bandwidth(area) computes the holographic maximum rate as area divided by (4 Planck areas times k_R times the eight-tick cadence). The upstream definition demandedRate(mass, dynamicalTime) computes the Newtonian demand as mass divided by dynamicalTime in RS-native units where the Planck mass is 1.
proof idea
One-line definition returning the quotient of the demandedRate input and the availableBandwidth input.
why it matters
The definition is the direct input to the three downstream theorems kernel_unity_at_saturation, kernel_gt_one_when_saturated and kernel_lt_one_when_sub that establish the Newtonian, transition and ILG regimes. It supplies the concrete realization of the ILG time kernel w_t inside the saturation picture, tying the eight-tick cadence (T7) and the holographic bound to the emergence of modified gravity below the critical acceleration. The module doc-comment states that this batching restores consistency when demand exceeds bandwidth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.