def Hex.quadStep (d a : Int) (h : ZPoly × ZPoly) : ZPoly × ZPoly

One synthetic-shift step in (ℤ[t]/(t² - d))[X]: from the pair of h = p + q · t and the next coefficient a, the pair of a + (X - t) · h.

Since t² = d, (X - t) · (p + q t) = (X p - d q) + (X q - p) t, so the step reads both components of h and writes both components of the result.

Equations

• Hex.quadStep d a h = (Hex.DensePoly.shift 1 h.fst - Hex.DensePoly.scale d h.snd + Hex.DensePoly.C a, Hex.DensePoly.shift 1 h.snd - h.fst)

def Hex.quadShift (d : Int) (coeffs : List Int) : ZPoly × ZPoly

The coefficient pair of g(X - t) in (ℤ[t]/(t² - d))[X], read off the ascending coefficient list of g: Hex.quadShift returns (p, q) with g(X - t) = p + q · t.

This is the synthetic Taylor shift with shift constant -t, carrying the coefficient pair through Horner's rule from the top coefficient down.

Equations

• Hex.quadShift d coeffs = List.foldr (Hex.quadStep d) (0, 0) coeffs

def Hex.quadNorm (d : Int) (g : ZPoly) : ZPoly

N_d(g) = g(X - t) · g(X + t) with t² = d, an integer polynomial.

Writing g(X - t) = p + q t, the conjugate is p - q t and the product is p² - d q²: the t component cancels by antisymmetry, so only the rational part is ever materialized.

Equations

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

theorem Hex.quadShift_nil (d : Int) : quadShift d [] = (0, 0)

The empty coefficient list is the zero polynomial.

theorem Hex.quadShift_cons (d a : Int) (as : List Int) : quadShift d (a :: as) = quadStep d a (quadShift d as)

Reading one more coefficient off the front is one Hex.quadStep.

theorem Hex.quadNorm_eq (d : Int) (g : ZPoly) : quadNorm d g = (quadShift d (DensePoly.toArray g).toList).fst * (quadShift d (DensePoly.toArray g).toList).fst - DensePoly.scale d ((quadShift d (DensePoly.toArray g).toList).snd * (quadShift d (DensePoly.toArray g).toList).snd)

The norm in terms of the shifted pair, with the t component already cancelled.

def Hex.iteratedNorm (c : Int) (ds : Array Int) : ZPoly

F(c; ds) = N_{dₖ}(⋯ N_{d₁}(X - c) ⋯), the iterated quadratic norm of the translation c along the radicands ds.

Equations

• Hex.iteratedNorm c ds = Array.foldl (fun (g : Hex.ZPoly) (d : Int) => Hex.quadNorm d g) (Hex.DensePoly.ofCoeffs #[-c, 1]) ds

def Hex.isPerfectSquare (m : Int) : Bool

Is m the square of an integer?

Equations

• Hex.isPerfectSquare (Int.ofNat n) = (n.sqrt * n.sqrt == n)
• Hex.isPerfectSquare (Int.negSucc a) = false

def Hex.squareClassProducts : List Int → List Int

The 2ⁿ - 1 products of the nonempty sublists of ds.

The head contributes its own singleton and doubles every product from the tail, once with and once without it.

Equations

• Hex.squareClassProducts [] = []
• Hex.squareClassProducts (d :: ds) = d :: List.flatMap (fun (m : Int) => [m, d * m]) (Hex.squareClassProducts ds)

def Hex.independentSquareClasses (ds : Array Int) : Bool

Are the radicands multiplicatively independent in ℚ*/(ℚ*)²?

Equivalently: is no nonempty subproduct a perfect square? A zero radicand and a repeated radicand are both rejected by this, as they must be.

Equations

• Hex.independentSquareClasses ds = (Hex.squareClassProducts ds.toList).all fun (m : Int) => !Hex.isPerfectSquare m

structure Hex.QuadraticNormCertificate : Type

Translation and radicands for one iterated quadratic norm.

• translation : Int

  The translation: the certified polynomial is ∏_ε (X - c - ∑ εᵢ √dᵢ).

• radicands : Array Int

  The radicands, in the order the norms are taken.

def Hex.instReprQuadraticNormCertificate.repr : QuadraticNormCertificate → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.instReprQuadraticNormCertificate : Repr QuadraticNormCertificate

Equations

• Hex.instReprQuadraticNormCertificate = { reprPrec := Hex.instReprQuadraticNormCertificate.repr }

@[instance_reducible]

instance Hex.instInhabitedQuadraticNormCertificate : Inhabited QuadraticNormCertificate

Equations

• Hex.instInhabitedQuadraticNormCertificate = { default := Hex.instInhabitedQuadraticNormCertificate.default }

def Hex.QuadraticNormCertificate.check (cert : QuadraticNormCertificate) (f : ZPoly) : Bool

Does the certificate prove f irreducible?

A true result asserts both halves: the radicands are independent, and f is, up to the unit -1, exactly the iterated quadratic norm they describe.

Every F(c; d) is monic and -1 is a unit of ℤ[X], so f and -f are irreducible together; that sign is the whole normalization the identification needs. There is no scaling and no content division, since a primitive integer polynomial with leading coefficient outside {1, -1} is never ± F(c; d).

Equations

• cert.check f = (Hex.independentSquareClasses cert.radicands && Hex.iteratedNorm cert.translation cert.radicands == f.normalizePrimitiveSign)