def Hex.QAdjoin.powerTable (a : AlgebraicNumber) : Array AlgebraicNumber

Consecutive powers used by coordinate recovery. Certification cannot fail.

Equations

• Hex.QAdjoin.powerTable a = (Hex.AlgebraicPoly.Common.powers? a (2 * Hex.DensePoly.natDegree a.p - 2)).getD (Hex.panicWith #[] "QAdjoin: power table certification failed")

def Hex.QAdjoin.ofAlgebraic? (a b : AlgebraicNumber) : Option (QAdjoin a)

Express b in the power basis of a, or return none when b ∉ ℚ(a). This does not enlarge the chosen field. A real generator rejects nonreal values before coordinate recovery.

Equations

• Hex.QAdjoin.ofAlgebraic? a b = if (a.isReal && !b.isReal) = true then none else Hex.AlgebraicPoly.Common.coordinates? a b (Hex.QAdjoin.powerTable a)

def Hex.QAdjoin.ofAlgebraics? (a : AlgebraicNumber) (bs : Array AlgebraicNumber) : Array (Option (QAdjoin a))

Convert a collection to one chosen field, sharing its power table. The output preserves input order and records nonmembership separately for each entry.

Equations

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

structure Hex.QAdjoin.Presentation : Type

One primitive generator and the input values in its rational power basis. The public entries name describes arbitrary input collections independently of AlgebraicPoly.Common.Presentation, whose coefficients field serves polynomial construction.

• generator : AlgebraicNumber
• entries : Array (QAdjoin self.generator)

def Hex.QAdjoin.checkPair? (theta alpha gamma : AlgebraicNumber) (coordinates : QAdjoin gamma × QAdjoin gamma) : Option (QAdjoin gamma × QAdjoin gamma)

Internal check of proposed coordinates against both selected canonical values.

Equations

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

def Hex.QAdjoin.recoverShift? (theta alpha gamma : AlgebraicNumber) (shift : Int) : Option (QAdjoin gamma × QAdjoin gamma)

Recover both inputs in a primitive presentation arising from a nonzero integer shift. The polynomial gcd gives candidate coordinates; canonical algebraic equality checks the chosen embeddings.

Equations

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

def Hex.QAdjoin.presentShift? (theta alpha gamma : AlgebraicNumber) (shift : Int) : Option Presentation

Internal packaging of a checked pair at one proposed generator.

Equations

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

def Hex.QAdjoin.fastPair? (theta alpha : AlgebraicNumber) : Option Presentation

When shift one has the full product degree, recover and check both input coordinates through its primitive generator.

Equations

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

def Hex.QAdjoin.commonFallback (bs : Array AlgebraicNumber) : Presentation

Internal trace-pairing fallback when the fast pair conversion does not apply.

Equations

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

def Hex.QAdjoin.common (bs : Array AlgebraicNumber) : Presentation

Find one number field containing every input, preserving order and duplicates. Empty and all-zero collections use ℚ(0) = ℚ. The primitive-element search can be expensive; subsequent arithmetic in the resulting QAdjoin uses rational coordinates without further root isolation.

Equations

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