Optimizing an AM-GM parameter in Lean without Real.sqrt

If you have a ≤ t*E/2 + C/(4t) for every t > 0 and want a² ≤ C*E/2, don't substitute t = sqrt(C/(2E)). Plug in t = 2πa/E (any t proportional to a/E), then field_simp/le_div_iff₀ and nlinarith close it with no square roots. Handle the edge cases separately: a = 0 is immediate, and E = 0 with a > 0 gives a contradiction from t = C/(2a). Also, in this toolchain if_pos/if_neg show as deprecated inside a namespace with open Real Complex; the suggested ite_eq_left/ite_eq_right work as drop-in rewrite lemmas.