Diophantine functions and Matiyasevic's theorem

Hilbert's tenth problem asked whether there exists an algorithm which for a given integer polynomial determines whether this polynomial has integer solutions. It was answered in the negative in 1970, the final step being completed by Matiyasevic who showed that the power function is Diophantine.

Here a function is called Diophantine if its graph is Diophantine as a set. A subset S ⊆ ℕ ^ α in turn is called Diophantine if there exists an integer polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

Main definitions

• IsPoly: a predicate stating that a function is a multivariate integer polynomial.
• Poly: the type of multivariate integer polynomial functions.
• Dioph: a predicate stating that a set is Diophantine, i.e. a set S ⊆ ℕ^α is Diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.
• dioph_fn: a predicate on a function stating that it is Diophantine in the sense that its graph is Diophantine as a set.

Main statements

• pell_dioph states that solutions to Pell's equation form a Diophantine set.
• pow_dioph states that the power function is Diophantine, a version of Matiyasevic's theorem.

References

• [M. Carneiro, A Lean formalization of Matiyasevic's theorem][carneiro2018matiyasevic]
• [M. Davis, Hilbert's tenth problem is unsolvable][MR317916]

Tags

Matiyasevic's theorem, Hilbert's tenth problem

TODO

• Finish the solution of Hilbert's tenth problem.
• Connect Poly to MvPolynomial

Multivariate integer polynomials

Note that this duplicates MvPolynomial.

inductive IsPoly {α : Type u_1} : ((α → ℕ) → ℤ) → Prop

A predicate asserting that a function is a multivariate integer polynomial. (We are being a bit lazy here by allowing many representations for multiplication, rather than only allowing monomials and addition, but the definition is equivalent and this is easier to use.)

• proj: ∀ {α : Type u_1} (i : α), IsPoly fun (x : α → ℕ) => ↑(x i)
• const: ∀ {α : Type u_1} (n : ℤ), IsPoly fun (x : α → ℕ) => n
• sub: ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, IsPoly f → IsPoly g → IsPoly fun (x : α → ℕ) => f x - g x
• mul: ∀ {α : Type u_1} {f g : (α → ℕ) → ℤ}, IsPoly f → IsPoly g → IsPoly fun (x : α → ℕ) => f x * g x

theorem IsPoly.neg {α : Type u_1} {f : (α → ℕ) → ℤ} : IsPoly f → IsPoly (-f)

theorem IsPoly.add {α : Type u_1} {f : (α → ℕ) → ℤ} {g : (α → ℕ) → ℤ} (hf : IsPoly f) (hg : IsPoly g) : IsPoly (f + g)

def Poly (α : Type u) : Type (max 0 u)

The type of multivariate integer polynomials

Equations

• Poly α = { f : (α → ℕ) → ℤ // IsPoly f }

instance Poly.instFunLike {α : Type u_1} : FunLike (Poly α) (α → ℕ) ℤ

Equations

• Poly.instFunLike = { coe := Subtype.val, coe_injective' := ⋯ }

theorem Poly.isPoly {α : Type u_1} (f : Poly α) : IsPoly ⇑f

The underlying function of a Poly is a polynomial

theorem Poly.ext {α : Type u_1} {f : Poly α} {g : Poly α} : (∀ (x : α → ℕ), f x = g x) → f = g

Extensionality for Poly α

def Poly.proj {α : Type u_1} (i : α) : Poly α

The ith projection function, x_i.

Equations

• Poly.proj i = ⟨fun (x : α → ℕ) => ↑(x i), ⋯⟩

@[simp]

theorem Poly.proj_apply {α : Type u_1} (i : α) (x : α → ℕ) : (Poly.proj i) x = ↑(x i)

def Poly.const {α : Type u_1} (n : ℤ) : Poly α

The constant function with value n : ℤ.

Equations

• Poly.const n = ⟨fun (x : α → ℕ) => n, ⋯⟩

@[simp]

theorem Poly.const_apply {α : Type u_1} (n : ℤ) (x : α → ℕ) : (Poly.const n) x = n

instance Poly.instZero {α : Type u_1} : Zero (Poly α)

Equations

• Poly.instZero = { zero := Poly.const 0 }

instance Poly.instOne {α : Type u_1} : One (Poly α)

Equations

• Poly.instOne = { one := Poly.const 1 }

instance Poly.instNeg {α : Type u_1} : Neg (Poly α)

Equations

• Poly.instNeg = { neg := fun (f : Poly α) => ⟨-⇑f, ⋯⟩ }

instance Poly.instAdd {α : Type u_1} : Add (Poly α)

Equations

• Poly.instAdd = { add := fun (f g : Poly α) => ⟨⇑f + ⇑g, ⋯⟩ }

instance Poly.instSub {α : Type u_1} : Sub (Poly α)

Equations

• Poly.instSub = { sub := fun (f g : Poly α) => ⟨⇑f - ⇑g, ⋯⟩ }

instance Poly.instMul {α : Type u_1} : Mul (Poly α)

Equations

• Poly.instMul = { mul := fun (f g : Poly α) => ⟨⇑f * ⇑g, ⋯⟩ }

@[simp]

theorem Poly.coe_zero {α : Type u_1} : ⇑0 = ⇑(Poly.const 0)

@[simp]

theorem Poly.coe_one {α : Type u_1} : ⇑1 = ⇑(Poly.const 1)

@[simp]

theorem Poly.coe_neg {α : Type u_1} (f : Poly α) : ⇑(-f) = -⇑f

@[simp]

theorem Poly.coe_add {α : Type u_1} (f : Poly α) (g : Poly α) : ⇑(f + g) = ⇑f + ⇑g

@[simp]

theorem Poly.coe_sub {α : Type u_1} (f : Poly α) (g : Poly α) : ⇑(f - g) = ⇑f - ⇑g

@[simp]

theorem Poly.coe_mul {α : Type u_1} (f : Poly α) (g : Poly α) : ⇑(f * g) = ⇑f * ⇑g

@[simp]

theorem Poly.zero_apply {α : Type u_1} (x : α → ℕ) : 0 x = 0

@[simp]

theorem Poly.one_apply {α : Type u_1} (x : α → ℕ) : 1 x = 1

@[simp]

theorem Poly.neg_apply {α : Type u_1} (f : Poly α) (x : α → ℕ) : (-f) x = -f x

@[simp]

theorem Poly.add_apply {α : Type u_1} (f : Poly α) (g : Poly α) (x : α → ℕ) : (f + g) x = f x + g x

@[simp]

theorem Poly.sub_apply {α : Type u_1} (f : Poly α) (g : Poly α) (x : α → ℕ) : (f - g) x = f x - g x

@[simp]

theorem Poly.mul_apply {α : Type u_1} (f : Poly α) (g : Poly α) (x : α → ℕ) : (f * g) x = f x * g x

instance Poly.instInhabited (α : Type u_3) : Inhabited (Poly α)

Equations

• Poly.instInhabited α = { default := 0 }

instance Poly.instAddCommGroup {α : Type u_1} : AddCommGroup (Poly α)

Equations

• Poly.instAddCommGroup = AddCommGroup.mk ⋯

instance Poly.instAddGroupWithOne {α : Type u_1} : AddGroupWithOne (Poly α)

Equations

• Poly.instAddGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance Poly.instCommRing {α : Type u_1} : CommRing (Poly α)

Equations

• Poly.instCommRing = CommRing.mk ⋯

theorem Poly.induction {α : Type u_1} {C : Poly α → Prop} (H1 : ∀ (i : α), C (Poly.proj i)) (H2 : ∀ (n : ℤ), C (Poly.const n)) (H3 : ∀ (f g : Poly α), C f → C g → C (f - g)) (H4 : ∀ (f g : Poly α), C f → C g → C (f * g)) (f : Poly α) : C f

def Poly.sumsq {α : Type u_1} : List (Poly α) → Poly α

The sum of squares of a list of polynomials. This is relevant for Diophantine equations, because it means that a list of equations can be encoded as a single equation: x = 0 ∧ y = 0 ∧ z = 0 is equivalent to x^2 + y^2 + z^2 = 0.

Equations

• Poly.sumsq [] = 0
• Poly.sumsq (p :: ps) = p * p + Poly.sumsq ps

theorem Poly.sumsq_nonneg {α : Type u_1} (x : α → ℕ) (l : List (Poly α)) : 0 ≤ (Poly.sumsq l) x

theorem Poly.sumsq_eq_zero {α : Type u_1} (x : α → ℕ) (l : List (Poly α)) : (Poly.sumsq l) x = 0 ↔ List.Forall (fun (a : Poly α) => a x = 0) l

def Poly.map {α : Type u_3} {β : Type u_4} (f : α → β) (g : Poly α) : Poly β

Map the index set of variables, replacing x_i with x_(f i).

Equations

• Poly.map f g = ⟨fun (v : β → ℕ) => g (v ∘ f), ⋯⟩

@[simp]

theorem Poly.map_apply {α : Type u_3} {β : Type u_4} (f : α → β) (g : Poly α) (v : β → ℕ) : (Poly.map f g) v = g (v ∘ f)

Diophantine sets

def Dioph {α : Type u} (S : Set (α → ℕ)) : Prop

A set S ⊆ ℕ^α is Diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

Equations

• Dioph S = ∃ (β : Type ?u.24) (p : Poly (α ⊕ β)), ∀ (v : α → ℕ), S v ↔ ∃ (t : β → ℕ), p (Sum.elim v t) = 0

theorem Dioph.ext {α : Type u} {S : Set (α → ℕ)} {S' : Set (α → ℕ)} (d : Dioph S) (H : ∀ (v : α → ℕ), v ∈ S ↔ v ∈ S') : Dioph S'

theorem Dioph.of_no_dummies {α : Type u} (S : Set (α → ℕ)) (p : Poly α) (h : ∀ (v : α → ℕ), S v ↔ p v = 0) : Dioph S

theorem Dioph.inject_dummies_lem {α : Type u} {β : Type u} {γ : Type u} (f : β → γ) (g : γ → Option β) (inv : ∀ (x : β), g (f x) = some x) (p : Poly (α ⊕ β)) (v : α → ℕ) : (∃ (t : β → ℕ), p (Sum.elim v t) = 0) ↔ ∃ (t : γ → ℕ), (Poly.map (Sum.elim Sum.inl (Sum.inr ∘ f)) p) (Sum.elim v t) = 0

theorem Dioph.inject_dummies {α : Type u} {β : Type u} {γ : Type u} {S : Set (α → ℕ)} (f : β → γ) (g : γ → Option β) (inv : ∀ (x : β), g (f x) = some x) (p : Poly (α ⊕ β)) (h : ∀ (v : α → ℕ), S v ↔ ∃ (t : β → ℕ), p (Sum.elim v t) = 0) : ∃ (q : Poly (α ⊕ γ)), ∀ (v : α → ℕ), S v ↔ ∃ (t : γ → ℕ), q (Sum.elim v t) = 0

theorem Dioph.reindex_dioph {α : Type u} (β : Type u) {S : Set (α → ℕ)} (f : α → β) : Dioph S → Dioph {v : β → ℕ | v ∘ f ∈ S}

theorem Dioph.DiophList.forall {α : Type u} (l : List (Set (α → ℕ))) (d : List.Forall Dioph l) : Dioph {v : α → ℕ | List.Forall (fun (S : Set (α → ℕ)) => v ∈ S) l}

theorem Dioph.inter {α : Type u} {S : Set (α → ℕ)} {S' : Set (α → ℕ)} (d : Dioph S) (d' : Dioph S') : Dioph (S ∩ S')

theorem Dioph.union {α : Type u} {S : Set (α → ℕ)} {S' : Set (α → ℕ)} : Dioph S → Dioph S' → Dioph (S ∪ S')

def Dioph.DiophPFun {α : Type u} (f : (α → ℕ) →. ℕ) : Prop

A partial function is Diophantine if its graph is Diophantine.

Equations

• Dioph.DiophPFun f = Dioph {v : Option α → ℕ | f.graph (v ∘ some, v none)}

def Dioph.DiophFn {α : Type u} (f : (α → ℕ) → ℕ) : Prop

A function is Diophantine if its graph is Diophantine.

Equations

• Dioph.DiophFn f = Dioph {v : Option α → ℕ | f (v ∘ some) = v none}

theorem Dioph.reindex_diophFn {α : Type u} {β : Type u} {f : (α → ℕ) → ℕ} (g : α → β) (d : Dioph.DiophFn f) : Dioph.DiophFn fun (v : β → ℕ) => f (v ∘ g)

theorem Dioph.ex_dioph {α : Type u} {β : Type u} {S : Set (α ⊕ β → ℕ)} : Dioph S → Dioph {v : α → ℕ | ∃ (x : β → ℕ), Sum.elim v x ∈ S}

theorem Dioph.ex1_dioph {α : Type u} {S : Set (Option α → ℕ)} : Dioph S → Dioph {v : α → ℕ | ∃ (x : ℕ), Option.elim' x v ∈ S}

theorem Dioph.dom_dioph {α : Type u} {f : (α → ℕ) →. ℕ} (d : Dioph.DiophPFun f) : Dioph f.Dom

theorem Dioph.diophFn_iff_pFun {α : Type u} (f : (α → ℕ) → ℕ) : Dioph.DiophFn f = Dioph.DiophPFun ↑f

theorem Dioph.abs_poly_dioph {α : Type u} (p : Poly α) : Dioph.DiophFn fun (v : α → ℕ) => (p v).natAbs

theorem Dioph.proj_dioph {α : Type u} (i : α) : Dioph.DiophFn fun (v : α → ℕ) => v i

theorem Dioph.diophPFun_comp1 {α : Type u} {S : Set (Option α → ℕ)} (d : Dioph S) {f : (α → ℕ) →. ℕ} (df : Dioph.DiophPFun f) : Dioph {v : α → ℕ | ∃ (h : f.Dom v), Option.elim' (f.fn v h) v ∈ S}

theorem Dioph.diophFn_comp1 {α : Type u} {S : Set (Option α → ℕ)} (d : Dioph S) {f : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) : Dioph {v : α → ℕ | Option.elim' (f v) v ∈ S}

theorem Dioph.diophFn_vec_comp1 {n : ℕ} {S : Set (Vector3 ℕ n.succ)} (d : Dioph S) {f : Vector3 ℕ n → ℕ} (df : Dioph.DiophFn f) : Dioph {v : Vector3 ℕ n | Vector3.cons (f v) v ∈ S}

theorem Dioph.vec_ex1_dioph (n : ℕ) {S : Set (Vector3 ℕ n.succ)} (d : Dioph S) : Dioph {v : Fin2 n → ℕ | ∃ (x : ℕ), Vector3.cons x v ∈ S}

theorem Dioph.diophFn_vec {n : ℕ} (f : Vector3 ℕ n → ℕ) : Dioph.DiophFn f ↔ Dioph {v : Fin2 (n + 1) → ℕ | f (v ∘ Fin2.fs) = v Fin2.fz}

theorem Dioph.diophPFun_vec {n : ℕ} (f : Vector3 ℕ n →. ℕ) : Dioph.DiophPFun f ↔ Dioph {v : Fin2 (n + 1) → ℕ | f.graph (v ∘ Fin2.fs, v Fin2.fz)}

theorem Dioph.diophFn_compn {α : Type} {n : ℕ} {S : Set (α ⊕ Fin2 n → ℕ)} : Dioph S → ∀ {f : Vector3 ((α → ℕ) → ℕ) n}, VectorAllP Dioph.DiophFn f → Dioph {v : α → ℕ | (Sum.elim v fun (i : Fin2 n) => f i v) ∈ S}

theorem Dioph.dioph_comp {α : Type} {n : ℕ} {S : Set (Vector3 ℕ n)} (d : Dioph S) (f : Vector3 ((α → ℕ) → ℕ) n) (df : VectorAllP Dioph.DiophFn f) : Dioph {v : α → ℕ | (fun (i : Fin2 n) => f i v) ∈ S}

theorem Dioph.diophFn_comp {α : Type} {n : ℕ} {f : Vector3 ℕ n → ℕ} (df : Dioph.DiophFn f) (g : Vector3 ((α → ℕ) → ℕ) n) (dg : VectorAllP Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f fun (i : Fin2 n) => g i v

def Dioph.«term_D∧_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D∧_» = Lean.ParserDescr.trailingNode `Dioph.«term_D∧_» 35 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D∧ ") (Lean.ParserDescr.cat `term 0))

def Dioph.«term_D∨_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D∨_» = Lean.ParserDescr.trailingNode `Dioph.«term_D∨_» 35 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D∨ ") (Lean.ParserDescr.cat `term 0))

def Dioph.«termD∃» : Lean.ParserDescr

Equations

• Dioph.«termD∃» = Lean.ParserDescr.node `Dioph.«termD∃» 30 (Lean.ParserDescr.symbol "D∃")

def Dioph.«term&_» : Lean.ParserDescr

Equations

• Dioph.«term&_» = Lean.ParserDescr.node `Dioph.«term&_» 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 1023))

theorem Dioph.proj_dioph_of_nat {n : ℕ} (m : ℕ) [Fin2.IsLT m n] : Dioph.DiophFn fun (v : Vector3 ℕ n) => v (Fin2.ofNat' m)

def Dioph.«termD&_» : Lean.ParserDescr

Equations

• Dioph.«termD&_» = Lean.ParserDescr.node `Dioph.«termD&_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "D&") (Lean.ParserDescr.cat `term 100))

theorem Dioph.const_dioph {α : Type} (n : ℕ) : Dioph.DiophFn (Function.const (α → ℕ) n)

def Dioph.«termD._» : Lean.ParserDescr

Equations

• Dioph.«termD._» = Lean.ParserDescr.node `Dioph.«termD._» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "D.") (Lean.ParserDescr.cat `term 100))

theorem Dioph.dioph_comp2 {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {S : ℕ → ℕ → Prop} (d : Dioph fun (v : Vector3 ℕ 2) => S (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))) : Dioph fun (v : α → ℕ) => S (f v) (g v)

theorem Dioph.diophFn_comp2 {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {h : ℕ → ℕ → ℕ} (d : Dioph.DiophFn fun (v : Vector3 ℕ 2) => h (v (Fin2.ofNat' 0)) (v (Fin2.ofNat' 1))) : Dioph.DiophFn fun (v : α → ℕ) => h (f v) (g v)

theorem Dioph.eq_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph fun (v : α → ℕ) => f v = g v

def Dioph.«term_D=_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D=_» = Lean.ParserDescr.trailingNode `Dioph.«term_D=_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D= ") (Lean.ParserDescr.cat `term 51))

