def Hex.NumberTower.Arithmetic.fixedCoeffs (n : Nat) (coefficients : Array Rat) : Array Rat

Fixed-width rational coordinates, padding with zero and truncating excess entries.

Equations

• Hex.NumberTower.Arithmetic.fixedCoeffs n coefficients = (Vector.ofFn fun (i : Fin n) => coefficients.getD (↑i) 0).toArray

def Hex.NumberTower.Arithmetic.addCoords (n : Nat) (a b : Array Rat) : Array Rat

Fixed-width coordinate addition.

Equations

• Hex.NumberTower.Arithmetic.addCoords n a b = (Vector.ofFn fun (i : Fin n) => a.getD (↑i) 0 + b.getD (↑i) 0).toArray

def Hex.NumberTower.Arithmetic.subCoords (n : Nat) (a b : Array Rat) : Array Rat

Fixed-width coordinate subtraction.

Equations

• Hex.NumberTower.Arithmetic.subCoords n a b = (Vector.ofFn fun (i : Fin n) => a.getD (↑i) 0 - b.getD (↑i) 0).toArray

def Hex.NumberTower.Arithmetic.negCoords (n : Nat) (a : Array Rat) : Array Rat

Fixed-width coordinate negation.

Equations

• Hex.NumberTower.Arithmetic.negCoords n a = (Vector.ofFn fun (i : Fin n) => -a.getD (↑i) 0).toArray

theorem Hex.NumberTower.Arithmetic.add_subCoords (n : Nat) (a b : Array Rat) : addCoords n (subCoords n a b) b = fixedCoeffs n a

Adding back the subtrahend recovers the fixed-width minuend.

def Hex.NumberTower.Arithmetic.block (a : Array Rat) (index width : Nat) : Array Rat

One mixed-radix block.

Equations

• Hex.NumberTower.Arithmetic.block a index width = (Vector.ofFn fun (i : Fin width) => a.getD (index * width + ↑i) 0).toArray

theorem Hex.NumberTower.Arithmetic.block_fixed (count width index : Nat) (a : Array Rat) (hindex : index < count) : block (fixedCoeffs (count * width) a) index width = fixedCoeffs width (block a index width)

A block of fixed-width coordinates is the fixed-width source block.

