theorem Hex.Berlekamp.isUnitPolynomial_one_FpPoly {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] : isUnitPolynomial 1 = true

The constant polynomial 1 : FpPoly p is recognised as a unit by isUnitPolynomial.

theorem Hex.Berlekamp.dvd_one_of_isUnitPolynomial {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {u : FpPoly p} (hu : isUnitPolynomial u = true) : u ∣ 1

A polynomial accepted by isUnitPolynomial (degree-zero, hence a nonzero constant) divides 1 : FpPoly p.

theorem Hex.Berlekamp.squareFree_common_of_gcd_eq_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {r : FpPoly p} (hsf : DensePoly.gcd r (DensePoly.derivative r) = 1) (d : FpPoly p) : d ∣ r → d ∣ DensePoly.derivative r → isUnitPolynomial d = true

Adapter from the strict executable-gcd form of square-freeness (DensePoly.gcd r r' = 1) to the relaxed common-divisor form (∀ d, d ∣ r → d ∣ r' → isUnitPolynomial d). The relaxed form is the shape the soundness chain culminating in berlekampFactor_singleton_irreducible consumes; the strict form is what existing in-tree callers carry, so this adapter lets them feed the chain unchanged.

theorem Hex.Berlekamp.isUnitPolynomial_of_squareFree_of_squared_dvd {p : Nat} [ZMod64.Bounds p] {r g : FpPoly p} (hsf : ∀ (d : FpPoly p), d ∣ r → d ∣ DensePoly.derivative r → isUnitPolynomial d = true) (hgg : g * g ∣ r) : isUnitPolynomial g = true

Strong square-free characterization: if every common divisor of r and its derivative is a unit, then any g with g * g ∣ r is itself a unit (via isUnitPolynomial).

theorem Hex.Berlekamp.common_dvd_one_of_squareFree_mul {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {a b d : FpPoly p} (hsquareFree : ∀ (e : FpPoly p), e ∣ a * b → e ∣ DensePoly.derivative (a * b) → isUnitPolynomial e = true) (hda : d ∣ a) (hdb : d ∣ b) : d ∣ 1

If the product a * b is square-free, then any common divisor d of the two factors a and b divides 1, since d * d ∣ a * b forces d to be a unit.

theorem Hex.Berlekamp.exists_reduced_crtZeroOne_kernelWitness_of_squareFree_split {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (a b : FpPoly p) (ha : DensePoly.Monic a) (hb : DensePoly.Monic b) (ha_pos : 0 < DensePoly.natDegree a) (hb_pos : 0 < DensePoly.natDegree b) (hsquareFree : ∀ (d : FpPoly p), d ∣ a * b → d ∣ DensePoly.derivative (a * b) → isUnitPolynomial d = true) (hgcd_monic : (DensePoly.gcd a b).Monic) : ∃ (h : FpPoly p), h = crtZeroOneXGCDCandidate a b % (a * b) ∧ a * b ∣ h.linearPow (p ^ 1) - h ∧ ∀ (c : ZMod64 p), ¬DensePoly.Congr h (DensePoly.C c) (a * b)

Square-free product specialization of exists_reduced_crtZeroOne_kernelWitness_of_coprime_split. The extra monicity hypothesis on the executable gcd connects the common-divisor form supplied by square-freeness to the gcd a b = 1 surface used by the XGCD-backed CRT candidate.

theorem Hex.Berlekamp.isUnitPolynomial_gcd_quotient_of_squareFree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] (r d : FpPoly p) (hsf : DensePoly.gcd r (DensePoly.derivative r) = 1) : isUnitPolynomial (DensePoly.gcd (r / DensePoly.gcd r d) d) = true

For square-free r (gcd r r' = 1), the gcd of d with the cofactor r / gcd r d is a unit, the gcd-quotient unit recognition used by the square-free distinct-degree check.

theorem Hex.Berlekamp.witnessLinearFactor_distinct_common_dvd_one {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {w : FpPoly p} {c d : ZMod64 p} (hcd : c ≠ d) (e : FpPoly p) (hec : e ∣ w - FpPoly.C c) (hed : e ∣ w - FpPoly.C d) : e ∣ 1

Distinct witness linear factors (w - C c) and (w - C d) are coprime: their difference is a nonzero constant, so any common divisor divides 1.

theorem Hex.Berlekamp.exists_gcd_not_isUnit_of_witnessProduct_dvd_of_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f w : FpPoly p} (hf_pos : 0 < DensePoly.natDegree f) (hdvd : f ∣ List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (w - FpPoly.C c)) 1 (ZMod64.values p)) : ∃ (c : ZMod64 p), isUnitPolynomial (DensePoly.gcd f (w - FpPoly.C c)) = false

Square-free divisor distribution (non-unit existence): if f has positive degree and divides the canonical witness product over F_p, some gcd(f, w - C c) is non-unit. The proof uses only coprime cancellation and the divisibility hypothesis.

theorem Hex.Berlekamp.exists_nontrivial_gcd_of_witnessProduct_dvd_of_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f w : FpPoly p} (hf_pos : 0 < DensePoly.natDegree f) (hdvd : f ∣ List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (w - FpPoly.C c)) 1 (ZMod64.values p)) (hnonconst : ∀ (c : ZMod64 p), ¬f ∣ w - FpPoly.C c) : ∃ (c : ZMod64 p), (DensePoly.gcd f (w - FpPoly.C c)).isZero = false ∧ (DensePoly.gcd f (w - FpPoly.C c)).degree? ≠ some 0 ∧ DensePoly.gcd f (w - FpPoly.C c) ≠ f

Square-free divisor distribution (nontrivial split): under the non-constancy hypothesis that no single (w - C c) is divisible by f, some witness gcd is nonzero, nonconstant, and not equal to f. This is the form consumed by the executable Berlekamp split surface (see HexBerlekamp.Berlekamp.kernelWitnessSplit?_some_of_nontrivial_splitFactorAt).

f does not need to be square-free for this statement. Square-freeness is used at the call site to derive the witness-level divisibility hypothesis.

theorem Hex.Berlekamp.exists_kernelWitnessSplit?_some_of_witnessProduct_dvd_of_pos_degree {p : Nat} [ZMod64.Bounds p] [ZMod64.PrimeModulus p] {f w : FpPoly p} (hf_pos : 0 < DensePoly.natDegree f) (hdvd : f ∣ List.foldl (fun (acc : FpPoly p) (c : ZMod64 p) => acc * (w - FpPoly.C c)) 1 (ZMod64.values p)) (hnonconst : ∀ (c : ZMod64 p), ¬f ∣ w - FpPoly.C c) : ∃ (r : SplitResult p), kernelWitnessSplit? f w = some r

Executable composition of the square-free distribution step: once the witness-product divisibility hypothesis is available and the witness is not constant modulo f, the Berlekamp split search finds a concrete split result.

The upstream derivation of hdvd from a fixed-space/kernel hypothesis is kept separate; this theorem only packages the local distribution result with the executable search reflection.