noncomputable def Hex.NumberTower.Norm.rawToComplex (levels : List Level) (a : Array ℚ) : ℂ

Interpret raw coordinates for a validated level list. The fallback is unreachable when the list comes from a Hex.NumberTower.

Equations

• Hex.NumberTower.Norm.rawToComplex levels a = (Option.map Hex.AlgebraicRoot.toComplex (Hex.NumberTower.RawEvaluation.evalCoords? levels a)).getD 0

theorem Hex.NumberTower.Norm.rawToComplex_eq_denote (levels : List Level) (a : Array ℚ) : rawToComplex levels a = LevelSemantics.denote levels a

The total raw evaluator agrees with direct mixed-radix denotation.

noncomputable def Hex.NumberTower.Norm.rawPolynomial (levels : List Level) (f : DensePoly (Arithmetic.Coeff levels)) : Polynomial ℂ

Interpret a raw lower-tower dense polynomial in Polynomial ℂ.

Equations

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

noncomputable def Hex.NumberTower.Norm.rawOuter (levels : List Level) (f : DensePoly (DensePoly (Arithmetic.Coeff levels))) : Polynomial (Polynomial ℂ)

Interpret an outer dense polynomial over raw lower-tower polynomials.

Equations

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

theorem Hex.NumberTower.Norm.raw_coeff_horner (levels : List Level) (coefficients : List (Arithmetic.Coeff levels)) (n : ℕ) : (List.foldr (fun (a : Arithmetic.Coeff levels) (value : Polynomial ℂ) => Polynomial.C (rawToComplex levels a.data) + Polynomial.X * value) 0 coefficients).coeff n = rawToComplex levels (coefficients.getD n 0).data

The Horner fold defining rawPolynomial has the expected coefficients: coefficient n is the complex denotation of the n-th raw coefficient, with 0 beyond the end.

theorem Hex.NumberTower.Norm.coeff_rawPolynomial (levels : List Level) (f : DensePoly (Arithmetic.Coeff levels)) (n : ℕ) : (rawPolynomial levels f).coeff n = rawToComplex levels (f.coeff n).data

Coefficients of a semantically interpreted raw polynomial are the denotations of its executable coefficients.

@[simp]

theorem Hex.NumberTower.Norm.rawPolynomial_zero (levels : List Level) : rawPolynomial levels 0 = 0

Raw semantic interpretation preserves the polynomial zero.

@[reducible]

noncomputable def Hex.NumberTower.Norm.coeffFieldPoly (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) : Field (Arithmetic.Coeff levels)

The transferred field with its zero projection pinned to the executable coefficient instance. This lets existing DensePoly values retain their instance-indexed type while the Mathlib laws are available locally.

Equations

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

@[implicit_reducible]

noncomputable def Hex.NumberTower.Norm.denseCommRing {R : Type u_1} [CommRing R] [DecidableEq R] : CommRing (DensePoly R)

Proof-local Mathlib ring laws for executable dense-polynomial operations.

Equations

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

