kernel_gt_one_when_saturated

formal source

 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.
 186
 187    When T_dyn ≫ τ₀, the demanded rate scales as 1/T_dyn while the
 188    bandwidth is fixed, so the kernel scales as T_dyn^α where
 189    α = (1−1/φ)/2 is the φ-determined exponent. -/
 190theorem alpha_is_bandwidth_exponent :
 191    alpha_locked = (1 - 1 / phi) / 2 := rfl