def HexRealRootsMathlib.TwoCircle.InTwoCircle (a b : ℝ) (w : ℂ) : Prop

The two-circle region of the interval (a, b), as an algebraic condition on the Möbius seed s = (w − a)·conj(b − w): w is inside when 0 < s.re or 3·s.re² < s.im². This is the open region; its complement is the closed sector condition s.re ≤ 0 ∧ s.im² ≤ 3·s.re².

Equations

• One or more equations did not get rendered due to their size.

def HexRealRootsMathlib.TwoCircle.sector : Set ℂ

The closed sector S = {z | z.re ≤ −‖z‖/2} (half-angle 2π/3), the target of the Möbius image. Classically written with Complex.abs; here the modulus is the norm ‖·‖.

Equations

• HexRealRootsMathlib.TwoCircle.sector = {z : ℂ | z.re ≤ -‖z‖ / 2}

theorem HexRealRootsMathlib.TwoCircle.mem_sector {z : ℂ} : z ∈ sector ↔ z.re ≤ -‖z‖ / 2

Membership in the closed sector unfolds to the scalar inequality. Exported so consumers can bridge this sector to Polynomial.sector (the identical set in the sign-variation development) without unfolding the opaque def across modules.

theorem HexRealRootsMathlib.TwoCircle.seed_re (a b : ℝ) (w : ℂ) : ((w - ↑a) * (starRingEnd ℂ) (↑b - w)).re = (w.re - a) * (b - w.re) - w.im ^ 2

Real part of the Möbius seed s = (w − a)·conj(b − w).

theorem HexRealRootsMathlib.TwoCircle.seed_im (a b : ℝ) (w : ℂ) : ((w - ↑a) * (starRingEnd ℂ) (↑b - w)).im = w.im * (b - a)

Imaginary part of the Möbius seed s = (w − a)·conj(b − w).

theorem HexRealRootsMathlib.TwoCircle.sector_re_iff (p q : ℝ) : p ≤ -√(p ^ 2 + q ^ 2) / 2 ↔ p ≤ 0 ∧ q ^ 2 ≤ 3 * p ^ 2

Sector membership as a scalar inequality: for real p, q, p ≤ −√(p²+q²)/2 ↔ p ≤ 0 ∧ q² ≤ 3p². This is the exact boundary matching that makes the region open and the sector closed.

theorem HexRealRootsMathlib.TwoCircle.not_inTwoCircle_iff_mem_sector (a b : ℝ) (w : ℂ) (hw : w ≠ ↑b) : ¬InTwoCircle a b w ↔ (w - ↑a) / (↑b - w) ∈ sector

Möbius-image characterisation of the region complement. For w ≠ b, the point w is outside the two-circle region iff its Möbius image (w − a)/(b − w) lies in the closed sector S = {z | z.re ≤ −‖z‖/2}.

theorem HexRealRootsMathlib.TwoCircle.not_inTwoCircle_self (a b : ℝ) : ¬InTwoCircle a b ↑b

The right endpoint b is not in the region (the seed vanishes there); the Möbius image is undefined, so b-roots are treated separately.

theorem HexRealRootsMathlib.TwoCircle.ball_bound_real {h y2 T : ℝ} (hy2 : 0 ≤ y2) (hyT : y2 ≤ T) (hdisj : 0 < h ^ 2 / 4 - T ∨ 3 * (h ^ 2 / 4 - T) ^ 2 < h ^ 2 * y2) : T ≤ 3 * h ^ 2 / 4

Scalar form of the ball bound: from the region disjunction on s.re = h²/4 − T and s.im² = h²·y², the squared distance T is at most 3h²/4.

theorem HexRealRootsMathlib.TwoCircle.dist_le (a b : ℝ) (w : ℂ) (hab : a ≤ b) (hw : InTwoCircle a b w) : dist w ↑((a + b) / 2) ≤ √3 * (b - a) / 2

Ball bound. The two-circle region of (a, b) (a ≤ b) is contained in the closed ball of radius √3·(b−a)/2 about the midpoint (a+b)/2.

theorem HexRealRootsMathlib.TwoCircle.inTwoCircle_conj (a b : ℝ) (w : ℂ) : InTwoCircle a b ((starRingEnd ℂ) w) ↔ InTwoCircle a b w

Conjugation symmetry. The two-circle region is invariant under complex conjugation (the seed conjugates, so s.re is preserved and s.im² is unchanged).

theorem HexRealRootsMathlib.TwoCircle.inTwoCircle_ofReal (a b w : ℝ) (h1 : a < w) (h2 : w < b) : InTwoCircle a b ↑w

Real membership. Every real point of the open interval (a, b) lies in the two-circle region.

noncomputable def HexRealRootsMathlib.TwoCircle.centrePos (a b : ℝ) : ℂ

The upper disc centre (a+b)/2 + i·(b−a)/(2√3).

Equations

• HexRealRootsMathlib.TwoCircle.centrePos a b = ↑((a + b) / 2) + Complex.I * ↑((b - a) / (2 * √3))

noncomputable def HexRealRootsMathlib.TwoCircle.centreNeg (a b : ℝ) : ℂ

The lower disc centre (a+b)/2 − i·(b−a)/(2√3).

Equations

• HexRealRootsMathlib.TwoCircle.centreNeg a b = ↑((a + b) / 2) - Complex.I * ↑((b - a) / (2 * √3))

noncomputable def HexRealRootsMathlib.TwoCircle.discRadius (a b : ℝ) : ℝ

The common disc radius (b−a)/√3.

Equations

• HexRealRootsMathlib.TwoCircle.discRadius a b = (b - a) / √3

@[simp]

theorem HexRealRootsMathlib.TwoCircle.centrePos_re (a b : ℝ) : (centrePos a b).re = (a + b) / 2

@[simp]

theorem HexRealRootsMathlib.TwoCircle.centrePos_im (a b : ℝ) : (centrePos a b).im = (b - a) / (2 * √3)

@[simp]

theorem HexRealRootsMathlib.TwoCircle.centreNeg_re (a b : ℝ) : (centreNeg a b).re = (a + b) / 2

@[simp]

theorem HexRealRootsMathlib.TwoCircle.centreNeg_im (a b : ℝ) : (centreNeg a b).im = -((b - a) / (2 * √3))

theorem HexRealRootsMathlib.TwoCircle.dist_lt_discRadius_iff (a b : ℝ) (w c : ℂ) (hρ : 0 < discRadius a b) : dist w c < discRadius a b ↔ (w.re - c.re) ^ 2 + (w.im - c.im) ^ 2 < (b - a) ^ 2 / 3

dist w c < discRadius a b as a squared coordinate inequality.

theorem HexRealRootsMathlib.TwoCircle.region_iff_disc_real (R c : ℝ) : 0 < R ∨ R ^ 2 < c ^ 2 ↔ -R < c ∨ -R < -c

The pure-scalar core of the disc characterisation: for reals R, c, the open-region disjunction on R (a stand-in for s.re) matches the union of the two half-plane conditions coming from the two discs.

theorem HexRealRootsMathlib.TwoCircle.inTwoCircle_iff_disc (a b : ℝ) (w : ℂ) (hab : a ≤ b) : InTwoCircle a b w ↔ dist w (centrePos a b) < discRadius a b ∨ dist w (centreNeg a b) < discRadius a b

Disc characterisation. The algebraic region is exactly the classical union of the two open discs through a and b with centres (a+b)/2 ± i·(b−a)/(2√3) and radius (b−a)/√3.