kernel_lt_one_when_sub
The bandwidth kernel stays strictly below one when recognition demand is less than available bandwidth with positive bandwidth. Researchers deriving the Newtonian limit in ILG gravity models cite this to establish the sub-saturation regime. The proof is a direct algebraic reduction that unfolds the kernel as a ratio and applies the division inequality.
claimLet $R_d$ be recognition demand and $R_b > 0$ the bandwidth capacity. If $R_d < R_b$, then the bandwidth kernel satisfies $R_d / R_b < 1$.
background
The bandwidth kernel is the ratio of demanded recognition events per unit time to the holographic bandwidth bound set by the eight-tick cycle. In the module setting, saturation occurs when this ratio reaches one, at which point the recognition operator batches updates and the ILG time kernel $w_t > 1$ appears to restore consistency with the gravitational field. Upstream results supply the general kernel forms from BITKernelFamilies and the J-cost definitions from MultiplicativeRecognizerL4 and ObserverForcing that underlie the demand count.
proof idea
The proof is a one-line wrapper that unfolds the bandwidthKernel definition, rewrites via the division-less-than-one lemma for positive denominator, and concludes directly from the hypothesis.
why it matters in Recognition Science
This result anchors the Newtonian regime below saturation and supports the module claims that ILG parameters such as C_lag are bandwidth-determined. It sits inside the T7 eight-tick octave and the forcing chain that produces D = 3 and the alpha band from recognition throughput limits. No downstream uses are recorded yet.
scope and limits
- Does not give the explicit algebraic form of the bandwidth kernel.
- Does not address the regime where demand exceeds bandwidth.
- Does not derive the numerical value of the saturation acceleration.
- Does not connect the kernel to specific constants such as phi or C_lag.
formal statement (Lean)
168theorem kernel_lt_one_when_sub {Rd Rb : ℝ} (hb : 0 < Rb) (h : Rd < Rb) :
169 bandwidthKernel Rd Rb < 1 := by
proof body
Term-mode proof.
170 unfold bandwidthKernel
171 rw [div_lt_one hb]
172 exact h
173
174/-! ## §6. ILG Parameters Are Bandwidth-Determined -/
175
176/-- **THEOREM**: The ILG C_lag = φ⁻⁵ is the coherence energy quantum.
177
178 In the bandwidth picture, φ⁻⁵ is the energy cost per recognition event
179 in RS-native units. The ILG kernel amplifies by this energy quantum
180 per excess event beyond the bandwidth limit. -/