structure Hex.NumberTower.Flattening (T : NumberTower) : Type

A one-generator presentation of a tower together with checked executable coordinate conversions in both directions.

• root : AlgebraicNumber

  The canonical primitive element generating the whole tower.

• toPrimitive : T.Elem → QAdjoin self.root

  Rewrite tower coordinates in the primitive presentation.

• fromPrimitive : QAdjoin self.root → T.Elem

  Evaluate primitive coordinates back to a tower element.

def Hex.NumberTower.flattenShiftCount (dimension : Nat) : Nat

The finite combined bound for primitive-element and coordinate-recovery collisions in a field of dimension dimension.

Equations

• Hex.NumberTower.flattenShiftCount dimension = Hex.Nat.choose dimension 2 + 1

structure Hex.NumberTower.Flatten.Generator (T : NumberTower) : Type

One exact absolute generator and its mixed-radix coordinate in the final tower.

• degree : Nat

  The generator's relative degree at its level.

• root : AlgebraicNumber

  The exactified canonical value of the generator.

• value : T.Elem

  The generator's mixed-radix coordinate in the final tower.

structure Hex.NumberTower.Flatten.Candidate (T : NumberTower) : Type

A primitive generator accumulated through the lower part of the tower.

• dimension : Nat

  The mixed-radix dimension generated so far.

• root : AlgebraicNumber

  The canonical primitive element accumulated so far.

• value : T.Elem

  The accumulated primitive element as a tower coordinate.

• coordinates : Array (PolyQuot self.root.p self.root.x)

  Each combined generator's coordinate in the accumulated presentation.

def Hex.NumberTower.Flatten.unitCoords (dimension index : Nat) : Array Rat

Standard coordinate vector of length dimension.

Equations

• Hex.NumberTower.Flatten.unitCoords dimension index = (Array.replicate dimension 0).set! index 1

def Hex.NumberTower.Flatten.generatorsAux? (T : NumberTower) : List Level → Option (Array (Generator T) × Nat)