theorem Hex.NumberTower.Arithmetic.block_one (count width index : Nat) (hindex : index < count) : block (fixedCoeffs (count * width) #[1]) index width = if index = 0 then fixedCoeffs width #[1] else fixedCoeffs width #[]

The only nonzero block of the fixed-width coordinate one is its constant block.

theorem Hex.NumberTower.Arithmetic.block_add (count width index : Nat) (a b : Array Rat) (hindex : index < count) : block (addCoords (count * width) a b) index width = addCoords width (block a index width) (block b index width)

A block of fixed-width coordinate addition is the sum of the blocks.

def Hex.NumberTower.Arithmetic.flattenBlocks (count width : Nat) (blocks : Array (Array Rat)) : Array Rat

Flatten a fixed number of equally wide coordinate blocks.

Equations

• Hex.NumberTower.Arithmetic.flattenBlocks count width blocks = if width = 0 then #[] else (Vector.ofFn fun (i : Fin (count * width)) => (blocks.getD (↑i / width) #[]).getD (↑i % width) 0).toArray

@[simp]

theorem Hex.NumberTower.Arithmetic.flattenBlocks_size (count width : Nat) (blocks : Array (Array Rat)) : (flattenBlocks count width blocks).size = count * width

Flattening fixed-width blocks always produces the requested total width.

theorem Hex.NumberTower.Arithmetic.block_flatten (count width index : Nat) (blocks : Array (Array Rat)) (hindex : index < count) : block (flattenBlocks count width blocks) index width = fixedCoeffs width (blocks.getD index #[])

Reading an in-range block after flattening recovers that source block at the fixed lower width.

def Hex.NumberTower.Arithmetic.convolveRow (degree width i : Nat) (multiply : Array Rat → Array Rat → Array Rat) (a b : Array Rat) (work : Array (Array Rat)) : Array (Array Rat)

Add one row of schoolbook block products to a convolution workspace.

Equations

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

@[simp]

theorem Hex.NumberTower.Arithmetic.convolveRow_size (degree width i : Nat) (multiply : Array Rat → Array Rat → Array Rat) (a b : Array Rat) (work : Array (Array Rat)) : (convolveRow degree width i multiply a b work).size = work.size

One convolution row edits the work array in place, preserving its size.

def Hex.NumberTower.Arithmetic.convolve (degree width : Nat) (multiply : Array Rat → Array Rat → Array Rat) (a b : Array Rat) : Array (Array Rat)

Schoolbook convolution of fixed-width coefficient blocks.

Equations

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

@[simp]

theorem Hex.NumberTower.Arithmetic.convolve_size (degree width : Nat) (multiply : Array Rat → Array Rat → Array Rat) (a b : Array Rat) : (convolve degree width multiply a b).size = 2 * degree - 1

Convolution allocates exactly the coefficient range of a product of two polynomials of degree below degree.

def Hex.NumberTower.Arithmetic.reduceCoeffs (degree width k : Nat) (defining : Array (Array Rat)) (multiply : Array Rat → Array Rat → Array Rat) (work : Array (Array Rat)) : Array (Array Rat)

Apply all lower-coefficient corrections for eliminating the coefficient at k with a monic relation.

Equations

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

@[simp]

theorem Hex.NumberTower.Arithmetic.reduceCoeffs_size (degree width k : Nat) (defining : Array (Array Rat)) (multiply : Array Rat → Array Rat → Array Rat) (work : Array (Array Rat)) : (reduceCoeffs degree width k defining multiply work).size = work.size

One coefficient-reduction step edits the work array in place, preserving its size.

def Hex.NumberTower.Arithmetic.reduceAt (degree width k : Nat) (defining : Array (Array Rat)) (multiply : Array Rat → Array Rat → Array Rat) (work : Array (Array Rat)) : Array (Array Rat)

Eliminate the coefficient at k, then discard it.

Equations

• Hex.NumberTower.Arithmetic.reduceAt degree width k defining multiply work = (Hex.NumberTower.Arithmetic.reduceCoeffs degree width k defining multiply work).take k

@[simp]

theorem Hex.NumberTower.Arithmetic.reduceAt_size (degree width k : Nat) (defining : Array (Array Rat)) (multiply : Array Rat → Array Rat → Array Rat) (work : Array (Array Rat)) (hsize : work.size = k + 1) : (reduceAt degree width k defining multiply work).size = k

One descending reduction step removes exactly its top coefficient.

def Hex.NumberTower.Arithmetic.reduce (degree width : Nat) (defining : Array (Array Rat)) (multiply : Array Rat → Array Rat → Array Rat) : Nat → Array (Array Rat) → Array (Array Rat)

Descending monic reduction of all coefficients at or above degree.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Arithmetic.reduce degree width defining multiply 0 x✝ = x✝.take degree

@[simp]

theorem Hex.NumberTower.Arithmetic.reduce_size (degree width fuel : Nat) (defining : Array (Array Rat)) (multiply : Array Rat → Array Rat → Array Rat) (work : Array (Array Rat)) (hsize : work.size = degree + fuel) : (reduce degree width defining multiply fuel work).size = degree

Descending reduction consumes its whole high-coefficient fuel.

def Hex.NumberTower.Arithmetic.mulCoords (levels : List Level) : Array Rat → Array Rat → Array Rat

Recursive mixed-radix multiplication on top-first raw level data.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Arithmetic.mulCoords [] x✝¹ x✝ = #[x✝¹.getD 0 0 * x✝.getD 0 0]

@[simp]

theorem Hex.NumberTower.Arithmetic.mulCoords_size (levels : List Level) (a b : Array Rat) : (mulCoords levels a b).size = levelsDim levels

Recursive multiplication returns exactly one mixed-radix coordinate vector.

structure Hex.NumberTower.Arithmetic.RawElem (levels : List Level) : Type

Dynamically indexed tower coefficient used internally when an algorithm recurses through runtime level data rather than a dependent NumberTower. The raw helper normalizes to the represented mixed-radix dimension.

• data : Array Rat

  The flattened mixed-radix rational coordinates.

def Hex.NumberTower.Arithmetic.raw (levels : List Level) (data : Array Rat) : RawElem levels

Wrap coordinate data as a RawElem, zero-padding or truncating to the represented mixed-radix dimension.

Equations

• Hex.NumberTower.Arithmetic.raw levels data = { data := Hex.NumberTower.Arithmetic.fixedCoeffs (Hex.NumberTower.levelsDim levels) data }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instDecidableEqRawElem (levels : List Level) : DecidableEq (RawElem levels)

Equations

• Hex.NumberTower.Arithmetic.instDecidableEqRawElem levels a b = match decEq a.data.toList b.data.toList with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instZeroRawElem (levels : List Level) : Zero (RawElem levels)

Equations

• Hex.NumberTower.Arithmetic.instZeroRawElem levels = { zero := Hex.NumberTower.Arithmetic.raw levels #[] }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instOneRawElem (levels : List Level) : One (RawElem levels)

Equations

• Hex.NumberTower.Arithmetic.instOneRawElem levels = { one := Hex.NumberTower.Arithmetic.raw levels #[1] }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instAddRawElem (levels : List Level) : Add (RawElem levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instSubRawElem (levels : List Level) : Sub (RawElem levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instNegRawElem (levels : List Level) : Neg (RawElem levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instMulRawElem (levels : List Level) : Mul (RawElem levels)

Equations

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

structure Hex.NumberTower.Arithmetic.Coeff (levels : List Level) : Type

Canonical lower-tower coefficient used by recursive inversion. Unlike the general-purpose RawElem, this type carries the fixed-width invariant needed by the semantic field bridge for polynomial xgcd.

• data : Array Rat

  The flattened mixed-radix rational coordinates.

• size_eq : self.data.size = levelsDim levels

  The coordinate array has exactly the represented dimension.

def Hex.NumberTower.Arithmetic.Coeff.ofData (levels : List Level) (data : Array Rat) : Coeff levels

Normalize arbitrary data into a canonical lower-tower coefficient.

Equations

• Hex.NumberTower.Arithmetic.Coeff.ofData levels data = { data := Hex.NumberTower.Arithmetic.fixedCoeffs (Hex.NumberTower.levelsDim levels) data, size_eq := ⋯ }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instDecidableEqCoeff (levels : List Level) : DecidableEq (Coeff levels)

Equations

• Hex.NumberTower.Arithmetic.instDecidableEqCoeff levels a b = match decEq a.data.toList b.data.toList with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instZeroCoeff (levels : List Level) : Zero (Coeff levels)

Equations

• Hex.NumberTower.Arithmetic.instZeroCoeff levels = { zero := Hex.NumberTower.Arithmetic.Coeff.ofData levels #[] }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instOneCoeff (levels : List Level) : One (Coeff levels)

Equations

• Hex.NumberTower.Arithmetic.instOneCoeff levels = { one := Hex.NumberTower.Arithmetic.Coeff.ofData levels #[1] }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instAddCoeff (levels : List Level) : Add (Coeff levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instSubCoeff (levels : List Level) : Sub (Coeff levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instNegCoeff (levels : List Level) : Neg (Coeff levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instMulCoeff (levels : List Level) : Mul (Coeff levels)

Equations

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

def Hex.NumberTower.Arithmetic.Coeff.value (level : Level) (lower : List Level) (a : Array Rat) : DensePoly (Coeff lower)

View one top-level coordinate array as a polynomial over canonical lower tower coefficients.

Equations

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

def Hex.NumberTower.Arithmetic.Coeff.relation (level : Level) (lower : List Level) : DensePoly (Coeff lower)

The monic defining relation as a polynomial over canonical lower-tower coefficients.

Equations

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

def Hex.NumberTower.Arithmetic.invCoords (levels : List Level) : Array Rat → Array Rat

Recursive inverse coordinates. The zero convention is inherited at every level; defensive nonconstant/zero gcd branches are unreachable for certified level lists. The extended gcd makes every remainder monic before dividing by it, so each lower-field inversion acts on a normalized operand and the quotient coefficients stay bounded in height; the unnormalized DensePoly.xgcdLeft chain amplified the heights of every later lower-field inversion.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Arithmetic.invCoords [] x✝ = #[if x✝.getD 0 0 = 0 then 0 else (x✝.getD 0 0)⁻¹]

@[simp]

theorem Hex.NumberTower.Arithmetic.invCoords_size (levels : List Level) (a : Array Rat) : (invCoords levels a).size = levelsDim levels

Recursive inversion always returns the canonical mixed-radix width, including its defensive zero fallbacks.

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instInvRawElem (levels : List Level) : Inv (RawElem levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instDivRawElem (levels : List Level) : Div (RawElem levels)

Equations

• Hex.NumberTower.Arithmetic.instDivRawElem levels = { div := fun (a b : Hex.NumberTower.Arithmetic.RawElem levels) => a * b⁻¹ }

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instInvCoeff (levels : List Level) : Inv (Coeff levels)

Equations

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

@[instance_reducible]

instance Hex.NumberTower.Arithmetic.instDivCoeff (levels : List Level) : Div (Coeff levels)

Equations

• Hex.NumberTower.Arithmetic.instDivCoeff levels = { div := fun (a b : Hex.NumberTower.Arithmetic.Coeff levels) => a * b⁻¹ }