Short polynomial containment decidability

[tom111]

Formalization of the problem whether a Turing machine can decide if an ideal in a polynomial ring contains a short polynomial.

I've created this with a lot of LLM help: A bit of Aristotle in the beginning and then Claude code to walk me through all the steps and prepare the file.

I'm relatively new to lean. Any comments and suggestions are very welcome.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[mo271]

Thanks, that looks great!

I think the way ComputablePred is used here and the encoding makes sense. I will start a thread on zulip nonetheless, because I think this is the first time we have such decision problems in our repo.

I just made suggestion for a serious of API test statements (which will also be useful when proving stuff about them).

Edit: https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/decision.20problems.20and.20.60ComputablePred.60

[mo271]

Suggested change

	*Reference:* [No short polynomials vanish on bounded rank matrices](
	https://doi.org/10.1112/blms.12819)
	by *Jan Draisma, Thomas Kahle, Finn Wiersig*, Bull. Lond. Math. Soc. (2023)
	*Reference:* [Finding binomials in polynomial ideals](
	https://doi.org/10.1186/s40687-017-0106-0)
	by *Anders Jensen, Thomas Kahle, Lukas Katthän*, Res. Math. Sci. (2017)
	*Reference:* [Computing the binomial part of a polynomial ideal](
	https://doi.org/10.1016/j.jsc.2023.102298)
	by *Martin Kreuzer, Florian Walsh*, J. Symbolic Comput. (2024)
	*Reference:* [Computing sparse multiples of polynomials](
	https://doi.org/10.1007/s00453-012-9652-4)
	by *Mark Giesbrecht, Daniel S. Roche, Hrushikesh Tilak*, Algorithmica (2012)
	*Reference:* [What is the shortest polynomial divisible by (x-1)(y-1)(x²y-1)?](
	https://mathoverflow.net/questions/273132) — MathOverflow question by Thomas Kahle (2017).
	YCor's comment poses the decidability question: "A general question is whether it's decidable
	(given an oracle to compute in K), and also whether it's decidable for principal ideals."
	A polynomial is *$t$-short* if it is nonzero and has at most $t$ terms. Given generators
	of an ideal $I \subseteq \mathbb{Q}[x_1, x_2, \ldots]$, can one algorithmically decide
	whether $I$ contains a $t$-short polynomial?
	The problem is solved for $t \leq 2$: monomials ($t = 1$) can be detected via colon ideals,
	and binomials ($t = 2$) via the algorithm of Jensen–Kahle–Katthän (2017). For $t \geq 3$,
	the problem is open, even in the univariate case $\mathbb{Q}[x]$.
	*References:*
	- [No short polynomials vanish on bounded rank matrices](
	https://doi.org/10.1112/blms.12819)
	by *Jan Draisma, Thomas Kahle, Finn Wiersig*, Bull. Lond. Math. Soc. (2023)
	- [Finding binomials in polynomial ideals](
	https://doi.org/10.1186/s40687-017-0106-0)
	by *Anders Jensen, Thomas Kahle, Lukas Katthän*, Res. Math. Sci. (2017)
	- [Computing the binomial part of a polynomial ideal](
	https://doi.org/10.1016/j.jsc.2023.102298)
	by *Martin Kreuzer, Florian Walsh*, J. Symbolic Comput. (2024)
	- [Computing sparse multiples of polynomials](
	https://doi.org/10.1007/s00453-012-9652-4)
	by *Mark Giesbrecht, Daniel S. Roche, Hrushikesh Tilak*, Algorithmica (2012)
	- [What is the shortest polynomial divisible by (x-1)(y-1)(x²y-1)?](
	https://mathoverflow.net/questions/273132) — MathOverflow question by Thomas Kahle (2017).
	YCor's comment poses the decidability question: "A general question is whether it's decidable
	(given an oracle to compute in K), and also whether it's decidable for principal ideals."

Our references are usually just such a list. (I will update the AGENTS.md to make that more clear : #3518)

[mo271]

might it make sense to change the docstring to zero-based indexing here as well? It is that way in the lean code, if it is not totally unusual in the informal math, perhaps a good idea to homogenize. also below (for instance in binomial_decidability)

[mo271]

Suggested change

	/-- No nonzero polynomial has zero terms, so `HasShortPoly 0` is always false. -/
	@[category API, AMS 13]
	theorem not_hasShortPoly_zero (I : Ideal (MvPolynomial ℕ ℚ)) : ¬ HasShortPoly 0 I := by
	intro ⟨p, _, hp_ne, hp_card⟩
	exact hp_ne (MvPolynomial.support_eq_empty.mp (Finset.card_eq_zero.mp (Nat.le_zero.mp hp_card)))
	/-- The zero ideal contains no nonzero elements, so it has no short polynomials. -/
	@[category API, AMS 13]
	theorem not_hasShortPoly_bot (t : ℕ) : ¬ HasShortPoly t (⊥ : Ideal (MvPolynomial ℕ ℚ)) := by
	intro ⟨p, hp_mem, hp_ne, _⟩
	exact hp_ne (Ideal.mem_bot.mp hp_mem)
	/-- The whole ring contains the monomial $1$, which has one term. -/
	@[category API, AMS 13]
	theorem hasShortPoly_one_top : HasShortPoly 1 (⊤ : Ideal (MvPolynomial ℕ ℚ)) := by
	refine ⟨X 0, Submodule.mem_top, by simp, ?_⟩
	simp [MvPolynomial.support_X]

Perhaps let's add a few API tests?

[mo271]

Suggested change

	/-- The empty exponent vector gives the zero `Finsupp`, representing $x^0 = 1$. -/
	@[category API, AMS 13]
	theorem monomialOfList_nil : monomialOfList [] = 0 := by
	simp [monomialOfList]

[mo271]

Suggested change

	/-- The empty list represents the zero polynomial. -/
	@[category API, AMS 13]
	theorem polyOfRep_nil : polyOfRep [] = 0 := by
	simp [polyOfRep]

[mo271]

Suggested change

	/-- Empty generators produce the zero ideal. -/
	@[category API, AMS 13]
	theorem idealOfInput_nil : idealOfInput [] = ⊥ := by
	simp [idealOfInput]

[mo271]

Suggested change

	/-- The zero ideal has no $t$-short polynomial. -/
	@[category API, AMS 13]
	theorem not_decisionProblem_nil (t : ℕ) : ¬ decisionProblem t [] := by
	simp only [decisionProblem]
	rw [idealOfInput_nil]
	exact not_hasShortPoly_bot t

[mo271]

AlphaProof can prove this:

theorem fib_ideal_contains_binomial (n : ℕ) (hn : 1 ≤ n) :
    X 0 ^ n - X 1 ∈ fibIdeal n := by
  norm_num [fibIdeal, false]
  rw[Ideal.mem_span_pair]
  by_contra!
  replace hn:∃ A B : MvPolynomial (Fin 2) Rat, A*(.X (1)-n.fib*.X 0-(n-1).fib)+B*(.X 0^2-.X 0-1)=.X 0^n-.X (1):=?_
  · bound
  use-1
  refine n.sub_add_cancel hn▸(n-1).strongRec fun and x=>match and with|0=>⟨0,by ring⟩|1=>⟨1,by ring⟩ | S+2=>((x _) (by constructor)).elim fun and h=>((x S (by valid)).elim) ?_
  use fun A B=>⟨and*.X 0+(S+2).fib,Nat.fib_add_two▸.trans (by rw [Nat.cast_add]) (by linear_combination h*.X 0)⟩

Potentially clean up the proof and also add it here (or rewrite it from scratch). But also fine to leave as sorry: just a good sanity check that we cannot find a disprove here...