Lee-O'Sullivan Correctness Common Helpers

Basic facts shared by Lee-O'Sullivan soundness and completeness proofs.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.distinctXCoordinatesBool_iff {F : Type u_1} [BEq F] [LawfulBEq F] {points : Array (F × F)} : distinctXCoordinatesBool points = true ↔ DistinctXCoordinates points

Executable distinct-x check agrees with the semantic predicate.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeCoefficientForm_eval_point {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) {points : Array (F × F)} (hdistinct : DistinctXCoordinates points) {point : F × F} (hpoint : point ∈ points.toList) : CPolynomial.eval point.1 (CPolynomial.interpolateCoefficientForm V E points) = point.2

The coefficient-form R used by Lee evaluates to the packed values at distinct nodes.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeVanishing_eval_point {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] (V : CPolynomial.VanishingPolynomialContext F) {points : Array (F × F)} {point : F × F} (hpoint : point ∈ points.toList) : CPolynomial.eval point.1 (V.vanishingPolynomial (Array.map (fun (p : F × F) => p.1) points)) = 0

The vanishing G used by Lee vanishes on every listed x.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisRows_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (points : Array (F × F)) (params : GSInterpParams) : Array.size (leeOSullivanBasisRows V E points params) = leeOSullivanWidth params

Lee basis rows have exactly ell + 1 rows.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisRowsWithRG_wellFormed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) : (leeOSullivanBasisRowsWithRG R G params).WellFormed

Lee basis rows built from fixed R and G are rectangular.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisRowsWithRG_width {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) : (leeOSullivanBasisRowsWithRG R G params).MatrixWidth = leeOSullivanWidth params

The executable Lee basis matrix has width ell + 1.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisRows_wellFormed {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (V : CPolynomial.VanishingPolynomialContext F) (E : CPolynomial.BatchEvalContext F) (points : Array (F × F)) (params : GSInterpParams) : (leeOSullivanBasisRows V E points params).WellFormed

Lee basis rows built from packed points are rectangular.

def CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomials {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) : Array (CBivariate F)

The Lee basis as bivariate polynomials, parallel to the executable row matrix.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomials_size {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) : (leeOSullivanBasisPolynomials R G params).size = leeOSullivanWidth params

The bivariate Lee basis has the same length as the row basis.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.leeOSullivanBasisPolynomials_getD_of_lt {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {i : ℕ} (hi : i < leeOSullivanWidth params) : (leeOSullivanBasisPolynomials R G params).getD i 0 = leeOSullivanBasisPolynomial R G params i

In-bounds reads from the bivariate Lee basis return the corresponding basis polynomial.

theorem CompPoly.GuruswamiSudan.LeeOSullivan.rowGet_leeOSullivanBasisRowsWithRG_getD {F : Type u_1} [Field F] [BEq F] [LawfulBEq F] [DecidableEq F] (R G : CPolynomial F) (params : GSInterpParams) {i j : ℕ} (hi : i < leeOSullivanWidth params) (hj : j < leeOSullivanWidth params) : PolynomialMatrix.rowGet (Array.getD (leeOSullivanBasisRowsWithRG R G params) i #[]) j = CPolynomial.coeff (leeOSullivanBasisPolynomial R G params i) j

In-bounds row entries of the executable Lee basis are the Y coefficients of the corresponding bivariate basis polynomial.