Executable GS Modular-Data Bridges

Semantic characterizations of the executable approximant-basis modular data: the modulus array gsModuli, the incrementally built binomial relation matrix gsRelationColumn / gsRelationMatrixWithModuli, and the executable row predicate rowSatisfiesModularBool. The main result identifies the modular row predicate over the GS data with divisibility of every sheared coefficient (hasseDeriv b Q.toPoly).eval R by G^(s-b).

Generic helpers

theorem CompPoly.GuruswamiSudan.ApproximantBasis.ofFn_rowGet {F : Type u_1} [Field F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) {i j : ℕ} (hi : i < rows) (hj : j < width) : PolynomialMatrix.rowGet (Array.getD (PolynomialMatrix.ofFn rows width entry) i #[]) j = entry i j

Entry access for PolynomialMatrix.ofFn.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.ofFn_size {F : Type u_1} [Field F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) : Array.size (PolynomialMatrix.ofFn rows width entry) = rows

Row count of PolynomialMatrix.ofFn.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.ofFn_matrixWidth {F : Type u_1} [Field F] (rows width : ℕ) (entry : ℕ → ℕ → CPolynomial F) (hrows : 0 < rows) : (PolynomialMatrix.ofFn rows width entry).MatrixWidth = width

Width of PolynomialMatrix.ofFn with at least one row.

Modular reduction semantics

theorem CompPoly.GuruswamiSudan.ApproximantBasis.modByMonicWith_toPoly {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) {p M : CPolynomial F} (hM : M.toPoly.Monic) : (PolynomialMatrix.modByMonicWith modCtx p M).toPoly = p.toPoly %ₘ M.toPoly

modByMonicWith computes the Mathlib monic remainder under toPoly.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.dvd_modByMonicWith_sub {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) {p M : CPolynomial F} (hM : M.toPoly.Monic) : M.toPoly ∣ (PolynomialMatrix.modByMonicWith modCtx p M).toPoly - p.toPoly

modByMonicWith is congruent to the identity modulo the modulus.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.modByMonicWith_eq_zero_iff_dvd {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (modCtx : CPolynomial.ModContext F) {p M : CPolynomial F} (hM : M.toPoly.Monic) : PolynomialMatrix.modByMonicWith modCtx p M = 0 ↔ M.toPoly ∣ p.toPoly

The executable remainder vanishes exactly on multiples of the modulus.

The GS modulus array

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsModuli_eq {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : ℕ) : gsModuli mulCtx G s = (List.map (fun (i : ℕ) => G ^ (i + 1)) (List.range s)).toArray.reverse

Closed form for the GS modulus array before reversal.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsModuli_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) (s : ℕ) : (gsModuli mulCtx G s).size = s

The GS modulus array has one modulus per multiplicity level.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsModuli_getD {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) {b s : ℕ} (hb : b < s) : (gsModuli mulCtx G s).getD b 0 = G ^ (s - b)

The b-th GS modulus is G^(s-b).

The GS relation column

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationColumn_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R modulus : CPolynomial F) (width b : ℕ) : (gsRelationColumn mulCtx modCtx R modulus width b).size = width

Size of the GS relation column.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationColumn_getD_of_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R modulus : CPolynomial F) {width b j : ℕ} (hj : j < b) : (gsRelationColumn mulCtx modCtx R modulus width b).getD j 0 = 0

Entries of the GS relation column below the diagonal vanish.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationColumn_getD_congr {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) {R modulus : CPolynomial F} (hM : modulus.toPoly.Monic) {width b j : ℕ} (hbj : b ≤ j) (hj : j < width) : modulus.toPoly ∣ ((gsRelationColumn mulCtx modCtx R modulus width b).getD j 0).toPoly - Polynomial.C ↑(j.choose b) * R.toPoly ^ (j - b)

Entries of the GS relation column are congruent to the binomial powers.

