Upstream candidate: a nonzero multivariate polynomial has a non-vanishing point

Mathlib.Algebra.MvPolynomial.Funext proves MvPolynomial.funext: over an infinite integral domain, two multivariate polynomials that agree on every point are equal. Its immediate contrapositive — a nonzero MvPolynomial over an infinite integral domain has a point where its evaluation is nonzero — is the multivariate analogue of Polynomial.exists_eval_ne_zero_of_natDegree_lt_card but is not packaged in mathlib as a standalone lemma.

The combinatorial-rigidity project's genericity device (the blueprint's lem:genericity-device, after Katoh–Tanigawa 2011, §5.1) rests on MvPolynomial.exists_eval_ne_zero: the panel-hinge rigidity matrix R(G,p) has entries that are polynomials in the panel coordinates p, so a minor that is nonzero at one realization is a nonzero MvPolynomial, hence non-vanishing at a generic p; a generic point attains the largest rank. It feeds the matrix specialization lemmas in Mathlib/LinearAlgebra/Matrix/Rank.lean.

MvPolynomial.exists_mem_eval_ne_zero₂ is the fibre-wise form, the blueprint's lem:pencil-x0-fibre-intersection: two nonvanishing loci restricted to a submodule still meet, proved by moving along the line through their two witnesses and invoking Polynomial.funext on the univariate restriction. The generic-point argument for the set X₀ of the pencil's main component needs it, since the two witnesses exists_eval_ne_zero₂ would otherwise supply need not lie in the same fibre L(q).

Mirror path: Mathlib/Algebra/MvPolynomial/Funext.lean. Promotion to mathlib is a copy-paste into the upstream Funext file, directly below MvPolynomial.funext.

theorem MvPolynomial.exists_eval_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p : MvPolynomial σ R} (hp : p ≠ 0) : ∃ (x : σ → R), (eval x) p ≠ 0

A nonzero multivariate polynomial has a non-vanishing point. Over an infinite integral domain R, a nonzero p : MvPolynomial σ R evaluates to a nonzero value at some point x : σ → R. This is the contrapositive of MvPolynomial.funext (if p vanished everywhere it would agree with the zero polynomial at every point, hence equal 0).

theorem MvPolynomial.exists_eval_ne_zero_of_forall_ne_zero {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {ι : Type u_3} [Finite ι] (p : ι → MvPolynomial σ R) (hp : ∀ (i : ι), p i ≠ 0) : ∃ (x : σ → R), ∀ (i : ι), (eval x) (p i) ≠ 0

Simultaneous non-vanishing point for a finite family. Over an infinite integral domain R, if each of finitely many multivariate polynomials p i : MvPolynomial σ R is nonzero, there is a single point x : σ → R at which every p i evaluates to a nonzero value.

Proof: the product ∏ i, p i is nonzero because R is a domain, so exists_eval_ne_zero supplies a common non-root, and map_prod factors the evaluation of the product.

This picks a common non-root of finitely many nonzero polynomials: it turns the per-factor nonzero hypotheses directly into per-factor eval ≠ 0 facts at one point, replacing hand-written mul_ne_zero + map_mul + ring chains. The fixed-arity forms exists_eval_ne_zero₂/₃/₄ below are the wrappers the combinatorial-rigidity project's genericity arguments call.

theorem MvPolynomial.exists_eval_ne_zero₂ {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p₁ p₂ : MvPolynomial σ R} (h₁ : p₁ ≠ 0) (h₂ : p₂ ≠ 0) : ∃ (x : σ → R), (eval x) p₁ ≠ 0 ∧ (eval x) p₂ ≠ 0

Two-factor form of exists_eval_ne_zero_of_forall_ne_zero: a common non-root of two nonzero multivariate polynomials over an infinite integral domain.

theorem MvPolynomial.exists_eval_ne_zero₃ {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p₁ p₂ p₃ : MvPolynomial σ R} (h₁ : p₁ ≠ 0) (h₂ : p₂ ≠ 0) (h₃ : p₃ ≠ 0) : ∃ (x : σ → R), (eval x) p₁ ≠ 0 ∧ (eval x) p₂ ≠ 0 ∧ (eval x) p₃ ≠ 0

Three-factor form of exists_eval_ne_zero_of_forall_ne_zero.

theorem MvPolynomial.exists_eval_ne_zero₄ {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {p₁ p₂ p₃ p₄ : MvPolynomial σ R} (h₁ : p₁ ≠ 0) (h₂ : p₂ ≠ 0) (h₃ : p₃ ≠ 0) (h₄ : p₄ ≠ 0) : ∃ (x : σ → R), (eval x) p₁ ≠ 0 ∧ (eval x) p₂ ≠ 0 ∧ (eval x) p₃ ≠ 0 ∧ (eval x) p₄ ≠ 0

Four-factor form of exists_eval_ne_zero_of_forall_ne_zero.

theorem MvPolynomial.exists_mem_eval_ne_zero₂ {R : Type u_1} [CommRing R] [IsDomain R] [Infinite R] {σ : Type u_2} {L : Submodule R (σ → R)} {p₁ p₂ : MvPolynomial σ R} (h₁ : ∃ z ∈ L, (eval z) p₁ ≠ 0) (h₂ : ∃ z ∈ L, (eval z) p₂ ≠ 0) : ∃ z ∈ L, (eval z) p₁ ≠ 0 ∧ (eval z) p₂ ≠ 0

Two polynomials each nonvanishing somewhere on a submodule are jointly nonvanishing somewhere on it. Over an infinite integral domain R, let L be a submodule of σ → R and p₁, p₂ : MvPolynomial σ R two polynomials each nonvanishing at some point of L. Then some single point of L makes both nonvanishing.

This is the fibre-wise form of exists_eval_ne_zero₂: the two hypotheses' witnesses z₁, z₂ need not agree, so the common non-root cannot simply be read off exists_eval_ne_zero₂'s witness (which carries no membership in L). Instead, restrict both polynomials to the line t ↦ z₁ + t • (z₂ - z₁) through the two witnesses — a submodule is closed under it, so every point of the line lies in L — giving two univariate polynomials (via MvPolynomial.aeval of that affine-linear substitution) that are each nonzero (evaluating at t = 0, t = 1 recovers the two hypotheses). Their product is nonzero, so by Polynomial.funext it has a non-root, which is a common non-root of both restrictions.

The fibre L(q) of the pencil's X₀ argument (lem:pencil-x0-fibre-intersection) is such a submodule: the generic point of X₀ intersects the attaining heights with the nondegenerate ones inside one fibre, two open conditions that must be shown to meet inside L(q), not merely somewhere in the ambient space.