noncomputable def Hex.NumberTower.eval? (T : NumberTower) (a : T.Elem) : Option ℂ

Checked semantic evaluation of a tower element through all stored fixed embeddings.

Equations

• T.eval? a = Option.map Hex.AlgebraicRoot.toComplex (Hex.NumberTower.RawEvaluation.evalCoords? T.levels.toList (Hex.NumberTower.coeffs a))

theorem Hex.NumberTower.evalCoords_isSome (levels : List Level) (data : Array ℚ) : (RawEvaluation.evalCoords? levels data).isSome = true

Raw coordinate evaluation is total at every tower depth.

theorem Hex.NumberTower.evalPoly_isSome (levels : List Level) (f : Array (Array ℚ)) (candidate : AlgebraicRoot) : (RawEvaluation.evalPoly? levels f candidate).isSome = true

Exact raw tower-polynomial evaluation is total.

theorem Hex.NumberTower.evalBall_isSome (levels : List Level) (f : Array (Array ℚ)) (candidate : AlgebraicRoot) (prec : ℕ) : (RawEvaluation.evalBall? levels f candidate prec).isSome = true

The raw certified-ball evaluator returns a ball at every precision.

theorem Hex.NumberTower.eval?_isSome (T : NumberTower) (a : T.Elem) : (T.eval? a).isSome = true

Every validated tower element can be evaluated in the stored embedding.

theorem Hex.NumberTower.eval?_eq (T : NumberTower) (a : T.Elem) {root : AlgebraicRoot} (h : RawEvaluation.evalCoords? T.levels.toList (coeffs a) = some root) : T.eval? a = some root.toComplex

A successful recursive evaluation has the value of the returned lazy algebraic root.

noncomputable def Hex.NumberTower.toComplex (T : NumberTower) (a : T.Elem) : ℂ

The complex value of a tower element. The fallback is unreachable by Hex.NumberTower.eval?_isSome.

Equations

• T.toComplex a = (T.eval? a).getD 0

theorem Hex.NumberTower.toComplex_eq (T : NumberTower) (a : T.Elem) {root : AlgebraicRoot} (h : RawEvaluation.evalCoords? T.levels.toList (coeffs a) = some root) : T.toComplex a = root.toComplex

A successful executable evaluation computes toComplex.

theorem Hex.NumberTower.levelsDim_pos (levels : List Level) (hvalid : LevelsValid levels) : 0 < levelsDim levels

Every structurally valid level list has positive mixed-radix dimension.

theorem Hex.NumberTower.dim_pos (T : NumberTower) : 0 < T.dim

Every validated tower has positive dimension.

noncomputable def Hex.NumberTower.LevelSemantics.denote (levels : List Level) : Array ℚ → ℂ

Direct complex Horner interpretation of raw mixed-radix coordinates.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.LevelSemantics.denote [] x✝ = ↑(x✝.getD 0 0)

noncomputable def Hex.NumberTower.LevelSemantics.polynomial (lower : List Level) (f : Array (Array ℚ)) : Polynomial ℂ

Interpret a raw polynomial over a lower tower in Polynomial ℂ.

Equations

