kernel_unity_at_saturation

formal source

 152  demandedRate / availableBandwidth
 153
 154/-- The bandwidth kernel equals 1 at saturation (transition point). -/
 155theorem kernel_unity_at_saturation {R : ℝ} (hR : 0 < R) :
 156    bandwidthKernel R R = 1 := by
 157  unfold bandwidthKernel
 158  exact div_self (ne_of_gt hR)
 159
 160/-- The bandwidth kernel exceeds 1 when demand > bandwidth (ILG regime). -/
 161theorem kernel_gt_one_when_saturated {Rd Rb : ℝ} (hb : 0 < Rb) (h : Rb < Rd) :
 162    1 < bandwidthKernel Rd Rb := by
 163  unfold bandwidthKernel
 164  rw [one_lt_div hb]
 165  exact h
 166
 167/-- The bandwidth kernel is below 1 when demand < bandwidth (Newtonian). -/
 168theorem kernel_lt_one_when_sub {Rd Rb : ℝ} (hb : 0 < Rb) (h : Rd < Rb) :
 169    bandwidthKernel Rd Rb < 1 := by
 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. -/
 181theorem Clag_is_coherence_quantum :
 182    Clag = 1 / phi ^ (5 : ℕ) := rfl
 183
 184/-- **THEOREM**: The ILG α = (1−1/φ)/2 determines the power-law index of
 185    the bandwidth kernel's scaling with dynamical time.