kernel_unity_at_saturation
plain-language theorem explainer
The bandwidth kernel, defined as the ratio of demanded recognition rate to available bandwidth, equals one exactly when the two rates coincide at a positive value. Workers deriving the saturation acceleration a_sat or the transition between Newtonian and ILG regimes would cite this boundary marker. The proof is a one-line wrapper that unfolds the ratio definition and invokes the algebraic identity x/x = 1 for x > 0.
Claim. Let $R > 0$. Then the ratio of demanded recognition rate to available bandwidth equals 1, i.e., $R/R = 1$.
background
The module treats bandwidth saturation as the point where Newtonian demand for recognition events exceeds the holographic bound, forcing the ILG time kernel w_t > 1 via batching over 8-tick cycles. Recognition bandwidth is the maximum event rate permitted by area A: R_max(A) = A / (4 ℓ_P² · k_R · 8 τ_0). The bandwidth kernel is the ratio of demanded rate to this maximum; it equals 1 precisely at saturation. Upstream, the BIT kernel families supply constant, inverse-linear, and exponential forms, while the ILG kernel supplies the power-law correction w(k,a) = 1 + C (a/(k τ_0))^α used once saturation is crossed.
proof idea
The term proof unfolds the definition of bandwidthKernel as demandedRate / availableBandwidth, then applies the lemma div_self to the hypothesis 0 < R, which directly yields the equality to 1.
why it matters
This equality fixes the transition point in the saturation picture, where demanded rate equals available bandwidth and the ILG kernel remains Newtonian. It anchors the critical acceleration a_sat derived from the holographic bound and the eight-tick cadence, and supports downstream claims that w_t > 1 restores consistency above saturation. The result closes the boundary case in the unification chain linking recognition throughput limits to modified gravity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.