noncomputable def Hex.NumberTower.toPolynomial (T : NumberTower) (f : T.Poly) : Polynomial ℂ

Interpret a dense tower polynomial through the fixed complex embedding.

Equations

• T.toPolynomial f = Array.foldr (fun (a : T.Elem) (value : Polynomial ℂ) => Polynomial.C (T.toComplex a) + Polynomial.X * value) 0 (Hex.DensePoly.toArray f)

theorem Hex.NumberTower.coeff_toPolynomial (T : NumberTower) (f : T.Poly) (n : ℕ) : (T.toPolynomial f).coeff n = T.toComplex (DensePoly.coeff f n)

Semantic tower-polynomial coefficients agree with executable access.

theorem Hex.NumberTower.toPolynomial_eq_polynomial (T : NumberTower) (f : T.Poly) : T.toPolynomial f = LevelSemantics.polynomial T.levels.toList (Array.map coeffs (DensePoly.toArray f))

The tower-polynomial interpretation is the raw level interpretation of its flattened coefficient arrays.

theorem Hex.NumberTower.toPolynomial_eq_map (T : NumberTower) (f : T.Poly) : T.toPolynomial f = Polynomial.map T.embedding (HexPolyMathlib.toPolynomial f)

Tower-polynomial interpretation is coefficientwise mapping through the certified complex embedding.

theorem Hex.NumberTower.toPolynomial_injective (T : NumberTower) : Function.Injective T.toPolynomial

The fixed complex interpretation distinguishes executable tower polynomials coefficientwise.

@[simp]

theorem Hex.NumberTower.natDegree_toPolynomial (T : NumberTower) (f : T.Poly) : (T.toPolynomial f).natDegree = DensePoly.natDegree f

Semantic interpretation preserves the executable polynomial degree.

@[simp]

theorem Hex.NumberTower.toPolynomial_zero (T : NumberTower) : T.toPolynomial 0 = 0

Semantic interpretation sends the executable zero polynomial to 0.

@[simp]

theorem Hex.NumberTower.toPolynomial_one (T : NumberTower) : T.toPolynomial 1 = 1

Semantic interpretation sends the executable one polynomial to 1.

@[simp]

theorem Hex.NumberTower.toPolynomial_add (T : NumberTower) (f g : T.Poly) : T.toPolynomial (f + g) = T.toPolynomial f + T.toPolynomial g

Semantic interpretation turns executable tower-polynomial addition into addition in Polynomial ℂ.

@[simp]

theorem Hex.NumberTower.toPolynomial_mul (T : NumberTower) (f g : T.Poly) : T.toPolynomial (f * g) = T.toPolynomial f * T.toPolynomial g

Semantic interpretation turns executable tower-polynomial multiplication into multiplication in Polynomial ℂ.

@[simp]

theorem Hex.NumberTower.toPolynomial_C (T : NumberTower) (a : T.Elem) : T.toPolynomial (DensePoly.C a) = Polynomial.C (T.toComplex a)

Semantic interpretation sends an executable constant polynomial to the constant polynomial on the interpreted coefficient.