Shear Equivalence for Guruswami-Sudan Multiplicity Constraints

The approximant-basis backend reduces GS interpolation to diagonal modular congruences on the Z^b-coefficients of the sheared polynomial Q(X, R + Z). This file proves the underlying semantic equivalence: for distinct interpolation nodes, the packed multiplicity constraints on Q hold iff every sheared coefficient C_b = (hasseDeriv b Q.toPoly).eval R is divisible by G^(s-b), where G is the vanishing polynomial of the nodes and R interpolates the values.

The proof works one node at a time. Writing M_b = (hasseDeriv b Q.toPoly) for the outer Y-Hasse derivatives, multiplicity at (x, y) says that the family M_b.eval (C y) is (X - x)^(s-b)-divisible, while the modular congruence constrains the family M_b.eval R. Because R and C y agree at x, an outer Taylor expansion transfers each divisibility family to the other; distinctness of the nodes then glues the per-node factors into powers of G.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.X_sub_C_pow_dvd_iff_hasseDeriv_eval_eq_zero {F : Type u_1} [Field F] (A : Polynomial F) (x : F) (k : ℕ) : (Polynomial.X - Polynomial.C x) ^ k ∣ A ↔ ∀ a < k, Polynomial.eval x ((Polynomial.hasseDeriv a) A) = 0

(X - x)^k divides A iff the first k Hasse derivatives of A vanish at x.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.X_sub_C_pow_dvd_hasseDeriv_eval_of_dvd_sub {F : Type u_1} [Field F] {P : Polynomial (Polynomial F)} {u v : Polynomial F} {x : F} {s : ℕ} (huv : Polynomial.X - Polynomial.C x ∣ v - u) (h : ∀ b < s, (Polynomial.X - Polynomial.C x) ^ (s - b) ∣ Polynomial.eval u ((Polynomial.hasseDeriv b) P)) {b : ℕ} (hb : b < s) : (Polynomial.X - Polynomial.C x) ^ (s - b) ∣ Polynomial.eval v ((Polynomial.hasseDeriv b) P)

Shear-transfer core: the (X - x)-adic divisibility family of the outer Hasse-derivative evaluations of P moves between outer evaluation points u and v that agree modulo X - x.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.X_sub_C_pow_dvd_hasseDeriv_eval_iff_hasMultiplicity {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {Q : CBivariate F} {R : Polynomial F} {x y : F} {s : ℕ} (hRx : Polynomial.eval x R = y) : (∀ b < s, (Polynomial.X - Polynomial.C x) ^ (s - b) ∣ Polynomial.eval R ((Polynomial.hasseDeriv b) Q.toPoly)) ↔ Q.hasMultiplicity s x y

At a single node (x, y) with R(x) = y, the (X - x)-adic divisibility family of the sheared coefficients (hasseDeriv b Q.toPoly).eval R is equivalent to GS multiplicity of Q at the node.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.linearFactor_toPoly_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (x : F) : (CPolynomial.linearFactor x).toPoly = Polynomial.X - Polynomial.C x

The linear factor of one node under toPoly.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.vanishingPolynomialArray_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (xs : Array F) : (CPolynomial.vanishingPolynomialArray xs).toPoly = (Multiset.map (fun (x : F) => Polynomial.X - Polynomial.C x) ↑xs.toList).prod

The array vanishing polynomial is the product of the node linear factors under toPoly.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.vanishingPolynomialArray_toPoly_monic {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (xs : Array F) : (CPolynomial.vanishingPolynomialArray xs).toPoly.Monic

The array vanishing polynomial is monic over the underlying toPoly image.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.prod_X_sub_C_pow_dvd_of_nodup {F : Type u_1} [Field F] [DecidableEq F] {A : Polynomial F} {xs : List F} {k : ℕ} (hA : A ≠ 0) (hnodup : xs.Nodup) (hroot : ∀ x ∈ xs, (Polynomial.X - Polynomial.C x) ^ k ∣ A) : (Multiset.map (fun (x : F) => Polynomial.X - Polynomial.C x) ↑xs).prod ^ k ∣ A

Per-node (X - x)^k divisibility glues to divisibility by the k-th power of the product of distinct linear factors.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.vanishing_pow_dvd_hasseDeriv_eval_iff_satisfiesMultiplicityConstraints {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] {points : Array (F × F)} {Q : CBivariate F} {R : CPolynomial F} {s : ℕ} (hdistinct : DistinctXCoordinates points) (hR : ∀ point ∈ points.toList, CPolynomial.eval point.1 R = point.2) : (∀ b < s, (CPolynomial.vanishingPolynomialArray (Array.map (fun (p : F × F) => p.1) points)).toPoly ^ (s - b) ∣ Polynomial.eval R.toPoly ((Polynomial.hasseDeriv b) Q.toPoly)) ↔ Q.SatisfiesMultiplicityConstraints points s

Batch shear equivalence: over distinct nodes, divisibility of every sheared coefficient C_b by G^(s-b) is equivalent to the packed GS multiplicity constraints.