theorem Dioph.add_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f v + g v

def Dioph.«term_D+_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D+_» = Lean.ParserDescr.trailingNode `Dioph.«term_D+_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D+ ") (Lean.ParserDescr.cat `term 81))

theorem Dioph.mul_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f v * g v

def Dioph.«term_D*_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D*_» = Lean.ParserDescr.trailingNode `Dioph.«term_D*_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D* ") (Lean.ParserDescr.cat `term 91))

theorem Dioph.le_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph {v : α → ℕ | f v ≤ g v}

def Dioph.«term_D≤_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D≤_» = Lean.ParserDescr.trailingNode `Dioph.«term_D≤_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D≤ ") (Lean.ParserDescr.cat `term 51))

theorem Dioph.lt_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph {v : α → ℕ | f v < g v}

def Dioph.«term_D<_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D<_» = Lean.ParserDescr.trailingNode `Dioph.«term_D<_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D< ") (Lean.ParserDescr.cat `term 51))

theorem Dioph.ne_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph {v : α → ℕ | f v ≠ g v}

def Dioph.«term_D≠_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D≠_» = Lean.ParserDescr.trailingNode `Dioph.«term_D≠_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D≠ ") (Lean.ParserDescr.cat `term 51))

theorem Dioph.sub_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f v - g v

