theorem Hex.NumberTower.LevelSemantics.denseMap_zero (lower : List Level) (x : ℂ) (hvalid : LevelsValid lower) (hinjective : DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), coeffDenote lower a⁻¹ = (coeffDenote lower a)⁻¹) : denseMap lower x hvalid hinjective hinv 0 = 0

Dense evaluation sends zero to zero.

def Hex.NumberTower.LevelSemantics.denseBlocks (degree : ℕ) {lower : List Level} (f : DensePoly (Arithmetic.Coeff lower)) : Array (Array ℚ)

The first prescribed coefficient range of a dense polynomial, exposed as lower-tower coordinate blocks.

Equations

• Hex.NumberTower.LevelSemantics.denseBlocks degree f = (Vector.ofFn fun (i : Fin degree) => (f.coeff ↑i).data).toArray

def Hex.NumberTower.LevelSemantics.liftDense (level : Level) (lower : List Level) (f : DensePoly (Arithmetic.Coeff lower)) : Arithmetic.Coeff (level :: lower)

Embed a lower-coefficient dense polynomial as one canonical coefficient at the extended level.

Equations

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

theorem Hex.NumberTower.LevelSemantics.coeffDenote_liftDense (level : Level) (lower : List Level) (f : DensePoly (Arithmetic.Coeff lower)) : coeffDenote (level :: lower) (liftDense level lower f) = denseEval lower level.root.toComplex level.degree f

Dense-polynomial coefficient embedding denotes its finite evaluation.

theorem Hex.NumberTower.LevelSemantics.denote_flatten_dense (level : Level) (lower : List Level) (f : DensePoly (Arithmetic.Coeff lower)) : denote (level :: lower) (Arithmetic.flattenBlocks level.degree (levelsDim lower) (List.map (fun (i : ℕ) => (f.coeff i).data) (List.range level.degree)).toArray) = denseEval lower level.root.toComplex level.degree f

Flattening an explicit range of dense coefficients denotes the prescribed finite dense evaluation.

theorem Hex.NumberTower.LevelSemantics.dense_eq_zero_of_eval (level : Level) (lower : List Level) (hinjective : DenoteInjective (level :: lower)) (f : DensePoly (Arithmetic.Coeff lower)) (hdegree : f.natDegree < level.degree) (heval : denseEval lower level.root.toComplex level.degree f = 0) : f = 0

Injective extended-level denotation rules out every nonzero vanishing dense polynomial below the defining degree.

theorem Hex.NumberTower.LevelSemantics.denseEval_value (level : Level) (lower : List Level) (a : Array ℚ) : denseEval lower level.root.toComplex level.degree (Arithmetic.Coeff.value level lower a) = denote (level :: lower) a

The inversion input polynomial evaluates to the denotation of its top-level coordinate array.

theorem Hex.NumberTower.LevelSemantics.denseEval_relation (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) : denseEval lower level.root.toComplex (level.degree + 1) (Arithmetic.Coeff.relation level lower) = 0

The executable monic level relation evaluates to zero at the stored root.

theorem Hex.NumberTower.LevelSemantics.value_degree_lt (level : Level) (lower : List Level) (a : Array ℚ) (hdegree : 0 < level.degree) : (Arithmetic.Coeff.value level lower a).natDegree < level.degree

The inversion input polynomial lies strictly below the current defining degree.

def Hex.NumberTower.LevelSemantics.Separates (level : Level) (lower : List Level) : Prop

Evaluation at the selected generator distinguishes all lower-coefficient polynomials below the defining degree. This is the exact semantic consequence of irreducibility needed to construct the next tower embedding.

Equations

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

theorem Hex.NumberTower.LevelSemantics.DenoteInjective.nil : DenoteInjective []

Rational fixed-width coefficients have unique complex denotation.

theorem Hex.NumberTower.LevelSemantics.DenoteInjective.cons (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hseparates : Separates level lower) : DenoteInjective (level :: lower)

Separating evaluation at one level extends injectivity of the lower fixed embedding to injectivity of the next canonical coefficient carrier.

theorem Hex.NumberTower.LevelSemantics.relation_size (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) : (Arithmetic.Coeff.relation level lower).size = level.degree + 1

The executable relation retains its monic top coefficient and therefore has exactly defining degree plus one stored coefficients.