• Hex.NumberTower.LevelSemantics.polynomial lower f = ∑ i ∈ Finset.range f.size, (Polynomial.monomial i) (Hex.NumberTower.LevelSemantics.denote lower (f.getD i #[]))

theorem Hex.NumberTower.LevelSemantics.polynomial_eval_horner (levels : List Level) (f : Array (Array ℚ)) (x : ℂ) : Polynomial.eval x (polynomial levels f) = List.foldr (fun (coefficient : Array ℚ) (value : ℂ) => value * x + denote levels coefficient) 0 f.toList

The raw polynomial interpretation evaluates by ordinary Horner folding.

theorem Hex.NumberTower.LevelSemantics.denote_cons (level : Level) (lower : List Level) (data : Array ℚ) : denote (level :: lower) data = ∑ i ∈ Finset.range level.degree, denote lower (Arithmetic.block data i (levelsDim lower)) * level.root.toComplex ^ i

Recursive Horner denotation is the finite power sum of its top-level coefficient blocks.

theorem Hex.NumberTower.LevelSemantics.denote_add (levels : List Level) (a b : Array ℚ) : denote levels (Arithmetic.addCoords (levelsDim levels) a b) = denote levels a + denote levels b

Direct tower denotation is additive on fixed-width coordinates.

theorem Hex.NumberTower.LevelSemantics.denote_fixed (levels : List Level) (data : Array ℚ) : denote levels (Arithmetic.fixedCoeffs (levelsDim levels) data) = denote levels data

Direct tower denotation only observes the canonical mixed-radix width.

theorem Hex.NumberTower.LevelSemantics.denote_sub (levels : List Level) (a b : Array ℚ) : denote levels (Arithmetic.subCoords (levelsDim levels) a b) = denote levels a - denote levels b

Direct tower denotation is subtractive on fixed-width coordinates.

theorem Hex.NumberTower.LevelSemantics.evalCoords_sound (levels : List Level) (data : Array ℚ) {root : AlgebraicRoot} (h : RawEvaluation.evalCoords? levels data = some root) : root.toComplex = denote levels data

Successful raw evaluation agrees with direct complex Horner denotation.

theorem Hex.NumberTower.LevelSemantics.evalPoly_sound (levels : List Level) (f : Array (Array ℚ)) (candidate result : AlgebraicRoot) (h : RawEvaluation.evalPoly? levels f candidate = some result) : result.toComplex = Polynomial.eval candidate.toComplex (polynomial levels f)

Successful exact evaluation of a raw tower polynomial agrees with its direct complex polynomial interpretation.

theorem Hex.NumberTower.LevelSemantics.toComplex_eq_denote (T : NumberTower) (a : T.Elem) : T.toComplex a = denote T.levels.toList (coeffs a)

The selected complex interpretation is the direct Horner denotation of the element's mixed-radix coordinates.

theorem Hex.NumberTower.LevelSemantics.toComplex_ofRat (T : NumberTower) (q : ℚ) : T.toComplex (T.ofRat q) = ↑q

The rational tower embedding has its expected complex value.

theorem Hex.NumberTower.toComplex_ofRat (T : NumberTower) (q : ℚ) : T.toComplex (T.ofRat q) = ↑q

The rational embedding has its expected value in every validated tower.

theorem Hex.NumberTower.LevelSemantics.norm_denote_le_coordsMajorant (levels : List Level) (data : Array ℚ) : ‖denote levels data‖ ≤ ↑(RawEvaluation.coordsMajorant levels data)

The recursive integer coordinate majorant bounds the selected complex value of any raw tower coordinate array.

theorem Hex.NumberTower.rawEvalBall_sound (levels : List Level) (f : Array (Array ℚ)) (candidate : AlgebraicRoot) (prec : ℕ) {ball : DyadicComplexBall} (hrun : RawEvaluation.evalBall? levels f candidate prec = some ball) : Polynomial.eval candidate.toComplex (LevelSemantics.polynomial levels f) ∈ ball.set

Certified ball evaluation encloses the exact raw tower-polynomial value.

theorem Hex.NumberTower.rawEvalBall_radius (levels : List Level) (f : Array (Array ℚ)) (candidate : AlgebraicRoot) (hcanonical : Factor.polyCoords (Factor.rawPoly levels f) = f) (prec : ℕ) {ball : DyadicComplexBall} (hrun : RawEvaluation.evalBall? levels f candidate prec = some ball) : ball.realRadius ≤ ↑(Disambiguation.evalMajorant (Factor.rawPoly levels f) (fun (coefficient : Arithmetic.Coeff levels) => RawEvaluation.coordsMajorant levels coefficient.data) candidate.p) * 2 ^ (-↑prec)

On canonical raw coordinates, the tower ball evaluator satisfies the error recurrence used by the bounded zero test.

theorem Hex.NumberTower.rawVanishesAt_sound (levels : List Level) (f : Array (Array ℚ)) (candidate : AlgebraicRoot) {keep : Bool} (hrun : RawEvaluation.vanishesAt? levels f candidate = some keep) : keep = true ↔ Polynomial.eval candidate.toComplex (LevelSemantics.polynomial levels f) = 0

The checked raw zero test returns exactly semantic vanishing.

theorem Hex.NumberTower.rawVanishesAt_isSome (levels : List Level) (f : Array (Array ℚ)) (candidate : AlgebraicRoot) (hcanonical : Factor.polyCoords (Factor.rawPoly levels f) = f) : (RawEvaluation.vanishesAt? levels f candidate).isSome = true

The bounded raw zero test is total on canonical tower-polynomial coordinates.

theorem Hex.NumberTower.level_relation_vanishes (level : Level) (lower : List Level) (hvalid : LevelsValid (level :: lower)) : Polynomial.eval level.root.toComplex (LevelSemantics.polynomial lower (level.polynomial lower)) = 0

A validated relative relation vanishes at its selected absolute generator. This is the semantic half of the central level invariant; relative irreducibility is recorded separately by the checked factorization bridge.