theorem Hex.NumberTower.toComplex_injective (T : NumberTower) : Function.Injective T.toComplex

The fixed complex interpretation is injective.

theorem Hex.NumberTower.coeffDenote_injective (T : NumberTower) : LevelSemantics.DenoteInjective T.levels.toList

The canonical coefficient denotation of a certified tower is injective.

theorem Hex.NumberTower.map_zero (T : NumberTower) : T.toComplex 0 = 0

Executable zero denotes complex zero.

theorem Hex.NumberTower.map_one (T : NumberTower) : T.toComplex 1 = 1

Executable one denotes complex one.

theorem Hex.NumberTower.map_add (T : NumberTower) (a b : T.Elem) : T.toComplex (a + b) = T.toComplex a + T.toComplex b

Coordinate addition computes complex addition.

theorem Hex.NumberTower.map_neg (T : NumberTower) (a : T.Elem) : T.toComplex (-a) = -T.toComplex a

Coordinate negation computes complex negation.

theorem Hex.NumberTower.map_sub (T : NumberTower) (a b : T.Elem) : T.toComplex (a - b) = T.toComplex a - T.toComplex b

Coordinate subtraction computes complex subtraction.

theorem Hex.NumberTower.map_mul (T : NumberTower) (a b : T.Elem) : T.toComplex (a * b) = T.toComplex a * T.toComplex b

Recursive reduced multiplication computes complex multiplication.

theorem Hex.NumberTower.map_inv (T : NumberTower) (a : T.Elem) : T.toComplex a⁻¹ = (T.toComplex a)⁻¹

Recursive extended-gcd inversion computes complex inversion, including the executable convention 0⁻¹ = 0.

theorem Hex.NumberTower.map_div (T : NumberTower) (a b : T.Elem) : T.toComplex (a / b) = T.toComplex a / T.toComplex b

Tower division computes complex division.

theorem Hex.NumberTower.map_smul (T : NumberTower) (q : ℚ) (a : T.Elem) : T.toComplex (q • a) = ↑q * T.toComplex a

The executable rational scalar action is semantic scalar multiplication.

theorem Hex.NumberTower.map_natPow (T : NumberTower) (a : T.Elem) (n : ℕ) : T.toComplex (natPow a n) = T.toComplex a ^ n

Natural powers preserve the selected complex interpretation.

theorem Hex.NumberTower.map_intPow (T : NumberTower) (a : T.Elem) (n : ℤ) : T.toComplex (intPow a n) = T.toComplex a ^ n

Integer powers preserve the selected complex interpretation.

@[reducible]

noncomputable def Hex.NumberTower.elemField (T : NumberTower) : Field T.Elem

The law-bearing field whose operations are the existing executable tower coordinate operations. The remaining casts and scalar actions use the canonical rational embedding.

Equations

• T.elemField = Function.Injective.field T.toComplex ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable def Hex.NumberTower.TowerField.instFieldElem_hexNumberFieldTowerMathlib (T : NumberTower) : Field T.Elem

Opt-in field instance for tower elements. It is scoped so importing the Mathlib correspondence layer does not make executable downstream definitions depend on a noncomputable semantic proof dictionary.

Equations

• Hex.NumberTower.TowerField.instFieldElem_hexNumberFieldTowerMathlib T = T.elemField

noncomputable def Hex.NumberTower.embedding (T : NumberTower) : T.Elem →+* ℂ

The selected complex interpretation as an injective ring homomorphism.

Equations