def Dioph.«term_D-_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D-_» = Lean.ParserDescr.trailingNode `Dioph.«term_D-_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D- ") (Lean.ParserDescr.cat `term 81))

theorem Dioph.dvd_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph fun (v : α → ℕ) => f v ∣ g v

def Dioph.«term_D∣_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D∣_» = Lean.ParserDescr.trailingNode `Dioph.«term_D∣_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D∣ ") (Lean.ParserDescr.cat `term 51))

theorem Dioph.mod_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f v % g v

def Dioph.«term_D%_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D%_» = Lean.ParserDescr.trailingNode `Dioph.«term_D%_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D% ") (Lean.ParserDescr.cat `term 81))

theorem Dioph.modEq_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) {h : (α → ℕ) → ℕ} (dh : Dioph.DiophFn h) : Dioph fun (v : α → ℕ) => f v ≡ g v [MOD h v]

def Dioph.«termD≡» : Lean.ParserDescr

Equations

• Dioph.«termD≡» = Lean.ParserDescr.node `Dioph.«termD≡» 1024 (Lean.ParserDescr.symbol " D≡ ")

theorem Dioph.div_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f v / g v

def Dioph.«term_D/_» : Lean.TrailingParserDescr

Equations

• Dioph.«term_D/_» = Lean.ParserDescr.trailingNode `Dioph.«term_D/_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " D/ ") (Lean.ParserDescr.cat `term 81))

theorem Dioph.pell_dioph : Dioph fun (v : Vector3 ℕ 4) => ∃ (h : 1 < v (Fin2.ofNat' 0)), Pell.xn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 2) ∧ Pell.yn h (v (Fin2.ofNat' 1)) = v (Fin2.ofNat' 3)

theorem Dioph.xn_dioph : Dioph.DiophPFun fun (v : Vector3 ℕ 2) => { Dom := 1 < v (Fin2.ofNat' 0), get := fun (h : 1 < v (Fin2.ofNat' 0)) => Pell.xn h (v (Fin2.ofNat' 1)) }

theorem Dioph.pow_dioph {α : Type} {f : (α → ℕ) → ℕ} {g : (α → ℕ) → ℕ} (df : Dioph.DiophFn f) (dg : Dioph.DiophFn g) : Dioph.DiophFn fun (v : α → ℕ) => f v ^ g v

A version of Matiyasevic's theorem