30.6. The Mathlib correspondence🔗

HexNumberFieldTowerMathlib interprets every element of a validated tower in ℂ through the stored embedding. That interpretation is injective and respects the executable arithmetic, and each of the four operations has a soundness theorem describing its result and a completeness theorem stating that it never returns none on a valid tower.

open Hex Hex.NumberTower HexNumberFieldTowerChapter

example (a b : Elem T23) :
    T23.toComplex (a * b) =
      T23.toComplex a * T23.toComplex b :=
  map_mul T23 a b

example (a b : Elem T23)
    (h : T23.toComplex a = T23.toComplex b) : a = b :=
  toComplex_injective T23 h

theorem

Hex.NumberTower.adjoin?_sound (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot) {E : T.Extension}
  (h : T.adjoin? candidate = some E) :
  Hex.NumberTower.Extension.Sound candidate E
Hex.NumberTower.adjoin?_sound
  (T : Hex.NumberTower)
  (candidate : Hex.AlgebraicRoot)
  {E : T.Extension}
  (h : T.adjoin? candidate = some E) :
  Hex.NumberTower.Extension.Sound
    candidate E

Every returned adjoining payload satisfies the fixed-embedding, generation, and identity-extension contracts.

theorem

Hex.NumberTower.flatten?_sound (T : Hex.NumberTower) {F : T.Flattening}
  (h : T.flatten? = some F) : F.Sound
Hex.NumberTower.flatten?_sound
  (T : Hex.NumberTower) {F : T.Flattening}
  (h : T.flatten? = some F) : F.Sound

Every returned primitive presentation has inverse coordinate maps, preserves arithmetic, and commutes with the fixed complex embeddings.