noncomputable def Hex.NumberTower.Norm.lowerHom (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Arithmetic.Coeff lower →+* Arithmetic.Coeff (level :: lower)

Embed the canonical lower coefficient field as the constant block of the next extension. The construction is parameterized by top-level injectivity, which is exactly the hypothesis available inside the recursive Trager proof.

Equations

• Hex.NumberTower.Norm.lowerHom level lower hvalid hinjectiveTop = { toFun := Hex.NumberTower.LevelSemantics.liftCoeff level lower, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Hex.NumberTower.Norm.lowerHom_apply (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (a : Arithmetic.Coeff lower) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; (lowerHom level lower hvalid hinjectiveTop) a = LevelSemantics.liftCoeff level lower a

The lower-coefficient embedding lowerHom acts by lifting a raw lower-tower coefficient into the constant block of the extended tower.

theorem Hex.NumberTower.Norm.topGenerator_denote (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) : LevelSemantics.coeffDenote (level :: lower) (Factor.topGenerator level lower) = level.root.toComplex

The executable representative of the newest generator denotes the selected root. In relative degree one the generator is already the lower constant forced by the monic linear relation.

theorem Hex.NumberTower.Norm.topGenerator_evalAt (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, LevelSemantics.denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) : LevelSemantics.evalAt level lower x (Factor.topGenerator level lower).data = x

The executable newest-generator representative evaluates to any root of the current monic relation, including the relative-degree-one encoding.

noncomputable def Hex.NumberTower.Norm.rawPolynomialHom (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) : DensePoly (Arithmetic.Coeff levels) →+* Polynomial ℂ

Coefficientwise semantic interpretation is a ring homomorphism once the canonical lower tower has its transferred field structure.

Equations

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

theorem Hex.NumberTower.Norm.rawPolynomialHom_apply (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) : (rawPolynomialHom levels hvalid hinjective hinv) f = rawPolynomial levels f

The bundled ring homomorphism rawPolynomialHom agrees pointwise with the direct Horner interpretation rawPolynomial, so the latter inherits all homomorphism laws.

theorem Hex.NumberTower.Norm.rawPolynomial_eq_map (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) : rawPolynomial levels f = Polynomial.map (LevelSemantics.coeffHom levels hvalid hinjective hinv) (HexPolyMathlib.toPolynomial f)

Raw polynomial interpretation is coefficientwise mapping through the fixed complex denotation.

theorem Hex.NumberTower.Norm.rawPolynomial_injective (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) : Function.Injective (rawPolynomial levels)

Injective coefficient denotation makes raw polynomial interpretation injective coefficientwise.

@[simp]

theorem Hex.NumberTower.Norm.rawPolynomial_one (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) : rawPolynomial levels 1 = 1

Semantic interpretation sends the executable one polynomial to 1.

@[simp]

theorem Hex.NumberTower.Norm.rawPolynomial_mul (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f g : DensePoly (Arithmetic.Coeff levels)) : rawPolynomial levels (f * g) = rawPolynomial levels f * rawPolynomial levels g

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

@[simp]

theorem Hex.NumberTower.Norm.rawPolynomial_C (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (a : Arithmetic.Coeff levels) : rawPolynomial levels (DensePoly.C a) = Polynomial.C (LevelSemantics.coeffDenote levels a)

A constant executable polynomial denotes the corresponding constant complex polynomial.

noncomputable def Hex.NumberTower.Norm.conjugateMap (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective (level :: lower)) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, LevelSemantics.denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) : Arithmetic.Coeff (level :: lower) →+* ℂ

Evaluation at a conjugate root, bundled using the proof-local field whose zero agrees definitionally with the executable coefficient carrier.

Equations

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

@[simp]

theorem Hex.NumberTower.Norm.conjugateMap_apply (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective (level :: lower)) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, LevelSemantics.denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) (a : Arithmetic.Coeff (level :: lower)) : (conjugateMap level lower hvalid hinjective x hrelation) a = LevelSemantics.evalAt level lower x a.data

noncomputable def Hex.NumberTower.Norm.conjugatePolynomial (level : Level) (lower : List Level) (x : ℂ) (f : Array (Array ℚ)) : Polynomial ℂ

Interpret raw top-tower polynomial coefficients at one conjugate of the newest generator.

Equations

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

theorem Hex.NumberTower.Norm.conjugate_coeff_horner (level : Level) (lower : List Level) (x : ℂ) (coefficients : List (Array ℚ)) (n : ℕ) : (List.foldr (fun (a : Array ℚ) (value : Polynomial ℂ) => Polynomial.C (LevelSemantics.evalAt level lower x a) + Polynomial.X * value) 0 coefficients).coeff n = LevelSemantics.evalAt level lower x (coefficients.getD n #[])

The Horner fold defining conjugatePolynomial has the expected coefficients: coefficient n evaluates the n-th raw coefficient at the conjugate x, with 0 beyond the end.

theorem Hex.NumberTower.Norm.coeff_conjugatePolynomial (level : Level) (lower : List Level) (x : ℂ) (f : Array (Array ℚ)) (n : ℕ) : (conjugatePolynomial level lower x f).coeff n = LevelSemantics.evalAt level lower x (f.getD n #[])

Coefficients of the conjugate interpretation are the conjugate evaluations of the raw coefficient blocks.

theorem Hex.NumberTower.Norm.conjugatePolynomial_eq_map (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective (level :: lower)) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, LevelSemantics.denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) (f : Array (Array ℚ)) : conjugatePolynomial level lower x f = Polynomial.map (conjugateMap level lower hvalid hinjective x hrelation) (HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) f))

Conjugate coefficient interpretation is coefficientwise mapping through the corresponding ring homomorphism.

theorem Hex.NumberTower.Norm.rawPolynomial_derivative (levels : List Level) (f : DensePoly (Arithmetic.Coeff levels)) : rawPolynomial levels (derivative levels f) = Polynomial.derivative (rawPolynomial levels f)

The runtime-indexed derivative has the ordinary formal derivative after coefficient denotation.

theorem Hex.NumberTower.Norm.derivative_eq (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (Arithmetic.Coeff levels)) : derivative levels f = f.derivative

Under the transferred coefficient field, the custom runtime-indexed derivative is the ordinary executable dense derivative.

theorem Hex.NumberTower.Norm.isSquarefree_iff (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : Array (Array ℚ)) : isSquarefree levels f = true ↔ Squarefree (rawPolynomial levels (Factor.rawPoly levels f))

The executable gcd-based squarefreeness test is exactly ordinary polynomial squarefreeness after semantic coefficient interpretation.

theorem Hex.NumberTower.Norm.outer_coeff_horner (levels : List Level) (coefficients : List (DensePoly (Arithmetic.Coeff levels))) (n : ℕ) : (List.foldr (fun (a : DensePoly (Arithmetic.Coeff levels)) (value : Polynomial (Polynomial ℂ)) => Polynomial.C (rawPolynomial levels a) + Polynomial.X * value) 0 coefficients).coeff n = rawPolynomial levels (coefficients.getD n 0)

The Horner fold defining rawOuter has the expected coefficients: coefficient n is the raw interpretation of the n-th inner polynomial, with 0 beyond the end.

theorem Hex.NumberTower.Norm.dense_array_toList_getD (levels : List Level) (coefficients : Array (DensePoly (Arithmetic.Coeff levels))) (n : ℕ) : coefficients.toList.getD n 0 = coefficients.getD n 0

Defaulted indexing through Array.toList agrees with defaulted array indexing for inner dense polynomials.

theorem Hex.NumberTower.Norm.coeff_rawOuter (levels : List Level) (f : DensePoly (DensePoly (Arithmetic.Coeff levels))) (n : ℕ) : (rawOuter levels f).coeff n = rawPolynomial levels (f.coeff n)

Coefficients of the outer interpretation are the raw interpretations of the executable inner coefficients.

theorem Hex.NumberTower.Norm.rawOuter_eq_map (levels : List Level) (hvalid : LevelsValid levels) (hinjective : LevelSemantics.DenoteInjective levels) (hinv : ∀ (a : Arithmetic.Coeff levels), LevelSemantics.coeffDenote levels a⁻¹ = (LevelSemantics.coeffDenote levels a)⁻¹) (f : DensePoly (DensePoly (Arithmetic.Coeff levels))) : rawOuter levels f = Polynomial.map (rawPolynomialHom levels hvalid hinjective hinv) (HexPolyMathlib.toPolynomial f)

The outer interpretation is coefficientwise mapping through rawPolynomialHom, exposing rawOuter to Polynomial.map lemmas.

noncomputable def Hex.NumberTower.Norm.outerEvalHom (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Polynomial (DensePoly (Arithmetic.Coeff lower)) →+* Polynomial (Arithmetic.Coeff (level :: lower))

Specialize a polynomial in the outer elimination variable at the newest generator, while embedding its lower[X] coefficients into (level :: lower)[X].

Equations

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

noncomputable def Hex.NumberTower.Norm.outerEval (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (g : DensePoly (DensePoly (Arithmetic.Coeff lower))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Polynomial (Arithmetic.Coeff (level :: lower))

Evaluate an outer polynomial in the newest generator while embedding its lower[X] coefficients into (level :: lower)[X].

Equations

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

theorem Hex.NumberTower.Norm.outerEvalHom_apply (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (g : DensePoly (DensePoly (Arithmetic.Coeff lower))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; (outerEvalHom level lower hvalid hinjectiveTop) (HexPolyMathlib.toPolynomial g) = outerEval level lower hvalid hinjectiveTop g

The evaluation homomorphism outerEvalHom acts by mapping inner coefficients through the lower embedding and evaluating the outer variable at the constant top generator.

theorem Hex.NumberTower.Norm.outerEval_map (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (g : DensePoly (DensePoly (Arithmetic.Coeff lower))) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; Polynomial.map (LevelSemantics.coeffHom (level :: lower) hvalid hinjectiveTop hinvTop) (outerEval level lower hvalid hinjectiveTop g) = Polynomial.eval (Polynomial.C level.root.toComplex) (rawOuter lower g)

Mapping outerEval into the fixed complex embedding is specialization of the semantic outer polynomial at the selected root.

theorem Hex.NumberTower.Norm.eval_liftCoefficient (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (a : Array ℚ) (x : ℂ) : Polynomial.eval (Polynomial.C x) (rawOuter lower (liftCoefficient level lower a)) = Polynomial.C (LevelSemantics.evalAt level lower x a)

After interpreting the lower tower, a lifted top-level coefficient specializes at a conjugate root to the corresponding constant polynomial.

theorem Hex.NumberTower.Norm.eval_shiftBase (lower : List Level) (hvalid : LevelsValid lower) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (c : ℤ) (x : ℂ) : have base := DensePoly.ofCoeffs #[DensePoly.monomial 1 1, DensePoly.C (Arithmetic.Coeff.ofData lower #[-↑c])]; Polynomial.eval (Polynomial.C x) (rawOuter lower base) = Polynomial.X - Polynomial.C (↑c * x)

The linear substitution base specializes to X - c·x at the chosen conjugate x.

theorem Hex.NumberTower.Norm.eval_shiftedOuter (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) (f : Array (Array ℚ)) (c : ℤ) (x : ℂ) : Polynomial.eval (Polynomial.C x) (rawOuter lower (shiftedOuter level lower f c)) = (conjugatePolynomial level lower x f).comp (Polynomial.X - Polynomial.C (↑c * x))

Specializing the shifted bivariate input at a conjugate gives ordinary polynomial composition by X - c·x.

theorem Hex.NumberTower.Norm.rawOuter_defining (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : LevelSemantics.DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), LevelSemantics.coeffDenote lower a⁻¹ = (LevelSemantics.coeffDenote lower a)⁻¹) : rawOuter lower (definingOuter level lower) = Polynomial.map Polynomial.C (rawPolynomial lower (Arithmetic.Coeff.relation level lower))

The executable outer defining polynomial is the constant-coefficient lift of the ordinary lower-field relation.

theorem Hex.NumberTower.Norm.outerEval_defining (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; outerEval level lower hvalid hinjectiveTop (definingOuter level lower) = 0

The outer defining polynomial vanishes when specialized at the executable top generator.

theorem Hex.NumberTower.Norm.rawPoly_polyCoords (levels : List Level) (f : DensePoly (Arithmetic.Coeff levels)) : Factor.rawPoly levels (Factor.polyCoords f) = f

Rebuilding a raw dense polynomial from its flattened coordinate arrays is the identity: Factor.polyCoords is a section of Factor.rawPoly.

theorem Hex.NumberTower.Norm.conjugatePolynomial_shiftTop (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, LevelSemantics.denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) (f : Array (Array ℚ)) (c : ℤ) : have hinvTop := ⋯; conjugatePolynomial level lower x (Factor.shiftTop level lower f c) = (conjugatePolynomial level lower x f).comp (Polynomial.X - Polynomial.C (↑c * x))

Shifting at the executable newest generator specializes at every conjugate to the corresponding scalar affine shift.

theorem Hex.NumberTower.Norm.outerEval_shifted (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjectiveTop : LevelSemantics.DenoteInjective (level :: lower)) (f : Array (Array ℚ)) (c : ℤ) : have hinjectiveLower := ⋯; have hinvLower := ⋯; have hinvTop := ⋯; outerEval level lower hvalid hinjectiveTop (shiftedOuter level lower f c) = HexPolyMathlib.toPolynomial (Factor.rawPoly (level :: lower) (Factor.shiftTop level lower f c))

Specializing the shifted outer presentation at the executable generator is exactly the current-level shifted polynomial.