pith. machine review for the scientific record. sign in
theorem proved tactic proof

low_accel_saturated

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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. -/

depends on (24)

Lean names referenced from this declaration's body.