kernel_lt_one_when_sub
plain-language theorem explainer
The bandwidth kernel stays strictly below unity when demanded recognition rate lies below available bandwidth, confirming the Newtonian regime. Researchers modeling emergent gravity via recognition throughput limits cite this to separate sub-saturated from saturated dynamics. The proof unfolds the kernel definition as a ratio and applies the standard division inequality for positive denominators.
Claim. Let $R_d, R_b > 0$ be real numbers satisfying $R_d < R_b$. Then the bandwidth kernel $K(R_d, R_b)$ obeys $K(R_d, R_b) < 1$.
background
The BandwidthSaturation module shows how ILG gravity emerges when a system's demanded recognition events per unit time exceed the holographic bound, forcing batching over the eight-tick cycle. The bandwidth kernel is the ratio of demanded rate to available bandwidth; values below one recover Newtonian dynamics. Upstream results include the BIT kernel definition (constant, inverse-linear, or exponential families) and the J-cost of recognition events supplied by MultiplicativeRecognizerL4.cost and ObserverForcing.cost.
proof idea
One-line wrapper that unfolds the bandwidthKernel definition, rewrites the target inequality via the division lemma for positive reals, and discharges the hypothesis directly.
why it matters
This result anchors the Newtonian regime inside the bandwidth saturation picture and feeds the module's later claims on saturation acceleration and ILG kernel compensation. It aligns with the Recognition Science forcing chain at T7 (eight-tick octave) and the throughput limit that sets C_lag = phi^{-5}. No open scaffolding remains for this specific inequality.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.