theorem Hex.SquareClass.isPerfectSquare_eq_true_iff (m : ℤ) : isPerfectSquare m = true ↔ IsSquare m

Hex.isPerfectSquare decides IsSquare on ℤ.

theorem Hex.SquareClass.length_squareClassProducts (l : List ℤ) : (squareClassProducts l).length + 1 = 2 ^ l.length

There are 2ⁿ - 1 subproducts, one per nonempty sublist. Stated additively so no truncated subtraction appears.

theorem Hex.SquareClass.mem_squareClassProducts (l : List ℤ) (m : ℤ) : m ∈ squareClassProducts l ↔ ∃ (t : List ℤ), t.Sublist l ∧ t ≠ [] ∧ t.prod = m

The enumerated subproducts are exactly the products of the nonempty sublists.

theorem Hex.SquareClass.independentSquareClasses_iff (ds : Array ℤ) : independentSquareClasses ds = true ↔ Independent ds.toList

The executable check decides independence: this is the whole arithmetic trust surface of the certificate's first half.

theorem HexBerlekampZassenhausMathlib.toPolynomial_shift_one (p : Hex.ZPoly) : HexPolyZMathlib.toPolynomial (Hex.DensePoly.shift 1 p) = Polynomial.X * HexPolyZMathlib.toPolynomial p

Prepending one zero coefficient is multiplication by X.

theorem HexBerlekampZassenhausMathlib.toPolynomial_scale (c : ℤ) (p : Hex.ZPoly) : HexPolyZMathlib.toPolynomial (Hex.DensePoly.scale c p) = Polynomial.C c * HexPolyZMathlib.toPolynomial p

Coefficientwise scaling is multiplication by a constant.

theorem HexBerlekampZassenhausMathlib.toPolynomial_ofList_cons (a : ℤ) (as : List ℤ) : HexPolyZMathlib.toPolynomial (Hex.DensePoly.ofList (a :: as)) = Polynomial.C a + Polynomial.X * HexPolyZMathlib.toPolynomial (Hex.DensePoly.ofList as)

Reading one more coefficient off the front is one Horner step.

theorem HexBerlekampZassenhausMathlib.toPolynomial_linear (c : ℤ) : HexPolyZMathlib.toPolynomial (Hex.DensePoly.ofCoeffs #[-c, 1]) = Polynomial.X - Polynomial.C c

The polynomial the iteration starts from.

theorem HexBerlekampZassenhausMathlib.quadShift_spec {K : Type u_1} [CommRing K] (d : ℤ) {r : K} (hr : r ^ 2 = ↑d) (l : List ℤ) : Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial (Hex.quadShift d l).1) + Polynomial.C r * Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial (Hex.quadShift d l).2) = (Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial (Hex.DensePoly.ofList l))).comp (Polynomial.X - Polynomial.C r)

The synthetic shift is correct: with r² = d in K, the pair (p, q) that Hex.quadShift builds off the coefficient list l satisfies p + r · q = g(X - r) over K, where g is the polynomial with those coefficients.

Everything else follows from this by substituting -r for r and multiplying.

theorem HexBerlekampZassenhausMathlib.map_quadNorm {K : Type u_1} [CommRing K] (g : Hex.ZPoly) (d : ℤ) (r : K) (hr : r ^ 2 = ↑d) : Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial (Hex.quadNorm d g)) = (Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial g)).comp (Polynomial.X - Polynomial.C r) * (Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial g)).comp (Polynomial.X + Polynomial.C r)

The norm correspondence: over a commutative ring K carrying a square root r of d, the executable quadratic norm is g(X - r) · g(X + r).

def HexBerlekampZassenhausMathlib.signedSums {K : Type u_1} [CommRing K] (rs : List K) : List K

The 2ⁿ signed sums ∑ᵢ εᵢ rᵢ, in the order the tower builds them.

Equations

• HexBerlekampZassenhausMathlib.signedSums rs = List.foldl (fun (ss : List K) (r : K) => List.flatMap (fun (s : K) => [s + r, s - r]) ss) [0] rs

noncomputable def HexBerlekampZassenhausMathlib.signPatternPoly {K : Type u_1} [CommRing K] (c : K) (rs : List K) : Polynomial K

F(c; d₁, …, dₙ) = ∏_{ε ∈ {±1}ⁿ} (X - c - ∑ᵢ εᵢ rᵢ), the polynomial the multiquadratic tower theorem is about, written over the square roots rs.

Equations

