theorem Hex.QAdjoin.ballSign?_isSome (ball : DyadicComplexBall) (z : ℂ) (mem : z ∈ ball.set) (small : 2 * ball.realRadius < |z.re|) : (ballSign? ball).isSome = true

A real-part enclosure narrower than half the value's magnitude determines its sign.

theorem Hex.QAdjoin.SignApprox.eliminant_spec (generator : AlgebraicNumber) (value : QAdjoin generator) : eliminant generator value ≠ 0 ∧ (HexRootsTheory.toPolyℂ (eliminant generator value)).IsRoot (PolyQuot.toComplex value generator.rep ⋯)

The evaluation eliminant is nonzero and vanishes at the selected coordinate.

theorem Hex.QAdjoin.SignApprox.endpoint?_isSome (generator : AlgebraicNumber) (value : QAdjoin generator) (realGenerator : generator.isReal = true) (large : 1 < value.coeffs.size) : (endpoint? generator value).isSome = true

The finite endpoint always separates a nonconstant coordinate from zero.