theorem Hex.NumberTower.LevelSemantics.relation_degree (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) : (Arithmetic.Coeff.relation level lower).natDegree = level.degree

The executable relation has its advertised defaulted degree.

theorem Hex.NumberTower.LevelSemantics.separates_of_irreducible (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hlowerInjective : DenoteInjective lower) (hlowerInv : ∀ (a : Arithmetic.Coeff lower), coeffDenote lower a⁻¹ = (coeffDenote lower a)⁻¹) : Irreducible (HexPolyMathlib.toPolynomial (Arithmetic.Coeff.relation level lower)) → Separates level lower

An irreducible defining relation that vanishes at the selected generator makes evaluation injective below its degree.

theorem Hex.NumberTower.LevelSemantics.relation_irreducible_of_injective (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : DenoteInjective (level :: lower)) (hlowerInjective : DenoteInjective lower) (hlowerInv : ∀ (a : Arithmetic.Coeff lower), coeffDenote lower a⁻¹ = (coeffDenote lower a)⁻¹) : Irreducible (HexPolyMathlib.toPolynomial (Arithmetic.Coeff.relation level lower))

Injectivity of canonical extended coordinates forces the monic level relation to be the minimal polynomial of the selected generator over the lower coefficient field.

theorem Hex.NumberTower.LevelSemantics.xgcdLeftMonic_size_one (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : DenoteInjective (level :: lower)) (hlowerInjective : DenoteInjective lower) (hinv : ∀ (b : Arithmetic.Coeff lower), coeffDenote lower b⁻¹ = (coeffDenote lower b)⁻¹) (a : Array ℚ) (ha : denote (level :: lower) a ≠ 0) : ((Arithmetic.Coeff.value level lower a).xgcdLeftMonic (Arithmetic.Coeff.relation level lower)).gcd.size = 1

For a nonzero input, the executable monic one-sided extended gcd with the defining relation returns a nonzero constant gcd.

theorem Hex.NumberTower.LevelSemantics.denote_xgcd_inverse (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hinjective : DenoteInjective (level :: lower)) (hlowerInjective : DenoteInjective lower) (hinv : ∀ (b : Arithmetic.Coeff lower), coeffDenote lower b⁻¹ = (coeffDenote lower b)⁻¹) (a : Array ℚ) (ha : denote (level :: lower) a ≠ 0) : have value := Arithmetic.Coeff.value level lower a; have relation := Arithmetic.Coeff.relation level lower; have result := value.xgcdLeftMonic relation; have c := result.gcd.leadingCoeff; have normalized := DensePoly.scale c⁻¹ result.left % relation; denote (level :: lower) (Arithmetic.flattenBlocks level.degree (levelsDim lower) (List.map (fun (i : ℕ) => (normalized.coeff i).data) (List.range level.degree)).toArray) = (denote (level :: lower) a)⁻¹

The normalized monic extended-gcd coefficient used by executable inversion denotes the reciprocal of a nonzero top-level coordinate array.

def Hex.NumberTower.LevelSemantics.liftCoeff (level : Level) (lower : List Level) (a : Arithmetic.Coeff lower) : Arithmetic.Coeff (level :: lower)

A lower-tower coefficient embedded as the constant coefficient of one extension level.

Equations

