C_ilg_prefactor_pos

formal source

 131    This replaces the earlier phi^(-5) = cLagLock in the galactic-scale kernel. -/
 132noncomputable def C_ilg_prefactor : ℝ := phi ^ (-(3/2 : ℝ))
 133
 134theorem C_ilg_prefactor_pos : 0 < C_ilg_prefactor := by
 135  unfold C_ilg_prefactor
 136  exact Real.rpow_pos_of_pos phi_pos _
 137
 138/-- The ILG alpha exponent: alpha = (1 - 1/phi) / 2 = alphaLock. -/
 139theorem ilg_alpha_is_alphaLock : alphaLock = (1 - 1/phi) / 2 := rfl
 140
 141/-! ## Certificate -/
 142
 143structure CoerciveProjectionCert where
 144  coercivity_positive : (0 : ℚ) < c_coercive
 145  net_above_one : (1 : ℚ) < K_net
 146  operator_positive : ∀ w f : ℝ, 1 ≤ w → 0 ≤ w * f ^ 2
 147  prefactor_positive : 0 < C_ilg_prefactor
 148
 149theorem coercive_projection_cert : CoerciveProjectionCert where
 150  coercivity_positive := c_coercive_pos
 151  net_above_one := K_net_gt_one
 152  operator_positive := fun w f hw => energy_bounded_below w f hw (sq_nonneg f)
 153  prefactor_positive := C_ilg_prefactor_pos
 154
 155end
 156
 157end CoerciveProjection
 158end Gravity
 159end IndisputableMonolith