• HexBerlekampZassenhausMathlib.signPatternPoly c rs = (List.map (fun (s : K) => Polynomial.X - Polynomial.C (c + s)) (HexBerlekampZassenhausMathlib.signedSums rs)).prod

@[simp]

theorem HexBerlekampZassenhausMathlib.length_signedSums {K : Type u_1} [CommRing K] (rs : List K) : (signedSums rs).length = 2 ^ rs.length

There are 2ⁿ sign patterns, so the certified polynomial has 2ⁿ roots counted with multiplicity.

theorem HexBerlekampZassenhausMathlib.monic_signPatternPoly {K : Type u_1} [CommRing K] (c : K) (rs : List K) : (signPatternPoly c rs).Monic

The sign-pattern product is monic.

theorem HexBerlekampZassenhausMathlib.natDegree_signPatternPoly {K : Type u_1} [CommRing K] [Nontrivial K] (c : K) (rs : List K) : (signPatternPoly c rs).natDegree = 2 ^ rs.length

The sign-pattern product has degree 2ⁿ, so the correspondence is not vacuous: the certified polynomial really has the doubled degree at every level.

theorem HexBerlekampZassenhausMathlib.map_foldl_quadNorm {K : Type u_1} [CommRing K] (g : Hex.ZPoly) {ds : List ℤ} {rs : List K} (h : List.Forall₂ (fun (d : ℤ) (r : K) => r ^ 2 = ↑d) ds rs) : Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial (List.foldl (fun (g : Hex.ZPoly) (d : ℤ) => Hex.quadNorm d g) g ds)) = List.foldl (fun (P : Polynomial K) (r : K) => P.comp (Polynomial.X - Polynomial.C r) * P.comp (Polynomial.X + Polynomial.C r)) (Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial g)) rs

Each successive norm is one composition pair, for any starting polynomial.

theorem HexBerlekampZassenhausMathlib.map_iteratedNorm {K : Type u_1} [CommRing K] (c : ℤ) (ds : Array ℤ) {rs : List K} (h : List.Forall₂ (fun (d : ℤ) (r : K) => r ^ 2 = ↑d) ds.toList rs) : Polynomial.map (algebraMap ℤ K) (HexPolyZMathlib.toPolynomial (Hex.iteratedNorm c ds)) = signPatternPoly (↑c) rs

The iterated quadratic norm is the sign-pattern product: over any commutative ring carrying square roots rs of the radicands ds, the executable Hex.iteratedNorm maps to ∏_ε (X - c - ∑ᵢ εᵢ rᵢ).

theorem HexBerlekampZassenhausMathlib.toPolynomial_inj {p q : Hex.ZPoly} (h : HexPolyZMathlib.toPolynomial p = HexPolyZMathlib.toPolynomial q) : p = q

Coefficient equality is polynomial equality: the identification half of the check compares dense coefficient arrays, and that comparison is exactly equality in Polynomial ℤ.

theorem HexBerlekampZassenhausMathlib.independent_of_check {cert : Hex.QuadraticNormCertificate} {f : Hex.ZPoly} (h : cert.check f = true) : Hex.SquareClass.Independent cert.radicands.toList

A successful check certifies independent square classes.

theorem HexBerlekampZassenhausMathlib.normalizePrimitiveSign_eq_of_check {cert : Hex.QuadraticNormCertificate} {f : Hex.ZPoly} (h : cert.check f = true) : f.normalizePrimitiveSign = Hex.iteratedNorm cert.translation cert.radicands

A successful check identifies the input with the iterated norm, up to sign.

theorem HexBerlekampZassenhausMathlib.toPolynomial_eq_or_neg_of_check {cert : Hex.QuadraticNormCertificate} {f : Hex.ZPoly} (h : cert.check f = true) : HexPolyZMathlib.toPolynomial f = HexPolyZMathlib.toPolynomial (Hex.iteratedNorm cert.translation cert.radicands) ∨ HexPolyZMathlib.toPolynomial f = -HexPolyZMathlib.toPolynomial (Hex.iteratedNorm cert.translation cert.radicands)

The identification half, in Polynomial ℤ: a successful check pins the input to the iterated norm up to the unit -1.

theorem HexBerlekampZassenhausMathlib.associated_toPolynomial_of_check {cert : Hex.QuadraticNormCertificate} {f : Hex.ZPoly} (h : cert.check f = true) : Associated (HexPolyZMathlib.toPolynomial f) (HexPolyZMathlib.toPolynomial (Hex.iteratedNorm cert.translation cert.radicands))

A successful check makes the input an associate of the iterated norm, so the two are irreducible together.