The GS relation matrix and the modular row predicate

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsModuli_getD_one {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (G : CPolynomial F) {b s : ℕ} (hb : b < s) : (gsModuli mulCtx G s).getD b 1 = G ^ (s - b)

The b-th GS modulus is G^(s-b), with default value 1.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationMatrixWithModuli_entry {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R : CPolynomial F) (moduli : Array (CPolynomial F)) (params : GSInterpParams) {k b : ℕ} (hk : k < interpolationWidth params) (hb : b < params.multiplicity) : PolynomialMatrix.rowGet (Array.getD (gsRelationMatrixWithModuli mulCtx modCtx R moduli params) k #[]) b = (gsRelationColumn mulCtx modCtx R (moduli.getD b 1) (interpolationWidth params) b).getD k 0

Entry access for the GS relation matrix.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationMatrixWithModuli_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R : CPolynomial F) (moduli : Array (CPolynomial F)) (params : GSInterpParams) : Array.size (gsRelationMatrixWithModuli mulCtx modCtx R moduli params) = interpolationWidth params

The GS relation matrix has one row per interpolation coefficient.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.gsRelationMatrixWithModuli_matrixWidth {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) (R : CPolynomial F) (moduli : Array (CPolynomial F)) (params : GSInterpParams) : (gsRelationMatrixWithModuli mulCtx modCtx R moduli params).MatrixWidth = params.multiplicity

The GS relation matrix has one column per multiplicity level.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.hasseDeriv_toPoly_ofCoeffRow_eval {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (row : PolynomialRow F) (R : Polynomial F) (b : ℕ) : Polynomial.eval R ((Polynomial.hasseDeriv b) (CBivariate.ofCoeffRow row).toPoly) = ∑ k ∈ Finset.range (Array.size row), Polynomial.C ↑(k.choose b) * (Array.getD row k 0).toPoly * R ^ (k - b)

Sheared coefficients of a coefficient row: the outer Hasse derivative of ofCoeffRow row evaluated at R is the binomial-weighted power sum.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.rowMulMatrixWith_congr_of_agree {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) {row row' : PolynomialRow F} (M : PolynomialMatrix F) (hagree : ∀ k < Array.size M, PolynomialMatrix.rowGet row k = PolynomialMatrix.rowGet row' k) : PolynomialMatrix.rowMulMatrixWith mulCtx row M = PolynomialMatrix.rowMulMatrixWith mulCtx row' M

The row-by-matrix product only sees the first M.size row entries.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.rowSatisfiesModularBool_congr_of_agree {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) {row row' : PolynomialRow F} (M : PolynomialMatrix F) (moduli : Array (CPolynomial F)) (hagree : ∀ k < Array.size M, PolynomialMatrix.rowGet row k = PolynomialMatrix.rowGet row' k) : PolynomialMatrix.rowSatisfiesModularBool mulCtx modCtx row M moduli = PolynomialMatrix.rowSatisfiesModularBool mulCtx modCtx row' M moduli

The modular row predicate only sees the first M.size row entries.

theorem CompPoly.GuruswamiSudan.ApproximantBasis.rowSatisfiesModularBool_gsRelationMatrix_iff {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (mulCtx : CPolynomial.MulContext F) (modCtx : CPolynomial.ModContext F) {G : CPolynomial F} (hG : G.toPoly.Monic) (R : CPolynomial F) (params : GSInterpParams) {row : PolynomialRow F} (hwidth : Array.size row ≤ interpolationWidth params) : PolynomialMatrix.rowSatisfiesModularBool mulCtx modCtx row (gsRelationMatrixWithRG mulCtx modCtx R G params) (gsModuli mulCtx G params.multiplicity) = true ↔ ∀ b < params.multiplicity, G.toPoly ^ (params.multiplicity - b) ∣ Polynomial.eval R.toPoly ((Polynomial.hasseDeriv b) (CBivariate.ofCoeffRow row).toPoly)

The executable GS modular row predicate over the relation matrix and modulus array is exactly divisibility of every sheared coefficient (hasseDeriv b (ofCoeffRow row).toPoly).eval R by G^(s-b).