• T.embedding = { toFun := T.toComplex, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Hex.NumberTower.embedding_apply (T : NumberTower) (a : T.Elem) : T.embedding a = T.toComplex a

theorem Hex.NumberTower.embedding_injective (T : NumberTower) : Function.Injective ⇑T.embedding

The selected complex ring homomorphism is an embedding.

theorem Hex.NumberTower.isZero_iff (T : NumberTower) (a : T.Elem) : isZero a = true ↔ T.toComplex a = 0

The Boolean zero test recognizes exactly semantic zero.

theorem Hex.NumberTower.eq_iff_toComplex (T : NumberTower) (a b : T.Elem) : a = b ↔ T.toComplex a = T.toComplex b

Mixed-radix coordinate equality is exactly semantic equality.

theorem Hex.NumberTower.TowerField.instCharZeroElem_hexNumberFieldTowerMathlib (T : NumberTower) : CharZero T.Elem

Tower coordinate fields have characteristic zero, through the injective complex embedding.

@[instance_reducible]

noncomputable def Hex.NumberTower.TowerField.instFieldElem_hexNumberFieldTowerMathlib_1 (T : NumberTower) : Lean.Grind.Field T.Elem

Opt-in Lean.Grind.Field law package for the executable tower operations, derived from the scoped field instance through the standard Mathlib bridge. It is scoped together with the field instance so executable downstream code does not silently depend on the semantic dictionary.

Equations

• Hex.NumberTower.TowerField.instFieldElem_hexNumberFieldTowerMathlib_1 T = Field.toGrindField

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

The field's rational cast is the executable rational embedding.

theorem Hex.NumberTower.ratCast_mul_eq_smul (T : NumberTower) (q : ℚ) (a : T.Elem) : ↑q * a = q • a

Multiplication by an embedded rational is the executable scalar action.

noncomputable def Hex.NumberTower.coordEquiv (T : NumberTower) : T.Elem ≃ₗ[ℚ] Fin T.dim → ℚ

The mixed-radix coordinate representation as a ℚ-linear equivalence with the fixed-width function space.

Equations

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

@[reducible, inline]

abbrev Hex.NumberTower.toField (T : NumberTower) : Type

The element type of a validated tower, regarded as the certified coordinate field. The field, characteristic-zero, and ℚ-algebra structures are the scoped instances of the TowerField namespace.

Equations

• T.toField = T.Elem

theorem Hex.NumberTower.dim_eq_finrank (T : NumberTower) : T.dim = Module.finrank ℚ T.toField

The executable mixed-radix dimension is the ℚ-vector-space dimension of the coordinate field.

def Hex.NumberTower.Extension.PreservesEmbedding {T : NumberTower} (E : T.Extension) : Prop

An extension embedding preserves the fixed absolute embedding. This is a property of checked constructors, not of arbitrary Hex.NumberTower.Extension records.

Equations

• E.PreservesEmbedding = ∀ (a : T.Elem), E.tower.toComplex (E.embed a) = T.toComplex a

def Hex.NumberTower.Extension.GeneratorValue {T : NumberTower} (E : T.Extension) : Prop

The distinguished generator denotes the extension's stored absolute root.

Equations

• E.GeneratorValue = (E.tower.toComplex E.gen = E.root.toComplex)

theorem Hex.NumberTower.Extension.embed_injective {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) : Function.Injective E.embed

A checked extension embedding is injective.

theorem Hex.NumberTower.Extension.embed_add {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) (a b : T.Elem) : E.embed (a + b) = E.embed a + E.embed b

A checked extension embedding is additive.

theorem Hex.NumberTower.Extension.embed_mul {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) (a b : T.Elem) : E.embed (a * b) = E.embed a * E.embed b

A checked extension embedding is multiplicative.

theorem Hex.NumberTower.Extension.embed_ofRat {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) (q : ℚ) : E.embed (T.ofRat q) = E.tower.ofRat q

A checked extension embedding fixes the embedded rationals.

theorem Hex.NumberTower.Extension.embed_smul {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) (q : ℚ) (a : T.Elem) : E.embed (q • a) = q • E.embed a

A checked extension embedding preserves the executable rational scalar action.

noncomputable def Hex.NumberTower.Extension.embedAlgHom {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) : T.toField →ₐ[ℚ] E.tower.toField

A checked extension embedding as a ℚ-algebra homomorphism between the certified coordinate fields. Injectivity is embedAlgHom_injective.

Equations

• E.embedAlgHom hE = { toFun := E.embed, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Hex.NumberTower.Extension.embedAlgHom_apply {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) (a : T.Elem) : (E.embedAlgHom hE) a = E.embed a

The algebra homomorphism packaging acts by the executable embedding.

theorem Hex.NumberTower.Extension.embedAlgHom_injective {T : NumberTower} (E : T.Extension) (hE : E.PreservesEmbedding) : Function.Injective ⇑(E.embedAlgHom hE)

The ℚ-algebra homomorphism packaging of a checked extension embedding is injective.