def Hex.NumberTower.PolynomialIrreducible (T : NumberTower) (f : T.Poly) : Prop

A nonconstant tower polynomial has no factorization into two nonconstant tower polynomials.

Equations

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

def Hex.NumberTower.Factorization.polyPow {T : NumberTower} (f : T.Poly) : ℕ → T.Poly

Executable natural power without presupposing a law-bearing monoid instance on tower coefficients.

Equations

• Hex.NumberTower.Factorization.polyPow f 0 = 1
• Hex.NumberTower.Factorization.polyPow f n.succ = Hex.NumberTower.Factorization.polyPow f n * f

def Hex.NumberTower.Factorization.reconstruct {T : NumberTower} {f : T.Poly} (r : T.Factorization f) : T.Poly

Reconstruct a polynomial from a public factorization payload.

Equations

• r.reconstruct = Array.foldl (fun (product : T.Poly) (factor : T.Poly × ℕ) => product * Hex.NumberTower.Factorization.polyPow factor.1 factor.2) (Hex.DensePoly.C r.scalar) r.factors

def Hex.NumberTower.Factorization.Sound {T : NumberTower} {f : T.Poly} (r : T.Factorization f) : Prop

Mathematical meaning of a checked factorization payload. Strict executable ordering of monic factors also rules out associates and duplicate entries.

Equations

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

theorem Hex.NumberTower.rawPolynomial_rawPoly (T : NumberTower) (f : T.Poly) : Norm.rawPolynomial T.levels.toList (Factor.rawPoly T.levels.toList (Array.map coeffs (DensePoly.toArray f))) = T.toPolynomial f

Raw canonical coordinates and the public tower polynomial have the same fixed complex interpretation.

theorem Hex.NumberTower.polyCoords_rawPoly (T : NumberTower) (f : T.Poly) : Factor.polyCoords (Factor.rawPoly T.levels.toList (Array.map coeffs (DensePoly.toArray f))) = Array.map coeffs (DensePoly.toArray f)

Public tower-polynomial coordinates are canonical raw coordinates.

theorem Hex.NumberTower.PolynomialIrreducible.toMathlib {T : NumberTower} {f : T.Poly} (hf : T.PolynomialIrreducible f) : Irreducible (HexPolyMathlib.toPolynomial f)

The executable factor-theoretic predicate implies Mathlib irreducibility.

theorem Hex.NumberTower.PolynomialIrreducible.ofMathlib {T : NumberTower} {f : T.Poly} (hf : Irreducible (HexPolyMathlib.toPolynomial f)) : T.PolynomialIrreducible f

Mathlib irreducibility implies the executable factor-theoretic predicate.

theorem Hex.NumberTower.polynomialIrreducible_iff (T : NumberTower) (f : T.Poly) : T.PolynomialIrreducible f ↔ Irreducible (HexPolyMathlib.toPolynomial f)

The executable-carrier irreducibility predicate coincides with Mathlib irreducibility of the interpreted polynomial.

theorem Hex.NumberTower.toPolynomial_polyPow (T : NumberTower) (f : T.Poly) (n : ℕ) : HexPolyMathlib.toPolynomial (Factorization.polyPow f n) = HexPolyMathlib.toPolynomial f ^ n

Semantic conversion preserves the executable natural power used in a public factorization payload.

theorem Hex.NumberTower.toPolynomial_reconstruct {T : NumberTower} {f : T.Poly} (r : T.Factorization f) : HexPolyMathlib.toPolynomial r.reconstruct = Polynomial.C r.scalar * (List.map (fun (factor : T.Poly × ℕ) => HexPolyMathlib.toPolynomial factor.1 ^ factor.2) r.factors.toList).prod

A public factorization reconstructs as its scalar times the product of the corresponding polynomial powers.

theorem Hex.NumberTower.semantic_reconstruct {T : NumberTower} {f : T.Poly} (r : T.Factorization f) : T.toPolynomial r.reconstruct = Polynomial.C (T.toComplex r.scalar) * (List.map (fun (factor : T.Poly × ℕ) => T.toPolynomial factor.1 ^ factor.2) r.factors.toList).prod

Complex interpretation of a reconstruction is the scalar times the product of the interpreted factor powers.

theorem Hex.NumberTower.isIrreducible_iff (T : NumberTower) (f : T.Poly) : Factor.isIrreducible T.levels.toList (Array.map coeffs (DensePoly.toArray f)) = true ↔ DensePoly.leadingCoeff f = 1 ∧ T.PolynomialIrreducible f

The recursive executable irreducibility test has exactly the intended factor-theoretic meaning in a validated tower.

theorem Hex.NumberTower.factor?_sound (T : NumberTower) (f : T.Poly) {r : T.Factorization f} (_h : factor? f = some r) : r.Sound

Every returned Trager factorization satisfies reconstruction, multiplicity, irreducibility, uniqueness, and ordering.

theorem Hex.NumberTower.factor?_isSome (T : NumberTower) (f : T.Poly) : (factor? f).isSome = true

Recursive Trager factorization succeeds for every tower polynomial.