Wilkie's conjecture

InductiveFunction symbols of the language of exponentiation#✓fully proved

The function symbols of the language of exponentiation, sorted by arity: there is exactly one, the unary symbol \(\exp\), and there are none of any other arity.

inductive expFunc : ℕ → Type
  | exp : expFunc 1

Used by 2

Used byLanguage of exponentiation · Definable sets of the real exponential field

DefinitionLanguage of exponentiation#✓fully proved

The first-order language with a single function symbol, the unary symbol \(\exp\), and no relation symbols.

def Language.exp : Language where
  Functions := expFunc
  Relations _ := Empty
  deriving Language.IsAlgebraic

Uses 1 · Used by 2

Statement usesFunction symbols of the language of exponentiation

Used byLanguage of rings with exponentiation · Definable sets of the real exponential field

AbbreviationLanguage of rings with exponentiation#✓fully proved

The first-order language whose function symbols are those of the language of rings, namely the binary symbols \(+\) and \(\cdot\), the unary symbol \(-\) and the constants \(0\) and \(1\), together with the unary symbol \(\exp\) of the language of exponentiation; it has no relation symbols.

abbrev expRing := Language.ring.sum Language.exp

Uses 1 · Used by 1

Statement usesLanguage of exponentiation

Used byDefinable sets of the real exponential field

DefinitionSemialgebraic set#✓fully proved

A set \(X \subseteq \mathbb{R}^n\) is semialgebraic if it is definable, with parameters from \(\mathbb{R}\), in the real numbers viewed as a structure for the language of rings.

def IsSemialgebraic (X : Set ℝⁿ) : Prop :=
  Set.Definable Set.univ Language.ring X

Used by 1

Used byAlgebraic part of a set

DefinitionDefinable sets of the real exponential field#✓fully proved

A set \(X \subseteq \mathbb{R}^n\) is definable in \(\mathbb{R}_{\exp}\) if it is definable, with parameters from \(\mathbb{R}\), in the real numbers viewed as a structure for the language of rings with exponentiation, where the ring symbols have their usual meaning and \(\exp\) is interpreted as the real exponential function.

def IsRExpDefinable (X : Set ℝⁿ) : Prop :=
  Set.Definable Set.univ expRing X

Uses 3 · Used by 1

Statement usesLanguage of exponentiation · Function symbols of the language of exponentiation · Language of rings with exponentiation

Used byWilkie's conjecture for the real exponential field

DefinitionAlgebraic part of a set#✓fully proved

For a set \(X \subseteq \mathbb{R}^n\), the algebraic part \(X^{\mathrm{alg}}\) of \(X\) is the union of all connected, infinite semialgebraic sets \(Y\) with \(Y \subseteq X\).

The source takes the union of the connected, positive-dimensional semialgebraic subsets of \(X\); for connected semialgebraic sets, being infinite is equivalent to being positive-dimensional.

def algPart (X : Set ℝⁿ) : Set ℝⁿ :=
  sSup { Y : Set ℝⁿ | Y ⊆ X ∧ IsSemialgebraic Y ∧ Y.Infinite ∧ IsConnected Y }

Uses 1 · Used by 1

Statement usesSemialgebraic set

Used byTranscendental part of a set

DefinitionTranscendental part of a set#✓fully proved

For a set \(X \subseteq \mathbb{R}^n\), the transcendental part of \(X\) is \(X^{\mathrm{trans}} := X \setminus X^{\mathrm{alg}}\), where \(X^{\mathrm{alg}}\) is the algebraic part of \(X\).

def transPart (X : Set ℝⁿ) : Set ℝⁿ := X \ algPart X

Uses 1 · Used by 1

Statement usesAlgebraic part of a set

Used byWilkie's conjecture for the real exponential field

DefinitionHeight of a point#✓fully proved

For \(a = (a_1, \dots, a_n) \in \mathbb{R}^n\), the height \(H(a)\) is the maximum of the absolute multiplicative Weil heights of the coordinates \(a_1, \dots, a_n\). A coordinate that is not algebraic over \(\mathbb{Q}\) counts with height \(1\), and for \(n = 0\) the height is \(0\).

def height (a : ℝⁿ) : ℝ := ⨆ i, NumberField.absMulHeight₁ (a i)

Used by 1

Used byPoints of bounded degree and height

DefinitionPoints of bounded degree and height#✓fully proved

For a set \(X \subseteq \mathbb{R}^n\) and natural numbers \(g\) and \(H\), the set \(X(g, H)\) consists of the points \(x = (x_1, \dots, x_n) \in X\) whose coordinates are all algebraic over \(\mathbb{Q}\), such that the field \(\mathbb{Q}(x) = \mathbb{Q}(x_1, \dots, x_n)\) satisfies \([\mathbb{Q}(x) : \mathbb{Q}] \le g\) and the height \(H(x)\) of \(x\), the maximum of the absolute multiplicative Weil heights of \(x_1, \dots, x_n\) (taken to be \(0\) when \(n = 0\)), satisfies \(H(x) \le H\).

def degreeHeightLE (X : Set ℝⁿ) (g H : ℕ) : Set ℝⁿ :=
  { x ∈ X | (∀ i, IsAlgebraic ℚ (x i)) ∧
    Module.finrank ℚ (IntermediateField.adjoin ℚ (Set.range x)) ≤ g ∧ height x ≤ H }

Uses 1 · Used by 1

Statement usesHeight of a point

Used byWilkie's conjecture for the real exponential field

TheoremWilkie's conjecture for the real exponential field#●ready to prove

Let \(X \subseteq \mathbb{R}^n\) be definable in \(\mathbb{R}_{\exp}\). Then there is a polynomial \(f\) in two variables with real coefficients such that the following holds for all natural numbers \(g\) and \(H\). Let \(X^{\mathrm{trans}}(g, H)\) be the set of points \(x = (x_1, \dots, x_n)\) of the transcendental part \(X^{\mathrm{trans}}\) of \(X\) whose coordinates are all algebraic over \(\mathbb{Q}\), such that the field \(\mathbb{Q}(x) = \mathbb{Q}(x_1, \dots, x_n)\) satisfies \([\mathbb{Q}(x) : \mathbb{Q}] \le g\) and the height \(H(x)\) of \(x\), the maximum of the absolute multiplicative Weil heights of \(x_1, \dots, x_n\) (taken to be \(0\) when \(n = 0\)), satisfies \(H(x) \le H\). Then \(X^{\mathrm{trans}}(g, H)\) is finite and has at most \(f(g, \log H)\) elements, where \(\log 0\) is taken to be \(0\).

This is Corollary 1 of the source.

public theorem_wanted corollary_1 (X : Set ℝⁿ) (h : IsRExpDefinable X) :
    ∃ f : MvPolynomial (Fin 2) ℝ, ∀ (g H : ℕ),
      (degreeHeightLE (transPart X) g H).Finite ∧
        Nat.card (degreeHeightLE (transPart X) g H) ≤ f.eval ![(g : ℝ), Real.log H]

Sources

• G. Binyamini, D. Novikov, and B. Zak, Wilkie's conjecture for Pfaffian structures, Annals of Math, 199 (2) 2024. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_wilkies_conjecture of the lean-eval benchmark.

Uses 3

Statement usesDefinable sets of the real exponential field · Points of bounded degree and height · Transcendental part of a set

9 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.