low_accel_saturated

formal source

 126    When a < a_sat, the gravitational area is large and the demanded recognition
 127    rate exceeds the holographic bandwidth. The recognition operator compensates
 128    by amplifying the effective gravitational coupling. -/
 129theorem low_accel_saturated {a : ℝ} (ha_pos : 0 < a) (ha : a < saturationAccel)
 130    {G_N M : ℝ} (hG : 0 < G_N) (hM : 0 < M) :
 131    gravArea G_N M saturationAccel < gravArea G_N M a := by
 132  have hGM : 0 < G_N * M := mul_pos hG hM
 133  have hsat : 0 < saturationAccel := saturationAccel_pos
 134  unfold gravArea
 135  have key : G_N * M / saturationAccel < G_N * M / a := by
 136    rw [div_lt_div_iff₀ hsat ha_pos]; nlinarith
 137  have hds : 0 ≤ G_N * M / saturationAccel := le_of_lt (div_pos hGM hsat)
 138  exact mul_lt_mul_of_pos_left
 139    (by nlinarith [mul_self_lt_mul_self hds key]) (mul_pos (by linarith) Real.pi_pos)
 140
 141/-! ## §5. ILG Kernel as Bandwidth Compensation -/
 142
 143/-- The ILG time kernel w_t amplifies gravity when bandwidth is saturated.
 144
 145    In the saturation picture, w_t is the ratio of demanded rate to available
 146    bandwidth:
 147        w_t = R_demand / R_max = (demanded rate) / (bandwidth)
 148
 149    When w_t > 1, more gravitational effect is packed into each 8-tick cycle
 150    than Newtonian dynamics would require — exactly the ILG modification. -/
 151noncomputable def bandwidthKernel (demandedRate availableBandwidth : ℝ) : ℝ :=
 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