theorem Hex.QAdjoin.ballSign?_spec (ball : DyadicComplexBall) (z : ℂ) (sign : ℤ) (mem : z ∈ ball.set) (accepted : ballSign? ball = some sign) : sign = ↑(SignType.sign z.re)

A successful disc probe gives the mathematical sign of the real part.

theorem Hex.QAdjoin.signApprox?_spec {generator : AlgebraicNumber} (value : QAdjoin generator) (real : generator.isReal = true) (sign : ℤ) (accepted : value.signApprox? = some sign) : sign = ↑(SignType.sign (PolyQuot.toComplex value generator.rep ⋯).re)

Successful checked signs agree with the selected real embedding.

theorem Hex.QAdjoin.signApprox?_isSome {generator : AlgebraicNumber} (value : QAdjoin generator) (real : generator.isReal = true) : value.signApprox?.isSome = true

The checked algorithm succeeds for every coordinate of a real generator.

theorem Hex.QAdjoin.signApprox_spec {generator : AlgebraicNumber} (value : QAdjoin generator) (real : generator.isReal = true) : value.signApprox real = ↑(SignType.sign (PolyQuot.toComplex value generator.rep ⋯).re)

The total operation has no reachable fallback on its stated domain.

theorem Hex.QAdjoin.signApprox_eq {generator : AlgebraicNumber} (value : QAdjoin generator) (real : generator.isReal = true) : orderOfSign (value.signApprox real) = value.toAlgebraicNumber.realCompare 0

The interval strategy agrees with canonical comparison to zero.