structure Hex.NumberTower.Level : Type

Runtime data for one monic algebraic extension. defining[j] is the flattened lower-tower coefficient of X^j; the omitted coefficient of X^degree is one.

• degree : Nat

  Relative degree of this extension over the tower below it.

• defining : Array (Array Rat)

  Lower coefficients of the monic defining polynomial, each flattened to the lower tower's mixed-radix coordinates.

• root : AlgebraicRoot

  The absolute algebraic root chosen as this level's generator.

def Hex.NumberTower.levelsDim : List Level → Nat

Dimension represented by a top-first list of extension levels.

Equations

• Hex.NumberTower.levelsDim [] = 1
• Hex.NumberTower.levelsDim (level :: lower) = level.degree * Hex.NumberTower.levelsDim lower

def Hex.NumberTower.Level.Structural (level : Level) (lowerDim : Nat) : Prop

Structural validity of one level above a lower field of dimension lowerDim.

Equations

• level.Structural lowerDim = (1 < level.degree ∧ level.defining.size = level.degree ∧ ∀ (i : Nat) (h : i < level.defining.size), level.defining[i].size = lowerDim)

def Hex.NumberTower.Level.structuralCheck (level : Level) (lowerDim : Nat) : Bool

Executable structural check for one raw level.

Equations

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

theorem Hex.NumberTower.Level.structural_of_check {level : Level} {lowerDim : Nat} (h : level.structuralCheck lowerDim = true) : level.Structural lowerDim

The executable structural check exposes the erased width invariant used by the certified wrapper.