bandwidthKernel
plain-language theorem explainer
The bandwidth kernel is the ratio of demanded recognition rate to available holographic bandwidth, serving as the ILG time kernel w_t. Researchers deriving saturation conditions for modified gravity would cite this definition when linking throughput limits to gravitational amplification. It is implemented as a direct division of the two real inputs.
Claim. The bandwidth kernel equals \( w_t = R_{\rm demand} / R_{\rm max} \), where \( R_{\rm demand} = M / T_{\rm dyn} \) is the recognition event rate required by Newtonian dynamics and \( R_{\rm max} = A / (4 \ell_P^2 \cdot k_R \cdot 8 \tau_0) \) is the maximum rate permitted by the holographic bound.
background
Recognition bandwidth is defined as the maximum recognition events per unit time allowed by the holographic bound on area A, computed as area divided by (4 planckArea times k_R times eightTickCadence). Demanded rate is the Newtonian requirement mass divided by dynamicalTime, expressed in RS-native units with Planck mass set to 1.
The module establishes that when demanded rate exceeds bandwidth, the recognition operator batches updates across 8-tick cycles, producing the ILG time kernel w_t greater than 1. This definition supplies exactly that ratio.
Upstream results supply the bandwidth definition (R_max(A) equals area over the product of four Planck areas, k_R, and eight-tick cadence) and the demandedRate definition (R_demand equals mass over dynamicalTime).
proof idea
One-line definition that returns the quotient of the two real-number inputs.
why it matters
This definition supplies the ratio used by the three downstream theorems kernel_unity_at_saturation, kernel_gt_one_when_saturated, and kernel_lt_one_when_sub. It implements the ILG time kernel described in the module doc-comment, connecting recognition throughput limits to the eight-tick octave (T7) and the emergence of modified gravity when saturation occurs. It forms the direct interface between RecognitionBandwidth and saturation analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.