Exactify a top-first level suffix from the oldest level upward, returning the accumulated generators and its mixed-radix dimension.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Flatten.generatorsAux? T [] = some (#[], 1)

def Hex.NumberTower.Flatten.generators? (T : NumberTower) : Option (Array (Generator T))

Exactify the stored roots from the oldest level upward and pair them with their canonical mixed-radix generator coordinates in the final tower.

Equations

• Hex.NumberTower.Flatten.generators? T = do let state ← Hex.NumberTower.Flatten.generatorsAux? T T.levels.toList if state.snd = T.dim then some state.fst else none

def Hex.NumberTower.Flatten.candidateAt? (theta alpha : AlgebraicNumber) (target index : Nat) : Option (Int × AlgebraicNumber)

Try one deterministic signed shift for a candidate of the full required degree.

Equations

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

def Hex.NumberTower.Flatten.liftZPoly {p : ZPoly} {x : SimpleRoot p} (f : ZPoly) : DensePoly (PolyQuot p x)

Lift an integer polynomial coefficientwise into a fixed primitive presentation.

Equations

• Hex.NumberTower.Flatten.liftZPoly f = Hex.DensePoly.ofCoeffs (Array.map (fun (coefficient : Int) => ↑coefficient • 1) (Hex.DensePoly.toArray f))

def Hex.NumberTower.Flatten.evalRatPoly {p : ZPoly} {x : SimpleRoot p} (f : DensePoly Rat) (a : PolyQuot p x) : PolyQuot p x

Evaluate a rational coordinate polynomial in another fixed presentation.

Equations

• Hex.NumberTower.Flatten.evalRatPoly f a = Array.foldr (fun (coefficient : Rat) (value : Hex.PolyQuot p x) => value * a + coefficient • 1) 0 f.toArray

def Hex.NumberTower.Flatten.tracePair? (theta alpha gamma : AlgebraicNumber) : Option (PolyQuot gamma.p gamma.x × PolyQuot gamma.p gamma.x)

Recover both inputs through the proved-total trace-pairing coordinates of a primitive candidate.

Equations

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

def Hex.NumberTower.Flatten.checkCoordinate? (target gamma : AlgebraicNumber) (coordinate : PolyQuot gamma.p gamma.x) : Option (PolyQuot gamma.p gamma.x)

Validate a recovered primitive coordinate against its canonical algebraic target.

Equations

• Hex.NumberTower.Flatten.checkCoordinate? target gamma coordinate = do let recovered ← coordinate.toAlgebraicNumber? gamma.rep ⋯ if (recovered == target) = true then some coordinate else none

def Hex.NumberTower.Flatten.checkPair? (theta alpha gamma : AlgebraicNumber) (coordinates : PolyQuot gamma.p gamma.x × PolyQuot gamma.p gamma.x) : Option (PolyQuot gamma.p gamma.x × PolyQuot gamma.p gamma.x)

Validate both fast gcd coordinates before exposing them.

Equations

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

def Hex.NumberTower.Flatten.recoverPairFast? (theta alpha gamma : AlgebraicNumber) (shift : Int) : Option (PolyQuot gamma.p gamma.x × PolyQuot gamma.p gamma.x)

Recover theta and alpha in a candidate presentation gamma = theta + shift * alpha using the validated linear-gcd path only.

Equations

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

def Hex.NumberTower.Flatten.recoverPair? (theta alpha gamma : AlgebraicNumber) (shift : Int) : Option (PolyQuot gamma.p gamma.x × PolyQuot gamma.p gamma.x)

Recover theta and alpha in a primitive candidate presentation. The bounded scan uses only recoverPairFast?; this total fallback adds trace pairing for the maximum-degree candidate and for a zero shift.

Equations

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

structure Hex.NumberTower.Flatten.Recovered : Type

A full-degree primitive candidate together with its recovered old and new generator coordinates.

• shift : Int

  The signed shift producing the accepted candidate.

• root : AlgebraicNumber

  The accepted full-degree primitive candidate.

• thetaCoordinate : PolyQuot self.root.p self.root.x

  The prior generator's coordinate in the candidate presentation.

• alphaCoordinate : PolyQuot self.root.p self.root.x

  The new generator's coordinate in the candidate presentation.

def Hex.NumberTower.Flatten.searchRecoveredAux (theta alpha : AlgebraicNumber) (target start : Nat) : Nat → Option Recovered

Search a prescribed shift suffix, rejecting degree collisions and any candidate for which validated linear-gcd recovery fails.

Equations

• One or more equations did not get rendered due to their size.
• Hex.NumberTower.Flatten.searchRecoveredAux theta alpha target start 0 = none

def Hex.NumberTower.Flatten.searchRecovered? (theta alpha : AlgebraicNumber) (target : Nat) : Option Recovered

Try the direct full-degree search first. If it is exhausted, select a maximum-degree primitive candidate and recover both input coordinates through the generated field.

Equations

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

def Hex.NumberTower.Flatten.candidate? {T : NumberTower} (generators : Array (Generator T)) : Option (Candidate T)

Combine the fixed generators one level at a time, retaining a tower coordinate for each accepted canonical primitive element.

Equations

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

def Hex.NumberTower.Flatten.extendBasis {p : ZPoly} {x : SimpleRoot p} (basis : Array (PolyQuot p x)) (generator : PolyQuot p x) (degree : Nat) : Array (PolyQuot p x)

Extend lower mixed-radix basis images by powers of one newly recovered generator. The lower basis remains the fastest-varying coordinate block.

Equations

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

def Hex.NumberTower.Flatten.basisImages {T : NumberTower} {p : ZPoly} {x : SimpleRoot p} (generators : Array (Generator T)) (coordinates : Array (PolyQuot p x)) : Array (PolyQuot p x)

Images of the full tower mixed-radix basis in the primitive presentation.

Equations

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

def Hex.NumberTower.Flatten.toPrimitiveWith {T : NumberTower} {p : ZPoly} {x : SimpleRoot p} (images : Array (PolyQuot p x)) (a : T.Elem) : PolyQuot p x

Apply a rational coordinate vector to precomputed primitive-basis images.

Equations

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

def Hex.NumberTower.Flatten.fromPrimitiveWith {T : NumberTower} {p : ZPoly} {x : SimpleRoot p} (generator : T.Elem) (a : PolyQuot p x) : T.Elem

Evaluate a reduced primitive coordinate polynomial at its tower element.

Equations

• Hex.NumberTower.Flatten.fromPrimitiveWith generator a = Array.foldr (fun (coefficient : Rat) (value : T.Elem) => value * generator + T.ofRat coefficient) 0 a.coeffs.toArray

def Hex.NumberTower.Flatten.evalZPoly {T : NumberTower} (f : ZPoly) (a : T.Elem) : T.Elem

Evaluate an integer polynomial at a tower element.

Equations

• Hex.NumberTower.Flatten.evalZPoly f a = Array.foldr (fun (coefficient : Int) (value : T.Elem) => value * a + T.ofRat ↑coefficient) 0 (Hex.DensePoly.toArray f)

def Hex.NumberTower.Flatten.certifies {T : NumberTower} (candidate : Candidate T) (images : Array (PolyQuot candidate.root.p candidate.root.x)) : Bool

Verify the coordinate composite on the tower basis and check that the candidate tower element satisfies its claimed primitive minimal polynomial. The first condition makes the rational-linear coordinate maps inverse; the root relation and irreducibility make evaluation through the primitive quotient an injective ring map. The resulting dimension squeeze makes the linear inverse multiplicative as well. The size, dimension, and root checks remain independent executable defenses even where the semantic proof can derive them from the successful construction.

Equations

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

def Hex.NumberTower.flatten? (T : NumberTower) : Option T.Flattening

Replace a checked tower by one canonical primitive-element presentation. The result is returned only after exact generator recovery, a tower-basis round trip, and the primitive polynomial relation succeed.

Equations

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