Integer-coefficient obstruction

This file contains the paper's impossibility result for a single triple of integer-coefficient polynomials.

theorem LeanPool.PythagoreanPolynomialParametrization.no_int_poly_parametrization : ¬∃ (n : ℕ) (f : IntPoly n) (g : IntPoly n) (h : IntPoly n), IntPolyParametrizes f g h pythagoreanTriples

Frisch--Vaserstein's obstruction: no finite-variable triple of integer-coefficient polynomials parametrizes all Pythagorean triples.