theorem Hex.QAdjoin.powerTable_eq (a : AlgebraicNumber) : AlgebraicPoly.Common.powers? a (2 * DensePoly.natDegree a.p - 2) = some (powerTable a)

The total power-table wrapper is its successful checked computation.

theorem Hex.QAdjoin.powerTable_spec (a : AlgebraicNumber) : (powerTable a).size = 2 * AlgebraicPoly.Common.degree a - 1 ∧ ∀ (i : ℕ) (hi : i < (powerTable a).size), (powerTable a)[i].toComplex = a.toComplex ^ i

The shared table has the consecutive powers needed by the trace pairing.

theorem Hex.QAdjoin.value_mem {a : AlgebraicNumber} (c : QAdjoin a) : PolyQuot.toComplex c a.rep ⋯ ∈ ℚ⟮a.toComplex⟯

Rational power-basis coordinates lie in the chosen simple extension.

theorem Hex.QAdjoin.value_real {a : AlgebraicNumber} (c : QAdjoin a) (ha : a.isReal = true) : (PolyQuot.toComplex c a.rep ⋯).im = 0

Every coordinate value in a real-generated field is real.

theorem Hex.QAdjoin.ofAlgebraic?_eq (a b : AlgebraicNumber) : ofAlgebraic? a b = AlgebraicPoly.Common.coordinates? a b (powerTable a)

The real-field rejection skips work without changing coordinate recovery.

theorem Hex.QAdjoin.ofAlgebraic?_sound (a b : AlgebraicNumber) {c : QAdjoin a} (h : ofAlgebraic? a b = some c) : c.toAlgebraicNumber = b

Successful conversion recovers exactly the original canonical number.

theorem Hex.QAdjoin.ofAlgebraic?_isSome_iff (a b : AlgebraicNumber) : (ofAlgebraic? a b).isSome = true ↔ b.toComplex ∈ ℚ⟮a.toComplex⟯

Conversion succeeds exactly for elements of the chosen field.

@[simp]

theorem Hex.QAdjoin.ofAlgebraics?_size (a : AlgebraicNumber) (bs : Array AlgebraicNumber) : (ofAlgebraics? a bs).size = bs.size

@[simp]

theorem Hex.QAdjoin.ofAlgebraics?_get (a : AlgebraicNumber) (bs : Array AlgebraicNumber) (i : ℕ) (hi : i < bs.size) : (ofAlgebraics? a bs)[i] = ofAlgebraic? a bs[i]

Batch conversion preserves the single-value membership decision at each index.

theorem Hex.QAdjoin.common_spec (bs : Array AlgebraicNumber) : (common bs).entries.size = bs.size ∧ ∀ (i : ℕ) (hi : i < bs.size) (hp : i < (common bs).entries.size), (common bs).entries[i].toAlgebraicNumber = bs[i]

The common presentation preserves length and every input value.

@[simp]

theorem Hex.QAdjoin.common_size (bs : Array AlgebraicNumber) : (common bs).entries.size = bs.size

theorem Hex.QAdjoin.common_get (bs : Array AlgebraicNumber) (i : ℕ) (hi : i < bs.size) : (common bs).entries[i].toAlgebraicNumber = bs[i]

Each common-field coordinate converts back to its original input.