# Single-fold Diophantine representations and undecidability under an at-most-one-solution promise

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Single-fold Diophantine representations](../../preprints/Single-fold-Diophantine-representations-September-24-2026/paper.pdf)

## Scope

The single-fold Diophantine conjecture asks whether every recursively enumerable set has a polynomial representation with a unique auxiliary witness for each member. The formalization establishes this for every recursively enumerable subset of $\mathbb N^n$, $n\ge1$: an integer polynomial has exactly one complete natural-number witness tuple for members and none for nonmembers.

The consequence that solvability remains undecidable under an at-most-one-solution promise is not separately formalized.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Single-fold Diophantine representations | [SingleFold.lean](../ComparatorChallenges/SingleFold.lean) |