Signs of irreducible quadratics over real closed fields

An irreducible quadratic over an ordered real closed field has negative discriminant. Its value is therefore everywhere nonzero and has the sign of its leading coefficient. The discriminant criterion also gives the converse characterization of irreducibility. These facts supply the quadratic case of the algebraic polynomial intermediate value theorem.

The general sign calculation in TauCeti.Algebra.Polynomial.QuadraticDiscriminant only requires an ordered ring; real closedness is used to turn a nonnegative discriminant into a square. The quadratic discriminant and root criteria are those of Mathlib.Algebra.QuadraticDiscriminant.

@[simp]

theorem TauCeti.irreducible_quadratic_iff_discrim_neg {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {a b c : R} (ha : a ≠ 0) : Irreducible (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) ↔ discrim a b c < 0

A genuine quadratic over a real closed field is irreducible exactly when its discriminant is negative.

theorem TauCeti.irreducible_quadratic_eval_pos_iff {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {a b c : R} (ha : a ≠ 0) (hi : Irreducible (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) (x : R) : 0 < Polynomial.eval x (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) ↔ 0 < a

Positivity of the value of an irreducible quadratic over a real closed field is equivalent to positivity of its leading coefficient.

theorem TauCeti.irreducible_quadratic_eval_neg_iff {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {a b c : R} (ha : a ≠ 0) (hi : Irreducible (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c)) (x : R) : Polynomial.eval x (Polynomial.C a * Polynomial.X ^ 2 + Polynomial.C b * Polynomial.X + Polynomial.C c) < 0 ↔ a < 0

The negative-sign counterpart of irreducible_quadratic_eval_pos_iff.

@[simp]

theorem TauCeti.irreducible_quadratic_eval_pos_iff_leadingCoeff_pos {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hi : Irreducible p) (hdeg : p.natDegree = 2) (x : R) : 0 < Polynomial.eval x p ↔ 0 < p.leadingCoeff

The value of an irreducible polynomial of degree two is positive exactly when its leading coefficient is positive. This form does not require a coefficient presentation.

@[simp]

theorem TauCeti.irreducible_quadratic_eval_neg_iff_leadingCoeff_neg {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hi : Irreducible p) (hdeg : p.natDegree = 2) (x : R) : Polynomial.eval x p < 0 ↔ p.leadingCoeff < 0

The negative-sign form for an arbitrary irreducible quadratic.

theorem TauCeti.irreducible_quadratic_eval_mul_pos {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] [IsRealClosed R] {p : Polynomial R} (hp : Irreducible p) (hdeg : p.natDegree = 2) (a b : R) : 0 < Polynomial.eval a p * Polynomial.eval b p

An irreducible quadratic has the same nonzero sign at any two points.