theorem Hex.NumberTower.LevelSemantics.block_map_mul (q : ℚ) (data : Array ℚ) (index width : ℕ) : Arithmetic.block (Array.map (fun (c : ℚ) => q * c) data) index width = Array.map (fun (c : ℚ) => q * c) (Arithmetic.block data index width)

Extracting a coordinate block commutes with coordinatewise rational scaling.

theorem Hex.NumberTower.LevelSemantics.denote_smul (levels : List Level) (q : ℚ) (data : Array ℚ) : denote levels (Array.map (fun (c : ℚ) => q * c) data) = ↑q * denote levels data

Coordinatewise rational scaling commutes with direct tower denotation.

noncomputable def Hex.NumberTower.LevelSemantics.evalBlocks (lower : List Level) (x : ℂ) (blocks : Array (Array ℚ)) : ℂ

Evaluate an array of lower-tower coefficient blocks as a power sum.

Equations

• Hex.NumberTower.LevelSemantics.evalBlocks lower x blocks = ∑ i ∈ Finset.range blocks.size, Hex.NumberTower.LevelSemantics.denote lower (blocks.getD i #[]) * x ^ i

noncomputable def Hex.NumberTower.LevelSemantics.evalUpTo (lower : List Level) (x : ℂ) (count : ℕ) (blocks : Array (Array ℚ)) : ℂ

Evaluate a prescribed initial range of lower-tower coefficient blocks.

Equations

• Hex.NumberTower.LevelSemantics.evalUpTo lower x count blocks = ∑ i ∈ Finset.range count, Hex.NumberTower.LevelSemantics.denote lower (blocks.getD i #[]) * x ^ i

theorem Hex.NumberTower.LevelSemantics.getD_set! (blocks : Array (Array ℚ)) (k i : ℕ) (value default : Array ℚ) (hk : k < blocks.size) : (blocks.set! k value).getD i default = if k = i then value else blocks.getD i default

Defaulted read after an in-bounds set!: position k holds the new value and every other position is unchanged.

theorem Hex.NumberTower.LevelSemantics.evalUpTo_set (lower : List Level) (x : ℂ) (count : ℕ) (blocks : Array (Array ℚ)) (k : ℕ) (value : Array ℚ) (hcount : k < count) (hsize : k < blocks.size) : evalUpTo lower x count (blocks.set! k value) = evalUpTo lower x count blocks + (denote lower value - denote lower (blocks.getD k #[])) * x ^ k

Updating one block inside the evaluated range changes its value by the corresponding monomial delta.

theorem Hex.NumberTower.LevelSemantics.evalUpTo_take (lower : List Level) (x : ℂ) (count cutoff : ℕ) (blocks : Array (Array ℚ)) (hcount : count ≤ cutoff) : evalUpTo lower x count (blocks.take cutoff) = evalUpTo lower x count blocks

Truncation above the evaluated range does not alter its power sum.

theorem Hex.NumberTower.LevelSemantics.fold_eval {ι : Type} (lower : List Level) (x : ℂ) (count size : ℕ) (indices : List ι) (step : Array (Array ℚ) → ι → Array (Array ℚ)) (term : ι → ℂ) (initial : Array (Array ℚ)) (hinitial : initial.size = size) (hstep : ∀ (work : Array (Array ℚ)), ∀ index ∈ indices, work.size = size → (step work index).size = size ∧ evalUpTo lower x count (step work index) = evalUpTo lower x count work + term index) : evalUpTo lower x count (List.foldl step initial indices) = evalUpTo lower x count initial + (List.map term indices).sum ∧ (List.foldl step initial indices).size = size

Generic accumulation principle for coordinate folds: if every step preserves the working size and adds one term to the evaluated power sum, the fold adds the sum of all terms.

theorem Hex.NumberTower.LevelSemantics.list_sum_range (count : ℕ) (term : ℕ → ℂ) : (List.map term (List.range count)).sum = ∑ i ∈ Finset.range count, term i

A sum over List.range agrees with the corresponding Finset.range sum.

theorem Hex.NumberTower.LevelSemantics.convolveRow_eval (lower : List Level) (x : ℂ) (degree i : ℕ) (a b : Array ℚ) (multiply : Array ℚ → Array ℚ → Array ℚ) (work : Array (Array ℚ)) (hdegree : 0 < degree) (hi : i < degree) (hsize : work.size = 2 * degree - 1) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower x (2 * degree - 1) (Arithmetic.convolveRow degree (levelsDim lower) i multiply a b work) = evalUpTo lower x (2 * degree - 1) work + (List.map (fun (j : ℕ) => denote lower (Arithmetic.block a i (levelsDim lower)) * denote lower (Arithmetic.block b j (levelsDim lower)) * x ^ (i + j)) (List.range degree)).sum

One convolution row adds exactly the monomial contributions of block i of a against every block of b.

theorem Hex.NumberTower.LevelSemantics.denote_flatten (level : Level) (lower : List Level) (blocks : Array (Array ℚ)) : denote (level :: lower) (Arithmetic.flattenBlocks level.degree (levelsDim lower) blocks) = ∑ i ∈ Finset.range level.degree, denote lower (blocks.getD i #[]) * level.root.toComplex ^ i

Flattening a top-level block array preserves its finite power sum through the requested extension degree.

noncomputable def Hex.NumberTower.LevelSemantics.evalAt (level : Level) (lower : List Level) (x : ℂ) (data : Array ℚ) : ℂ

Evaluate top-level mixed-radix coordinates at an arbitrary conjugate of the newest generator while retaining the fixed lower embedding.

Equations

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

theorem Hex.NumberTower.LevelSemantics.evalAt_flatten (level : Level) (lower : List Level) (x : ℂ) (blocks : Array (Array ℚ)) : evalAt level lower x (Arithmetic.flattenBlocks level.degree (levelsDim lower) blocks) = evalUpTo lower x level.degree blocks

Flattening explicit top-level blocks preserves arbitrary-conjugate evaluation.

theorem Hex.NumberTower.LevelSemantics.evalAt_fixed (level : Level) (lower : List Level) (x : ℂ) (data : Array ℚ) : evalAt level lower x (Arithmetic.fixedCoeffs (level.degree * levelsDim lower) data) = evalAt level lower x data

Fixed-width normalization does not change arbitrary-conjugate evaluation.

theorem Hex.NumberTower.LevelSemantics.evalAt_root (level : Level) (lower : List Level) (data : Array ℚ) : evalAt level lower level.root.toComplex data = denote (level :: lower) data

The selected stored root specializes arbitrary-conjugate evaluation back to canonical tower denotation.

theorem Hex.NumberTower.LevelSemantics.polynomial_eval (lower : List Level) (blocks : Array (Array ℚ)) (x : ℂ) : Polynomial.eval x (polynomial lower blocks) = evalBlocks lower x blocks

The polynomial view of raw blocks evaluates to their finite power sum.

theorem Hex.NumberTower.LevelSemantics.denote_empty (levels : List Level) : denote levels #[] = 0

The empty coordinate array denotes zero at every tower height.

theorem Hex.NumberTower.LevelSemantics.denote_zero (levels : List Level) : denote levels (Arithmetic.fixedCoeffs (levelsDim levels) #[]) = 0

The canonical all-zero block denotes zero at every tower depth.

theorem Hex.NumberTower.LevelSemantics.denote_embed (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (data : Array ℚ) (hsize : data.size = levelsDim lower) : denote (level :: lower) data = denote lower data

A fixed-width lower coordinate vector occupies the constant block of the next extension level.

theorem Hex.NumberTower.LevelSemantics.denote_neg (levels : List Level) (data : Array ℚ) : denote levels (Arithmetic.negCoords (levelsDim levels) data) = -denote levels data

Fixed-width coordinate negation denotes complex negation.

theorem Hex.NumberTower.LevelSemantics.denote_replicate_zero (levels : List Level) : denote levels (Array.replicate (levelsDim levels) 0) = 0

The zero-filled coordinate array of full width denotes zero.

theorem Hex.NumberTower.LevelSemantics.evalUpTo_replicate_zero (lower : List Level) (x : ℂ) (count : ℕ) : evalUpTo lower x count (Array.replicate count (Array.replicate (levelsDim lower) 0)) = 0

A power sum over zero-filled blocks vanishes.

theorem Hex.NumberTower.LevelSemantics.convolve_eval (lower : List Level) (x : ℂ) (degree : ℕ) (a b : Array ℚ) (multiply : Array ℚ → Array ℚ → Array ℚ) (hdegree : 0 < degree) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower x (2 * degree - 1) (Arithmetic.convolve degree (levelsDim lower) multiply a b) = ∑ i ∈ Finset.range degree, ∑ j ∈ Finset.range degree, denote lower (Arithmetic.block a i (levelsDim lower)) * denote lower (Arithmetic.block b j (levelsDim lower)) * x ^ (i + j)

The executable convolution evaluates to the double sum of blockwise products weighted by x ^ (i + j).

theorem Hex.NumberTower.LevelSemantics.convolve_mul (lower : List Level) (x : ℂ) (degree : ℕ) (a b : Array ℚ) (multiply : Array ℚ → Array ℚ → Array ℚ) (hdegree : 0 < degree) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower x (2 * degree - 1) (Arithmetic.convolve degree (levelsDim lower) multiply a b) = (∑ i ∈ Finset.range degree, denote lower (Arithmetic.block a i (levelsDim lower)) * x ^ i) * ∑ j ∈ Finset.range degree, denote lower (Arithmetic.block b j (levelsDim lower)) * x ^ j

The executable convolution evaluates to the product of the two operand power sums: schoolbook multiplication is correct under denotation.

theorem Hex.NumberTower.LevelSemantics.reduceCoeffs_eval (lower : List Level) (x : ℂ) (degree k : ℕ) (defining : Array (Array ℚ)) (multiply : Array ℚ → Array ℚ → Array ℚ) (work : Array (Array ℚ)) (hdk : degree ≤ k) (hsize : work.size = k + 1) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : have zeroBlock := Array.replicate (levelsDim lower) 0; have high := work.getD k zeroBlock; evalUpTo lower x k (Arithmetic.reduceCoeffs degree (levelsDim lower) k defining multiply work) = evalUpTo lower x k work + ∑ j ∈ Finset.range degree, -(denote lower high * denote lower (defining.getD j zeroBlock) * x ^ (k - degree + j))

One coefficient-reduction step subtracts the top block times each defining coefficient at the correspondingly shifted position.

theorem Hex.NumberTower.LevelSemantics.denote_one (levels : List Level) (hvalid : LevelsValid levels) : denote levels (Arithmetic.fixedCoeffs (levelsDim levels) #[1]) = 1

The canonical constant-one block denotes one for every valid lower tower.

theorem Hex.NumberTower.LevelSemantics.denote_rat (levels : List Level) (hvalid : LevelsValid levels) (q : ℚ) : denote levels #[q] = ↑q

A one-coordinate rational constant has its usual complex value at every validated tower depth.

@[simp]

theorem Hex.NumberTower.LevelSemantics.evalAt_zero (level : Level) (lower : List Level) (_hvalid : LevelsValid (level :: lower)) (x : ℂ) : evalAt level lower x (Arithmetic.Coeff.data 0) = 0

Conjugate evaluation sends the zero coefficient to 0.

@[simp]

theorem Hex.NumberTower.LevelSemantics.evalAt_one (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (x : ℂ) : evalAt level lower x (Arithmetic.Coeff.data 1) = 1

Conjugate evaluation sends the one coefficient to 1.

theorem Hex.NumberTower.LevelSemantics.evalAt_add (level : Level) (lower : List Level) (_hvalid : LevelsValid (level :: lower)) (x : ℂ) (a b : Arithmetic.Coeff (level :: lower)) : evalAt level lower x (a + b).data = evalAt level lower x a.data + evalAt level lower x b.data

Conjugate evaluation is additive.

theorem Hex.NumberTower.LevelSemantics.denote_generator (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hdegree : 1 < level.degree) : denote (level :: lower) ((Array.replicate (levelsDim lower) 0).push 1) = level.root.toComplex

The mixed-radix basis coordinate immediately after the lower block denotes the newly adjoined generator.

theorem Hex.NumberTower.LevelSemantics.evalAt_generator (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (hdegree : 1 < level.degree) (x : ℂ) : evalAt level lower x ((Array.replicate (levelsDim lower) 0).push 1) = x

The mixed-radix basis coordinate immediately after the lower block evaluates to the chosen conjugate of the newest generator.

theorem Hex.NumberTower.LevelSemantics.relation_sum (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) : ∑ j ∈ Finset.range level.degree, denote lower (level.defining.getD j #[]) * level.root.toComplex ^ j + level.root.toComplex ^ level.degree = 0

The stored monic relation is the vanishing power sum used by descending coordinate reduction.

theorem Hex.NumberTower.LevelSemantics.reduceAt_eval_of_relation (level : Level) (lower : List Level) (x : ℂ) (hrelationInput : ∑ j ∈ Finset.range level.degree, denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) (k : ℕ) (multiply : Array ℚ → Array ℚ → Array ℚ) (work : Array (Array ℚ)) (hvalid : LevelsValid (level :: lower)) (hdk : level.degree ≤ k) (hsize : work.size = k + 1) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower x k (Arithmetic.reduceAt level.degree (levelsDim lower) k level.defining multiply work) = evalUpTo lower x (k + 1) work

One descending reduction step preserves evaluation at any zero of the mapped monic level relation.

theorem Hex.NumberTower.LevelSemantics.reduce_eval_of_relation (level : Level) (lower : List Level) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) (fuel : ℕ) (multiply : Array ℚ → Array ℚ → Array ℚ) (work : Array (Array ℚ)) (hvalid : LevelsValid (level :: lower)) (hsize : work.size = level.degree + fuel) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower x level.degree (Arithmetic.reduce level.degree (levelsDim lower) level.defining multiply fuel work) = evalUpTo lower x (level.degree + fuel) work

Full descending reduction preserves evaluation at any zero of the mapped monic relation.

theorem Hex.NumberTower.LevelSemantics.reduceAt_eval (level : Level) (lower : List Level) (k : ℕ) (multiply : Array ℚ → Array ℚ → Array ℚ) (work : Array (Array ℚ)) (hvalid : LevelsValid (level :: lower)) (hdk : level.degree ≤ k) (hsize : work.size = k + 1) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower level.root.toComplex k (Arithmetic.reduceAt level.degree (levelsDim lower) k level.defining multiply work) = evalUpTo lower level.root.toComplex (k + 1) work

Full degree reduction at the stored root preserves the evaluated power sum: each subtracted multiple of the monic defining relation vanishes at the root, so the reduced width-k array evaluates like the original width-k+1 array.

theorem Hex.NumberTower.LevelSemantics.reduce_eval (level : Level) (lower : List Level) (fuel : ℕ) (multiply : Array ℚ → Array ℚ → Array ℚ) (work : Array (Array ℚ)) (hvalid : LevelsValid (level :: lower)) (hsize : work.size = level.degree + fuel) (hmul : ∀ (u v : Array ℚ), denote lower (multiply u v) = denote lower u * denote lower v) : evalUpTo lower level.root.toComplex level.degree (Arithmetic.reduce level.degree (levelsDim lower) level.defining multiply fuel work) = evalUpTo lower level.root.toComplex (level.degree + fuel) work

Descending reduction preserves evaluation at the current algebraic root.

theorem Hex.NumberTower.LevelSemantics.denote_mul (levels : List Level) (hvalid : LevelsValid levels) (a b : Array ℚ) : denote levels (Arithmetic.mulCoords levels a b) = denote levels a * denote levels b

Recursive convolution and monic reduction denote complex multiplication.

theorem Hex.NumberTower.LevelSemantics.evalAt_mul (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) (x : ℂ) (hrelation : ∑ j ∈ Finset.range level.degree, denote lower (level.defining.getD j #[]) * x ^ j + x ^ level.degree = 0) (a b : Array ℚ) : evalAt level lower x (Arithmetic.mulCoords (level :: lower) a b) = evalAt level lower x a * evalAt level lower x b

Recursive reduced multiplication is respected by evaluation at every complex zero of the mapped top-level relation.

noncomputable def Hex.NumberTower.LevelSemantics.coeffDenote (levels : List Level) (a : Arithmetic.Coeff levels) : ℂ

Complex denotation restricted to the canonical fixed-width coefficient carrier used by recursive inversion.

Equations

• Hex.NumberTower.LevelSemantics.coeffDenote levels a = Hex.NumberTower.LevelSemantics.denote levels a.data

@[simp]

theorem Hex.NumberTower.LevelSemantics.coeffDenote_zero (levels : List Level) : coeffDenote levels 0 = 0

Coefficient denotation sends the zero coefficient to 0.

@[simp]

theorem Hex.NumberTower.LevelSemantics.coeffDenote_one (levels : List Level) (hvalid : LevelsValid levels) : coeffDenote levels 1 = 1

Coefficient denotation sends the one coefficient to 1.

theorem Hex.NumberTower.LevelSemantics.coeffDenote_add (levels : List Level) (a b : Arithmetic.Coeff levels) : coeffDenote levels (a + b) = coeffDenote levels a + coeffDenote levels b

Coefficient denotation is additive over the executable addition.

theorem Hex.NumberTower.LevelSemantics.coeffDenote_sub (levels : List Level) (a b : Arithmetic.Coeff levels) : coeffDenote levels (a - b) = coeffDenote levels a - coeffDenote levels b

Coefficient denotation respects the executable subtraction.

theorem Hex.NumberTower.LevelSemantics.coeffDenote_neg (levels : List Level) (a : Arithmetic.Coeff levels) : coeffDenote levels (-a) = -coeffDenote levels a

Coefficient denotation respects the executable negation.

theorem Hex.NumberTower.LevelSemantics.coeffDenote_mul (levels : List Level) (hvalid : LevelsValid levels) (a b : Arithmetic.Coeff levels) : coeffDenote levels (a * b) = coeffDenote levels a * coeffDenote levels b

Coefficient denotation is multiplicative over the executable mixed-radix multiplication.

def Hex.NumberTower.LevelSemantics.coeffSmul (levels : List Level) (q : ℚ) (a : Arithmetic.Coeff levels) : Arithmetic.Coeff levels

Rational coordinate scaling on canonical coefficients.

Equations

• Hex.NumberTower.LevelSemantics.coeffSmul levels q a = Hex.NumberTower.Arithmetic.Coeff.ofData levels (Array.map (fun (c : ℚ) => q * c) a.data)

theorem Hex.NumberTower.LevelSemantics.coeffDenote_smul (levels : List Level) (q : ℚ) (a : Arithmetic.Coeff levels) : coeffDenote levels (coeffSmul levels q a) = ↑q * coeffDenote levels a

Coefficient denotation turns the executable rational scaling into multiplication by the embedded rational.

def Hex.NumberTower.LevelSemantics.coeffPow {levels : List Level} (a : Arithmetic.Coeff levels) : ℕ → Arithmetic.Coeff levels

Natural powers using the executable coefficient multiplication.

Equations

• Hex.NumberTower.LevelSemantics.coeffPow a 0 = 1
• Hex.NumberTower.LevelSemantics.coeffPow a n.succ = Hex.NumberTower.LevelSemantics.coeffPow a n * a

theorem Hex.NumberTower.LevelSemantics.coeffDenote_pow (levels : List Level) (hvalid : LevelsValid levels) (a : Arithmetic.Coeff levels) (n : ℕ) : coeffDenote levels (coeffPow a n) = coeffDenote levels a ^ n

Coefficient denotation turns the executable natural power into the complex power.

def Hex.NumberTower.LevelSemantics.coeffZPow {levels : List Level} (a : Arithmetic.Coeff levels) : ℤ → Arithmetic.Coeff levels

Integer powers using the executable coefficient inverse for negative exponents.

Equations

• Hex.NumberTower.LevelSemantics.coeffZPow a (Int.ofNat n) = Hex.NumberTower.LevelSemantics.coeffPow a n
• Hex.NumberTower.LevelSemantics.coeffZPow a (Int.negSucc n) = (Hex.NumberTower.LevelSemantics.coeffPow a (n + 1))⁻¹

def Hex.NumberTower.LevelSemantics.DenoteInjective (levels : List Level) : Prop

Canonical coefficients at one level list have unique complex denotation.

Equations

• Hex.NumberTower.LevelSemantics.DenoteInjective levels = Function.Injective (Hex.NumberTower.LevelSemantics.coeffDenote levels)

@[reducible]

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

Transfer a lawful field structure to canonical executable coefficients once recursive inversion is known to preserve complex denotation. Auxiliary casts, scalar actions, and powers are chosen through rational coordinate scaling and the existing executable operations.

Equations

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

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

Canonical coefficient denotation bundled as a ring homomorphism for the transferred executable field.

Equations

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

theorem Hex.NumberTower.LevelSemantics.fixedCoeffs_eq_self (levels : List Level) (a : Arithmetic.Coeff levels) : Arithmetic.fixedCoeffs (levelsDim levels) a.data = a.data

Canonical coefficient data is already the right width, so zero-padding fixes it.

theorem Hex.NumberTower.LevelSemantics.coeff_eq_of_data_eq {levels : List Level} {a b : Arithmetic.Coeff levels} (h : a.data = b.data) : a = b

Canonical coefficients with equal coordinate data are equal.

@[simp]

theorem Hex.NumberTower.LevelSemantics.coeff_ofData_data (levels : List Level) (a : Arithmetic.Coeff levels) : Arithmetic.Coeff.ofData levels a.data = a

Rebuilding a canonical coefficient from its own data is the identity.

noncomputable def Hex.NumberTower.LevelSemantics.denseEval (lower : List Level) (x : ℂ) (degree : ℕ) (f : DensePoly (Arithmetic.Coeff lower)) : ℂ

Evaluate a prescribed coefficient range of an executable dense polynomial through lower-tower denotation.

Equations

• Hex.NumberTower.LevelSemantics.denseEval lower x degree f = ∑ i ∈ Finset.range degree, Hex.NumberTower.LevelSemantics.coeffDenote lower (f.coeff i) * x ^ i

noncomputable def Hex.NumberTower.LevelSemantics.denseMap (lower : List Level) (x : ℂ) (hvalid : LevelsValid lower) (hinjective : DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), coeffDenote lower a⁻¹ = (coeffDenote lower a)⁻¹) : DensePoly (Arithmetic.Coeff lower) → ℂ

Evaluation of executable dense polynomials after transferring the lawful lower-tower field structure.

Equations

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

theorem Hex.NumberTower.LevelSemantics.denseMap_eq_denseEval (lower : List Level) (x : ℂ) (hvalid : LevelsValid lower) (hinjective : DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), coeffDenote lower a⁻¹ = (coeffDenote lower a)⁻¹) (degree : ℕ) (f : DensePoly (Arithmetic.Coeff lower)) (hdegree : f.natDegree < degree) : denseMap lower x hvalid hinjective hinv f = denseEval lower x degree f

Ring-hom evaluation agrees with the prescribed coefficient sum whenever the polynomial has degree below that range.

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

Dense evaluation preserves multiplication.

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

Dense evaluation preserves addition.

theorem Hex.NumberTower.LevelSemantics.denseMap_scale (lower : List Level) (x : ℂ) (hvalid : LevelsValid lower) (hinjective : DenoteInjective lower) (hinv : ∀ (a : Arithmetic.Coeff lower), coeffDenote lower a⁻¹ = (coeffDenote lower a)⁻¹) (c : Arithmetic.Coeff lower) (f : DensePoly (Arithmetic.Coeff lower)) : denseMap lower x hvalid hinjective hinv (DensePoly.scale c f) = coeffDenote lower c * denseMap lower x hvalid hinjective hinv f

Dense evaluation sends coefficient scaling to scalar multiplication.

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

Dense evaluation of a constant is lower-tower denotation.