Documentation

ArkLib.Data.CodingTheory.ProximityGap

Definitions and Theorems about Proximity Gaps #

We define the proximity gap properties of linear codes over finite fields.

[BCIKS20] refers to the paper "Proximity Gaps for Reed-Solomon Codes" by Eli Ben-Sasson, Dan Carmon, Yuval Ishai, Swastik Kopparty, and Shubhangi Saraf.

Using {https://eprint.iacr.org/2020/654}, version 20210703:203025.

Main Definitions and Statements #

def ProximityGap.proximityMeasure {n : Type} [Fintype n] [DecidableEq n] {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : Submodule F (nF)) [DecidablePred fun (x : nF) => x C] (u v : nF) (d : ) :

The proximity measure of two vectors u and v from a code C at distance d is the number of vectors at distance at most d from the linear combination of u and v with coefficients r in F.

Equations
    Instances For
      def ProximityGap.proximityGap {n : Type} [Fintype n] [DecidableEq n] {F : Type} [Field F] [Fintype F] [DecidableEq F] (C : Submodule F (nF)) [DecidablePred fun (x : nF) => x C] (d bound : ) :

      A code C exhibits proximity gap at distance d and cardinality bound bound if for every pair of vectors u and v, whenever the proximity measure for C u v d is greater than bound, then the distance of [u | v] from the interleaved code C ^⊗ 2 is at most d.

      Equations
        Instances For
          def ProximityGap.correlatedAgreement {n : Type} [Fintype n] {F : Type} (C : Set (nF)) (δ : NNReal) {k : } (W : Fin knF) :

          A code C exhibits δ-correlated agreement with respect to a tuple of vectors W_1, ..., W_k if there exists a set S of coordinates such that the size of S is at least (1 - δ) * |n|, and there exists a tuple of codewords v_1, ..., v_k such that v_i agrees with W_i on S for all i.

          Equations
            Instances For
              noncomputable def ProximityGap.δ_ε_proximityGap {ι : Type} [Fintype ι] [Nonempty ι] {α : Type} [DecidableEq α] [Nonempty α] (P : Finset (ια)) (C : Set (Finset (ια))) (δ ε : NNReal) :

              Definition 1.1 in [BCIKS20].

              Let P be a set P and C a collection of sets. We say that C displays a (δ, ε)-proximity gap with respect to P and the relative Hamming distance measure if for every S ∈ C exactly one of the following holds:

              1. The probability that a randomly sampled element s from S is δ-close to P is 1.
              2. The probability that a randomly sampled element s from S is δ-close to P is at most ε.

              We call δ the proximity parameter and ε the error parameter.

              Equations
                Instances For
                  noncomputable def ProximityGap.errorBound {ι : Type} [Fintype ι] {F : Type} [Field F] [Fintype F] (δ : NNReal) (deg : ) (domain : ι F) :

                  The error bound ε in the pair of proximity and error parameters (δ,ε) for Reed-Solomon codes defined up to the Johnson bound. More precisely, let ρ be the rate of the Reed-Solomon code. Then for δ ∈ (0, 1 - √ρ), we define the relevant error parameter ε for the unique decoding bound, i.e. δ ∈ (0, (1-ρ)/2] and Johnson bound, i.e. δ ∈ ((1-ρ)/2 , 1 - √ρ). Otherwise, we set ε = 0.

                  Equations
                    Instances For
                      theorem ProximityGap.proximity_gap_RSCodes {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {k t : } [NeZero k] [NeZero t] {deg : } {domain : ι F} (C : Fin tFin kιF) {δ : NNReal} ( : δ 1 - ReedSolomonCode.sqrtRate deg domain) :

                      Theorem 1.2 (Proximity Gaps for Reed-Solomon codes) in [BCIKS20].

                      Let C be a collection of affine spaces. Then C displays a (δ, ε)-proximity gap with respect to a Reed-Solomon code, where (δ,ε) are the proximity and error parameters defined up to the Johnson bound.

                      theorem ProximityGap.correlatedAgreement_lines {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {u : Fin 2ιF} {deg : } {domain : ι F} {δ : NNReal} ( : δ 1 - ReedSolomonCode.sqrtRate deg domain) (hproximity : (do let zPMF.uniformOfFintype F pure (δᵣ(u 0 + z u 1, (ReedSolomon.code domain deg)) δ)) True > (errorBound δ deg domain)) :
                      correlatedAgreement (↑(ReedSolomon.code domain deg)) δ u

                      Theorem 1.4 (Main Theorem — Correlated agreement over lines) in [BCIKS20].

                      Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and two words u₀ and u₁, such that the probability that a random affine line passing through u₀ and u₁ is δ-close to Reed-Solomon code is at most ε. Then, the words u₀ and u₁ have correlated agreement.

                      theorem ProximityGap.correlatedAgreement_affine_curves {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] [DecidableEq ι] {k : } {u : Fin kιF} {deg : } {domain : ι F} {δ : NNReal} ( : δ 1 - ReedSolomonCode.sqrtRate deg domain) (hproximity : (do let yPMF.uniformOfFintype { x : ιF // x Curve.parametrisedCurveFinite u } pure (δᵣ(y, (ReedSolomon.code domain deg)) δ)) True > k * (errorBound δ deg domain)) :
                      correlatedAgreement (↑(ReedSolomon.code domain deg)) δ u

                      Theorem 1.5 (Correlated agreement for low-degree parameterised curves) in [BCIKS20].

                      Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and a curve passing through words u₀, ..., uκ, such that the probability that a random point on the curve is δ-close to the Reed-Solomon code is at most ε. Then, the words u₀, ..., uκ have correlated agreement.

                      theorem ProximityGap.correlatedAgreement_affine_spaces {ι : Type} [Fintype ι] [Nonempty ι] {F : Type} [Field F] [Fintype F] [DecidableEq F] {k : } [NeZero k] {u : Fin (k + 1)ιF} {deg : } {domain : ι F} {δ : NNReal} ( : δ 1 - ReedSolomonCode.sqrtRate deg domain) (hproximity : (do let yPMF.uniformOfFintype ↥(u 0 +ᵥ affineSpan F (Finset.image (Fin.tail u) Finset.univ)) pure (δᵣ(y, (ReedSolomon.code domain deg)) δ)) True > (errorBound δ deg domain)) :
                      correlatedAgreement (↑(ReedSolomon.code domain deg)) δ u

                      Theorem 1.6 (Correlated agreement over affine spaces) in [BCIKS20].

                      Take a Reed-Solomon code of length ι and degree deg, a proximity-error parameter pair (δ, ε) and an affine space with origin u₀ and affine generting set u₁, ..., uκ such that the probability a random point in the affine space is δ-close to the Reed-Solomon code is at most ε. Then the words u₀, ..., uκ have correlated agreement.

                      Note that we have k+2 vectors to form the affine space. This an intricacy needed us to be able to isolate the affine origin from the affine span and to form a generating set of the correct size. The reason for taking an extra vector is that after isolating the affine origin, the affine span is formed as the span of the difference of the rest of the vector set.

                      noncomputable def ProximityGap.Trivariate.eval_on_Z₀ {F : Type} [Field F] (p : RatFunc F) (z : F) :
                      F
                      Equations
                        Instances For

                          Pretty printer defined by notation3 command.

                          Equations
                            Instances For

                              Pretty printer defined by notation3 command.

                              Equations
                                Instances For

                                  Pretty printer defined by notation3 command.

                                  Equations
                                    Instances For

                                      Pretty printer defined by notation3 command.

                                      Equations
                                        Instances For
                                          Equations
                                            Instances For
                                              noncomputable def ProximityGap.D_X (rho : ) (n m : ) :

                                              The degree bound (a.k.a. D_X) for instantiation of Guruswami-Sudan in lemma 5.3 of the Proximity Gap paper. D_X(m) = (m + 1/2)√rhon.

                                              Equations
                                                Instances For
                                                  noncomputable def ProximityGap.proximity_gap_degree_bound (rho : ) (m n : ) :
                                                  Equations
                                                    Instances For
                                                      noncomputable def ProximityGap.proximity_gap_johnson (rho : ) (m : ) :

                                                      The ball radius from lemma 5.3 of the Proximity Gap paper, which follows from the Johnson bound. δ₀(rho, m) = 1 - √rho - √rho/2m.

                                                      Equations
                                                        Instances For
                                                          theorem ProximityGap.guruswami_sudan_for_proximity_gap_existence {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n k m : } {ωs : Fin n F} {f : Fin nF} :
                                                          ∃ (Q : F[Z][X]), GuruswamiSudan.Condition (k + 1) m (proximity_gap_degree_bound ((k + 1) / n) m n) ωs f Q

                                                          The first part of lemma 5.3 from the Proximity gap paper. Given the D_X (proximity_gap_degree_bound) and δ₀ (proximity_gap_johnson), a solution to Guruswami-Sudan system exists.

                                                          theorem ProximityGap.guruswami_sudan_for_proximity_gap_property {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n k m : } {ωs : Fin n F} {w : Fin nF} {Q : F[Z][X]} (cond : GuruswamiSudan.Condition (k + 1) m (proximity_gap_degree_bound ((k + 1) / n) m n) ωs w Q) {p : (ReedSolomon.code ωs n)} (h : δᵣ(w, p) proximity_gap_johnson ((k + 1) / n) m) :

                                                          The second part of lemma 5.3 from the Proximity gap paper. For any solution Q of the Guruswami-Sudan system, and for any polynomial P ∈ RS[n, k, rho] such that δᵣ(w, P) ≤ δ₀(rho, m), we have that Y - P(X) divides Q(X, Y) in the polynomial ring F[X][Y]. Note that in F[X][Y], the term X actually refers to the outer variable, Y.

                                                          def ProximityGap.D_Y {F : Type} [Field F] (Q : F[Z][X][Y]) :

                                                          Following the Proximity Gap paper this the Y-degree of a trivariate polynomial Q.

                                                          Equations
                                                            Instances For
                                                              def ProximityGap.D_YZ {F : Type} [Field F] (Q : F[Z][X][Y]) :

                                                              The YZ-degree of a trivariate polynomial.

                                                              Equations
                                                                Instances For
                                                                  structure ProximityGap.ModifiedGuruswami {F : Type} [Field F] [DecidableEq F] (m n k : ) (ωs : Fin n F) (Q : F[Z][X][Y]) (u₀ u₁ : Fin nF) :

                                                                  The Guruswami-Sudan condition as it is stated in the proximity gap paper.

                                                                  Instances For
                                                                    theorem ProximityGap.modified_guruswami_has_a_solution {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {m n k : } {ωs : Fin n F} {u₀ u₁ : Fin nF} :
                                                                    ∃ (Q : F[Z][X][Y]), ModifiedGuruswami m n k ωs Q u₀ u₁

                                                                    The claim 5.4 from the proximity gap paper. It essentially claims that there exists a soultion to the Guruswami-Sudan constraints above.

                                                                    noncomputable instance ProximityGap.instFintypeElemOfFinite_arkLib {α : Type} (s : Set α) [inst : Finite s] :
                                                                    Fintype s
                                                                    Equations
                                                                      noncomputable def ProximityGap.coeffs_of_close_proximity {F : Type} [Field F] [DecidableEq F] {n : } (k : ) [Finite F] (ωs : Fin n F) (δ : ) (u₀ u₁ : Fin nF) :

                                                                      The set S (equation 5.2 of the proximity gap paper).

                                                                      Equations
                                                                        Instances For
                                                                          theorem ProximityGap.exists_Pz_of_coeffs_of_close_proximity {F : Type} [Field F] [DecidableEq F] {n : } {δ : } {u₀ u₁ : Fin nF} {ωs : Fin n F} [Finite F] {k : } {z : F} (hS : z coeffs_of_close_proximity k ωs δ u₀ u₁) :
                                                                          ∃ (Pz : Polynomial F), Pz.natDegree k δᵣ(u₀ + z u₁, (fun (a : F) => Polynomial.eval a Pz) ωs) δ

                                                                          There exists a δ-close polynomial P_z for each z from the set S.

                                                                          noncomputable def ProximityGap.Pz {F : Type} [Field F] [DecidableEq F] {n : } {δ : } {u₀ u₁ : Fin nF} {ωs : Fin n F} [Finite F] {k : } {z : F} (hS : z coeffs_of_close_proximity k ωs δ u₀ u₁) :

                                                                          The δ-close polynomial Pz for each z from the set S (coeffs_of_close_proximity).

                                                                          Equations
                                                                            Instances For
                                                                              theorem ProximityGap.exists_a_set_and_a_matching_polynomial {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                              ∃ (S' : Finset F) (h_sub : S' coeffs_of_close_proximity k ωs δ u₀ u₁) (P : F[Z][X]), S'.card > (coeffs_of_close_proximity k ωs δ u₀ u₁).card / (2 * D_Y Q) ∀ (z : { x : F // x S' }), Pz = Polynomial.map (Polynomial.evalRingHom z) P P.natDegree k Polynomial.Bivariate.degreeX P 1

                                                                              Proposition 5.5 from the proximity gap paper. There exists a subset S' of the set S and a bivariate polynomial P(X, Z) that matches Pz on that set.

                                                                              noncomputable def ProximityGap.matching_set {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {Q : F[Z][X][Y]} [Finite F] (ωs : Fin n F) (δ : ) (u₀ u₁ : Fin nF) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

                                                                              The subset S' extracted from the proprosition 5.5.

                                                                              Equations
                                                                                Instances For
                                                                                  theorem ProximityGap.matching_set_is_a_sub_of_coeffs_of_close_proximity {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                  matching_set k ωs δ u₀ u₁ h_gs coeffs_of_close_proximity k ωs δ u₀ u₁

                                                                                  S' is indeed a subset of S

                                                                                  theorem ProximityGap.irreducible_factorization_of_gs_solution {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] {k : } (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                  ∃ (C : F[Z][X]) (R : List F[Z][X][Y]) (f : List ) (e : List ), R.length = f.length f.length = e.length eᵢe, 1 eᵢ RᵢR, Rᵢ.Separable RᵢR, Irreducible Rᵢ Q = Polynomial.C C * xR.toFinset ×ˢ f.toFinset ×ˢ e.toFinset, match x with | (Rᵢ, fᵢ, eᵢ) => Rᵢ.comp (Y ^ fᵢ) ^ eᵢ

                                                                                  The equation 5.12 from the proximity gap paper.

                                                                                  theorem ProximityGap.discr_of_irred_components_nonzero {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                  ∃ (x₀ : F), R.choose, Polynomial.Bivariate.evalX x₀ (Polynomial.Bivariate.discr_y R) 0

                                                                                  Claim 5.6 of the proximity gap paper.

                                                                                  theorem ProximityGap.exists_factors_with_large_common_root_set {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (δ : ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

                                                                                  Claim 5.7 of the proximity gap paper.

                                                                                  noncomputable def ProximityGap.R {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (δ : ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

                                                                                  Claim 5.7 establishes existens of a polynomial R. This is the extraction of this polynomial.

                                                                                  Equations
                                                                                    Instances For
                                                                                      noncomputable def ProximityGap.H {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (δ : ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

                                                                                      Claim 5.7 establishes existens of a polynomial H. This is the extraction of this polynomial.

                                                                                      Equations
                                                                                        Instances For
                                                                                          theorem ProximityGap.irreducible_H {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                          Irreducible (H k δ x₀ h_gs)

                                                                                          An important property of the polynomial H extracted from claim 5.7 is that it is irreducible.

                                                                                          theorem ProximityGap.approximate_solution_is_exact_solution_coeffs {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) (t : ) :
                                                                                          t kAppendixA.ClaimA2.α' x₀ (R k δ x₀ h_gs) t = 0

                                                                                          The claim 5.8 from the proximity gap paper. States that the approximate solution is actually a solution. This version of the claim is stated in terms of coefficients.

                                                                                          theorem ProximityGap.approximate_solution_is_exact_solution_coeffs' {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                          AppendixA.ClaimA2.γ' x₀ (R k δ x₀ h_gs) = PowerSeries.mk fun (t : ) => if t k then 0 else (PowerSeries.coeff (AppendixA.𝕃 (H k δ x₀ h_gs)) t) (AppendixA.ClaimA2.γ' x₀ (R k δ x₀ h_gs) )

                                                                                          The claim 5.8 from the proximity gap paper. States that the approximate solution is actually a solution. This version is in terms of polynomials.

                                                                                          theorem ProximityGap.solution_gamma_is_linear_in_Z {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                          ∃ (v₀ : Polynomial F) (v₁ : Polynomial F), AppendixA.ClaimA2.γ' x₀ (R k δ x₀ h_gs) = AppendixA.polyToPowerSeries𝕃 (H k δ x₀ h_gs) (Polynomial.map Polynomial.C v₀ + X * Polynomial.map Polynomial.C v₁)

                                                                                          Claim 5.9 from the proximity gap paper. States that the solution γ is linear in the variable Z.

                                                                                          noncomputable def ProximityGap.P {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (δ : ) (x₀ : F) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :

                                                                                          The linear represenation of the solution γ extracted from the claim 5.9.

                                                                                          Equations
                                                                                            Instances For
                                                                                              theorem ProximityGap.gamma_eq_P {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) :
                                                                                              AppendixA.ClaimA2.γ' x₀ (R k δ x₀ h_gs) = AppendixA.polyToPowerSeries𝕃 (H k δ x₀ h_gs) (P k δ x₀ h_gs)

                                                                                              The extracted P from claim 5.9 equals γ.

                                                                                              noncomputable def ProximityGap.matching_set_at_x {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} {ωs : Fin n F} [Finite F] (δ : ) (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) (x : Fin n) :

                                                                                              The set S'_x from the proximity gap paper (just before claim 5.10). The set of all z∈S' such that w(x,z) matches P_z(x).

                                                                                              Equations
                                                                                                Instances For
                                                                                                  theorem ProximityGap.solution_gamma_matches_word_if_subset_large {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} [Finite F] {ωs : Fin n F} (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) {x : Fin n} {D : } (hD : D Polynomial.Bivariate.totalDegree (H k δ x₀ h_gs)) (hx : (matching_set_at_x k δ h_gs x).card > (2 * k + 1) * Polynomial.Bivariate.natDegreeY (H k δ x₀ h_gs) * Polynomial.Bivariate.natDegreeY (R k δ x₀ h_gs) * D) :
                                                                                                  Polynomial.eval (Polynomial.C (ωs x)) (P k δ x₀ h_gs) = Polynomial.C (u₀ x) + u₁ x Y

                                                                                                  Claim 5.10 of the proximity gap paper. Needed to prove the claim 5.9. This claim states that γ(x)=w(x,Z) if the cardinality |S'_x| is big enough.

                                                                                                  theorem ProximityGap.exists_points_with_large_matching_subset {F : Type} [Field F] [DecidableEq F] [DecidableEq (RatFunc F)] {n m : } (k : ) {δ : } {x₀ : F} {u₀ u₁ : Fin nF} {Q : F[Z][X][Y]} [Finite F] {ωs : Fin n F} (h_gs : ModifiedGuruswami m n k ωs Q u₀ u₁) {x : Fin n} {D : } (hD : D Polynomial.Bivariate.totalDegree (H k δ x₀ h_gs)) :
                                                                                                  ∃ (Dtop : Finset (Fin n)), Dtop.card = k + 1 xDtop, (matching_set_at_x k δ h_gs x).card > (2 * k + 1) * Polynomial.Bivariate.natDegreeY (H k δ x₀ h_gs) * Polynomial.Bivariate.natDegreeY (R k δ x₀ h_gs) * D

                                                                                                  Claim 5.11 from the proximity gap paper. There exists a set of points {x₀,...,x_{k+1}} such that the sets S_{x_j} satisfy the condition in the claim 5.10.