• Hex.NumberTower.LevelSemantics.liftCoeff level lower a = { data := Hex.NumberTower.Arithmetic.flattenBlocks level.degree (Hex.NumberTower.levelsDim lower) #[a.data], size_eq := ⋯ }

theorem Hex.NumberTower.LevelSemantics.coeffDenote_lift (level : Level) (lower : List Level) (hdegree : 0 < level.degree) (a : Arithmetic.Coeff lower) : coeffDenote (level :: lower) (liftCoeff level lower a) = coeffDenote lower a

Constant-block embedding preserves coefficient denotation.

theorem Hex.NumberTower.LevelSemantics.DenoteInjective.tail (level : Level) (lower : List Level) (hdegree : 1 < level.degree) (hinjective : DenoteInjective (level :: lower)) : DenoteInjective lower

Injectivity at an extension level implies injectivity for its lower coefficient tower.

theorem Hex.NumberTower.LevelSemantics.fixed_all_zero_iff (levels : List Level) (hinjective : DenoteInjective levels) (a : Array ℚ) : ((Arithmetic.fixedCoeffs (levelsDim levels) a).all fun (q : ℚ) => decide (q = 0)) = true ↔ denote levels a = 0

The executable fixed-width all-zero test is equivalent to semantic zero when canonical coefficient denotation is injective.

theorem Hex.NumberTower.LevelSemantics.denote_invCoords (levels : List Level) (hvalid : LevelsValid levels) (hinjective : DenoteInjective levels) (a : Array ℚ) : denote levels (Arithmetic.invCoords levels a) = (denote levels a)⁻¹

Recursive extended-gcd coordinates denote complex inversion at every validated tower depth, including the executable 0⁻¹ = 0 convention.

theorem Hex.NumberTower.LevelSemantics.coeffDenote_inv (levels : List Level) (hvalid : LevelsValid levels) (hinjective : DenoteInjective levels) (a : Arithmetic.Coeff levels) : coeffDenote levels a⁻¹ = (coeffDenote levels a)⁻¹

Executable inversion of a canonical coefficient preserves denotation at any validated level list with an injective fixed embedding.

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

Evaluation at any complex zero of the mapped defining relation is a ring homomorphism from the canonical top-level coefficient field.

Equations

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

@[simp]

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

theorem Hex.NumberTower.LevelSemantics.coeffDenote_inv_nil (a : Arithmetic.Coeff []) : coeffDenote [] a⁻¹ = (coeffDenote [] a)⁻¹

Executable inversion at the rational base preserves denotation.

@[reducible]

noncomputable def Hex.NumberTower.LevelSemantics.coeffFieldNil : Field (Arithmetic.Coeff [])

Canonical base-tower coefficients are the rational field.

Equations

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

noncomputable def Hex.NumberTower.LevelSemantics.coeffRatEquiv : Arithmetic.Coeff [] ≃+* ℚ

Canonical base-tower coefficients are ring-equivalent to the rationals.

Equations

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

@[simp]

theorem Hex.NumberTower.LevelSemantics.coeffRatEquiv_ofData (data : Array ℚ) : coeffRatEquiv (Arithmetic.Coeff.ofData [] data) = data.getD 0 0

Under the rational identification of base-tower coefficients, rebuilding from raw data reads off its first entry.

theorem Hex.NumberTower.LevelSemantics.map_rawPoly_nil (f : Array (Array ℚ)) : Polynomial.map coeffRatEquiv.toRingHom (HexPolyMathlib.toPolynomial (Factor.rawPoly [] f)) = HexPolyMathlib.toPolynomial (Factor.toRatPoly f)

Mapping a raw base-tower polynomial through the canonical rational equivalence recovers the rational polynomial stored by its coordinates.

theorem Hex.NumberTower.LevelSemantics.isIrreducible_nil_toMathlib (f : Array (Array ℚ)) (hcheck : Factor.isIrreducible [] f = true) : Irreducible (HexPolyMathlib.toPolynomial (Factor.rawPoly [] f))

The rational-base arm of the recursive checker proves ordinary irreducibility after transporting canonical base coefficients to Rat.

theorem Hex.NumberTower.LevelSemantics.map_relation_nil (level : Level) (hstruct : level.Structural 1) : Polynomial.map coeffRatEquiv.toRingHom (HexPolyMathlib.toPolynomial (Arithmetic.Coeff.relation level [])) = HexPolyMathlib.toPolynomial (Factor.toRatPoly (level.polynomial []))

Mapping the executable base relation through the canonical rational equivalence recovers its raw rational polynomial.

theorem Hex.NumberTower.LevelSemantics.relation_irreducible_rational (level : Level) (hstruct : level.Structural 1) (hrelation : level.RationalRelation []) : Irreducible (HexPolyMathlib.toPolynomial (Arithmetic.Coeff.relation level []))

A rational-presentation certificate makes the executable base relation irreducible over the canonical base coefficient field.

theorem Hex.NumberTower.LevelSemantics.DenoteInjective.singleton (level : Level) (hvalid : LevelsValid [level]) : DenoteInjective [level]

Every validated one-level presentation has injective canonical complex denotation. Rational-presentation certificates use their stored primitive associate; relative certificates over the rational base use the recursive factor checker base case.

theorem Hex.NumberTower.toComplex_injective_of_denote (T : NumberTower) (hinjective : LevelSemantics.DenoteInjective T.levels.toList) : Function.Injective T.toComplex

Injectivity of canonical raw coefficient denotation induces injectivity of the public fixed-width tower interpretation.