def Hex.QAdjoin.ballSign? (ball : DyadicComplexBall) : Option Int

A disc separated from the imaginary axis fixes the sign of its real part.

Equations

• Hex.QAdjoin.ballSign? ball = if ball.radius < ball.re then some 1 else if ball.re < -ball.radius then some (-1) else none

def Hex.QAdjoin.SignApprox.initial? (generator : AlgebraicNumber) (value : QAdjoin generator) : Option Int

Read the existing enclosure with a minimum of sixteen coefficient bits.

Equations

• Hex.QAdjoin.SignApprox.initial? generator value = Hex.QAdjoin.ballSign? (Hex.PolyQuot.evalRatBall value.coeffs generator.rep.val.square (max 16 generator.rep.val.square.prec))

def Hex.QAdjoin.SignApprox.refined? (generator : AlgebraicNumber) (value : QAdjoin generator) : Option Int

A modest absolute-precision probe before constructing an evaluation eliminant.

Equations

• Hex.QAdjoin.SignApprox.refined? generator value = Hex.QAdjoin.ballSign? (Hex.PolyQuot.approx value generator.rep ⋯ 32).snd

def Hex.QAdjoin.SignApprox.eliminant (generator : AlgebraicNumber) (value : QAdjoin generator) : ZPoly

An integer polynomial vanishing at the selected coordinate value.

Equations

• Hex.QAdjoin.SignApprox.eliminant generator value = Hex.PolyQuot.Roots.normEliminant (Hex.DensePoly.ofList [-value, 1])

def Hex.QAdjoin.SignApprox.endpoint? (generator : AlgebraicNumber) (value : QAdjoin generator) : Option Int

The finite reciprocal-Cauchy endpoint. Approximation guard bits already absorb Horner error amplification, so the output-radius majorant is one.

Equations

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

def Hex.QAdjoin.signApprox? {generator : AlgebraicNumber} (value : QAdjoin generator) : Option Int

Checked sign in the generator's real embedding; reject nonreal generators.

Equations

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

def Hex.QAdjoin.signApprox {generator : AlgebraicNumber} (value : QAdjoin generator) (_real : generator.isReal = true) : Int

Total sign for a real generator. The companion proves the fallback unreachable.

Equations

• value.signApprox _real = value.signApprox?.getD (Hex.panicWith 0 "signApprox: finite precision endpoint failed")

def Hex.orderOfSign (sign : Int) : Ordering

Interpret an integer sign as comparison with zero.

Equations

• Hex.orderOfSign sign = compare sign 0