saturationAccel_pos

formal source

  90noncomputable def saturationAccel : ℝ :=
  91  Real.pi / (2 * k_R)
  92
  93theorem saturationAccel_pos : 0 < saturationAccel := by
  94  unfold saturationAccel
  95  exact div_pos Real.pi_pos (mul_pos (by norm_num : (0:ℝ) < 2) k_R_pos)
  96
  97/-- Saturation acceleration is well-defined (positive and finite). -/
  98theorem saturationAccel_well_defined : 0 < saturationAccel ∧ saturationAccel ≠ 0 :=
  99  ⟨saturationAccel_pos, ne_of_gt saturationAccel_pos⟩
 100
 101/-! ## §4. Regime Classification -/
 102
 103/-- **THEOREM**: Above saturation acceleration, the system is sub-saturated
 104    (Newtonian gravity suffices).
 105
 106    When a > a_sat, the gravitational area is small enough that the holographic
 107    bandwidth exceeds the demanded recognition rate. -/
 108theorem high_accel_newtonian {a : ℝ} (ha : saturationAccel < a)
 109    {G_N M : ℝ} (hG : 0 < G_N) (hM : 0 < M) :
 110    gravArea G_N M a < gravArea G_N M saturationAccel := by
 111  have hsat : 0 < saturationAccel := saturationAccel_pos
 112  have ha_pos : 0 < a := lt_trans hsat ha
 113  have hGM : 0 < G_N * M := mul_pos hG hM
 114  unfold gravArea
 115  have key : G_N * M / a < G_N * M / saturationAccel := by
 116    rw [div_lt_div_iff₀ ha_pos hsat]; nlinarith
 117  have hda : 0 ≤ G_N * M / a := le_of_lt (div_pos hGM ha_pos)
 118  -- gravArea is 4π(GM/a)²; since GM/a < GM/a_sat, the square comparison follows
 119  -- by monotonicity of x ↦ x² on [0,∞) and multiplication by 4π > 0
 120  exact mul_lt_mul_of_pos_left
 121    (by nlinarith [mul_self_lt_mul_self hda key]) (mul_pos (by linarith) Real.pi_pos)
 122
 123/-- **THEOREM**: Below saturation acceleration, the system is bandwidth-saturated