def ConcentratedRegime (H T Tstar : ℝ) : Prop := H > 1/2 ∧ T < Tstar
thesis/CESProofs/Potential/EffectiveCurvature.lean:295
## General-Weight and IRS Effective Curvature Definitions