Restricting polynomials to an embedded set of variables

Setting all other variables to zero preserves every individual-degree bound. This lets circuit polynomials be written with natural-number input and gate indices, then restricted to the exact finite variable count used by the PCP.

noncomputable def MIPRE.LowDegree.extendZero {σ : Type u_1} {τ : Type u_2} {F : Type u_3} [CommRing F] {f : σ → τ} (hf : Function.Injective f) (x : σ → F) (j : τ) : F

Extend values by zero outside an embedded set of coordinates.

Equations

• MIPRE.LowDegree.extendZero hf x j = if h : j ∈ Set.range f then x ((Equiv.ofInjective f hf).symm ⟨j, h⟩) else 0

@[simp]

theorem MIPRE.LowDegree.extendZero_apply {σ : Type u_1} {τ : Type u_2} {F : Type u_3} [CommRing F] {f : σ → τ} (hf : Function.Injective f) (x : σ → F) (i : σ) : extendZero hf x (f i) = x i

theorem MIPRE.LowDegree.eval_killCompl {σ : Type u_1} {τ : Type u_2} {F : Type u_3} [CommRing F] {f : σ → τ} (hf : Function.Injective f) (p : MvPolynomial τ F) (x : σ → F) : (MvPolynomial.eval x) ((MvPolynomial.killCompl hf) p) = (MvPolynomial.eval (extendZero hf x)) p

Evaluation after restriction equals evaluation at the zero extension.

theorem MIPRE.LowDegree.eval_killCompl_eq {σ : Type u_1} {τ : Type u_2} {F : Type u_3} [CommRing F] {f : σ → τ} (hf : Function.Injective f) (p : MvPolynomial τ F) (x : σ → F) (y : τ → F) (hxy : ∀ (i : σ), y (f i) = x i) (hy : ∀ j ∉ Set.range f, y j = 0) : (MvPolynomial.eval x) ((MvPolynomial.killCompl hf) p) = (MvPolynomial.eval y) p

A useful form of restriction correctness: any zero extension agrees.

theorem MIPRE.LowDegree.degreeOf_killCompl_le {σ : Type u_1} {τ : Type u_2} {F : Type u_3} [CommRing F] {f : σ → τ} (hf : Function.Injective f) (p : MvPolynomial τ F) (i : σ) : MvPolynomial.degreeOf i ((MvPolynomial.killCompl hf) p) ≤ MvPolynomial.degreeOf (f i) p

Restriction cannot increase the degree of any retained coordinate.