Pell.Solution₁.x_ne_zero
theorem Pell.Solution₁.x_ne_zero : ∀ {d : ℤ}, 0 ≤ d → ∀ (a : Pell.Solution₁ d), a.x ≠ 0
The theorem `Pell.Solution₁.x_ne_zero` states that for any integer `d` that is greater than or equal to zero, and for any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, the x-value of the solution `a` is not equal to zero. This theorem ensures that the x-coordinate of a solution to the Pell equation is always non-zero, thus excluding trivial solutions where `x` is zero.
More concisely: For any non-negative integer `d` and solution `(x, y)` to the Pell equation `x^2 - d*y^2 = 1`, the x-coordinate `x` is non-zero.
|
Pell.existsUnique_pos_generator
theorem Pell.existsUnique_pos_generator :
∀ {d : ℤ},
0 < d → ¬IsSquare d → ∃! a₁, 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Pell.Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
The theorem `Pell.existsUnique_pos_generator` states that for any positive integer `d` that is not a perfect square, there exists a unique positive generator `a₁` for the group of solutions to the Pell equation `x^2 - d*y^2 = 1`. This generator `a₁` satisfies the conditions that `a₁.x` is greater than 1, `a₁.y` is positive, and for any solution `a` to the Pell equation, there exists an integer `n` such that `a` is either the `n`-th power of `a₁` or the `n`-th power of `-a₁`.
More concisely: For any positive integer `d` not being a perfect square, the Pell equation `x^2 - d*y^2 = 1` has a unique positive solution `a₁` such that `a₁.x > 1`, `a₁.y > 0`, and every solution `a` can be expressed as the `n`-th power of `a₁` or the `n`-th power of `-a₁` for some integer `n`.
|
Pell.IsFundamental.eq_pow_of_nonneg
theorem Pell.IsFundamental.eq_pow_of_nonneg :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 0 < a.x → 0 ≤ a.y → ∃ n, a = a₁ ^ n
This theorem states that for any given integer 'd' and a solution 'a₁' to the Pell equation `x^2 - d*y^2 = 1` (where 'a₁' is considered fundamental if `x > 1`, `y > 0`, and 'a₁'s `x` is the smallest possible among solutions with `x > 1`), any other solution 'a' to the same Pell equation with `x > 0` and `y ≥ 0` can be expressed as 'a₁' raised to some nonnegative integer power 'n'. Essentially, any nonnegative solution is a power with nonnegative exponent of a fundamental solution.
More concisely: Given a fundamental solution 'a₁' to the Pell equation `x^2 - d*y^2 = 1`, any other solution 'a' with `x > 0` and `y ≥ 0` can be expressed as 'a₁' raised to some nonnegative integer power.
|
Pell.Solution₁.prop_x
theorem Pell.Solution₁.prop_x : ∀ {d : ℤ} (a : Pell.Solution₁ d), a.x ^ 2 = 1 + d * a.y ^ 2
The theorem `Pell.Solution₁.prop_x` states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, the square of the `x`-component of the solution can be rewritten as `1 + d` times the square of the `y`-component. In other words, if `(x, y)` is a solution of the Pell equation, then we have `x^2 = 1 + d * y^2`.
More concisely: For any solution `(x, y)` of the Pell equation `x^2 - d*y^2 = 1` in Lean 4, it holds that `x^2 = 1 + d * y^2`.
|
Pell.Solution₁.eq_one_or_neg_one_iff_y_eq_zero
theorem Pell.Solution₁.eq_one_or_neg_one_iff_y_eq_zero : ∀ {d : ℤ} {a : Pell.Solution₁ d}, a = 1 ∨ a = -1 ↔ a.y = 0
This theorem states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, the solution `a` is either `1` or `-1` if and only if the `y` component of `a` is `0`. Here, `Pell.Solution₁ d` represents the type of solutions to the Pell equation, and `a` is an element of this type. The theorem links the values of the solution `a` to the `y` component of the solution.
More concisely: For any integer `d`, the solution `a` to the Pell equation `x^2 - d*y^2 = 1` in `Pell.Solution₁ d` is equal to `1` or `-1` if and only if the `y` component of `a` is equal to `0`.
|
Pell.Solution₁.prop
theorem Pell.Solution₁.prop : ∀ {d : ℤ} (a : Pell.Solution₁ d), a.x ^ 2 - d * a.y ^ 2 = 1
The theorem `Pell.Solution₁.prop` asserts that for any integer `d` and any solution `a` to the Pell equation in the set `Pell.Solution₁ d`, the square of the x-component of `a` minus `d` times the square of the y-component of `a`, equals 1. In mathematical terms, it states that for every solution to the Pell equation, \(x^2 - d*y^2 = 1\), where `d` is an integer.
More concisely: For any integer `d` and solution `a` in the set `Pell.Solution₁ d` of the Pell equation, `x^2 = d*y^2 + 1`, where `x` and `y` are the components of `a`.
|
Pell.pos_generator_iff_fundamental
theorem Pell.pos_generator_iff_fundamental :
∀ {d : ℤ} (a : Pell.Solution₁ d),
(1 < a.x ∧ 0 < a.y ∧ ∀ (b : Pell.Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n) ↔ Pell.IsFundamental a
The theorem `Pell.pos_generator_iff_fundamental` states that for any integer `d` and a solution `a` to the Pell equation `x^2 - d*y^2 = 1`, the solution `a` is a generator (up to sign) of the group of all solutions to the Pell equation if and only if it is a fundamental solution. In other words, if `a` has positive `x` and `y` components with `x > 1`, and for any other solution `b`, there exists an integer `n` such that `b` equals `a` raised to the power of `n` or `b` equals the negative of `a` raised to the power of `n`, then `a` is considered a fundamental solution. Conversely, every fundamental solution exhibits this property.
More concisely: A solution `a` to the Pell equation `x^2 - d*y^2 = 1` with positive `x` and `x > 1` is a generator (up to sign) if and only if it is a fundamental solution.
|
Pell.IsFundamental.zpow_eq_one_iff
theorem Pell.IsFundamental.zpow_eq_one_iff :
∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ∀ (n : ℤ), a ^ n = 1 ↔ n = 0
This theorem states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, if `a` is a fundamental solution (meaning that its `x` value is larger than 1, its `y` value is positive, and its `x` value is the smallest possible among all other solutions with `x` values greater than 1), then the `n`th power of `a` equals 1 if and only if `n` equals 0. In other words, a fundamental solution to the Pell equation raised to any power other than zero will never equal 1.
More concisely: A fundamental solution to the Pell equation `x^2 - d*y^2 = 1` never equals 1 for any power `n` different from zero.
|
Pell.IsFundamental.x_le_x
theorem Pell.IsFundamental.x_le_x :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d}, Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → a₁.x ≤ a.x := by
sorry
The theorem `Pell.IsFundamental.x_le_x` states that for any integer `d` and any fundamental solution `a₁` to the Pell equation `x^2 - d*y^2 = 1`, the `x`-coordinate of `a₁` is lower than or equal to the `x`-coordinate of any other solution `a` to the same equation such that `a.x > 1`. Thus, if a solution to the Pell equation is fundamental, its `x`-coordinate provides a lower bound for the `x`-coordinates of all other positive solutions.
More concisely: For any fundamental solution to the Pell equation $x^2 - d\ y^2 = 1$, its $x$-coordinate is the lowest among all positive solutions.
|
Pell.is_pell_solution_iff_mem_unitary
theorem Pell.is_pell_solution_iff_mem_unitary : ∀ {d : ℤ} {a : ℤ√d}, a.re ^ 2 - d * a.im ^ 2 = 1 ↔ a ∈ unitary (ℤ√d)
The theorem `Pell.is_pell_solution_iff_mem_unitary` states that for any integer `d` and any element `a` of the number system formed by taking the square root of `d` in the integers (`ℤ√d`), the condition that the real part of `a` squared minus `d` times the imaginary part of `a` squared equals 1 (i.e., `a.re ^ 2 - d * a.im ^ 2 = 1`) is equivalent to `a` being a member of the submonoid of unitary elements. A unitary element in this context is defined as an element `U` in a star-monoid `R` such that the star product of `U` and `U` equals 1 and the product of `U` and its star equals 1. This theorem suggests a connection between solutions to the Pell equation and unitary elements.
More concisely: For an integer `d` and an element `a` in the square root of `d` integers, `a` is a unitary element if and only if `a.re^2 - d * a.im^2 = 1`.
|
Pell.Solution₁.eq_zero_of_d_neg
theorem Pell.Solution₁.eq_zero_of_d_neg : ∀ {d : ℤ}, d < 0 → ∀ (a : Pell.Solution₁ d), a.x = 0 ∨ a.y = 0
The theorem `Pell.Solution₁.eq_zero_of_d_neg` states that for any negative integer `d`, in any solution to the Pell equation `x^2 - d*y^2 = 1` (represented as an element `a` of type `Pell.Solution₁ d`), either `x` (represented as `a.x`) or `y` (represented as `a.y`) must be equal to zero. In other words, if `d` is negative, then either `x` or `y` in the solution of the Pell equation must be zero.
More concisely: For any negative integer `d`, a solution `a` to the Pell equation `x^2 - d*y^2 = 1` in `Pell.Solution₁ d` has either `x = 0` or `y = 0`.
|
Pell.IsFundamental.zpow_y_lt_iff_lt
theorem Pell.IsFundamental.zpow_y_lt_iff_lt :
∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ∀ (m n : ℤ), (a ^ m).y < (a ^ n).y ↔ m < n
This theorem states that for any integer `d` and a fundamental solution `a` of the Pell equation `x^2 - d*y^2 = 1`, for any integers `m` and `n`, the `y` component of `a` raised to the `m` power is less than the `y` component of `a` raised to the `n` power if and only if `m` is less than `n`. This theorem is connecting a comparison between powers of a fundamental solution of the Pell equation to a comparison between the exponents themselves.
More concisely: For any fundamental solution `a` of the Pell equation `x^2 - d*y^2 = 1`, the `y` component raised to the power of `m` is less than the `y` component raised to the power of `n` if and only if `m` is less than `n`.
|
Pell.Solution₁.prop_y
theorem Pell.Solution₁.prop_y : ∀ {d : ℤ} (a : Pell.Solution₁ d), d * a.y ^ 2 = a.x ^ 2 - 1
This theorem provides an alternative form of the Pell equation `x^2 - d*y^2 = 1` that is convenient for rewriting expressions involving `d * y^2`. Specifically, for any integer `d` and any solution `a` to the Pell equation with that `d`, the product of `d` and the square of the `y`-component of the solution (`d * y^2`) equals the square of the `x`-component of the solution minus one (`x^2 - 1`).
More concisely: For any integer `d` and solution `(x, y)` to the Pell equation `x^2 - d*y^2 = 1`, we have `d * y^2 = x^2 - 1`.
|
Pell.IsFundamental.x_pos
theorem Pell.IsFundamental.x_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → 0 < a.x
The theorem `Pell.IsFundamental.x_pos` states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1` that is considered "fundamental" (meaning that its `x` value is larger than 1, its `y` value is positive, and its `x` is the smallest among solutions with `x` larger than 1), the `x` value of `a` is always positive.
More concisely: For any fundamental solution (x, y) to the Pell equation x^2 - d*y^2 = 1, the value of x is positive.
|
Pell.Solution₁.exists_nontrivial_of_not_isSquare
theorem Pell.Solution₁.exists_nontrivial_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ a, a ≠ 1 ∧ a ≠ -1 := by
sorry
This theorem states that for any positive integer `d` that does not satisfy the `IsSquare` property (i.e., `d` is not a perfect square), there exists a non-trivial solution to the Pell equation `x^2 - d*y^2 = 1`. A non-trivial solution here is defined as a solution `a` that is not equal to 1 or -1. Specifically, the theorem asserts that such a solution `a` always exists for any non-square positive integer `d`.
More concisely: For any non-square positive integer `d`, there exist non-trivial integers `x` and `y` such that `x^2 - d*y^2 = 1`.
|
Pell.IsFundamental.mul_inv_x_pos
theorem Pell.IsFundamental.mul_inv_x_pos :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → 0 < (a * a₁⁻¹).x
The theorem `Pell.IsFundamental.mul_inv_x_pos` asserts that for any integer `d` and any two solutions `a₁` and `a` to the Pell equation `x^2 - d*y^2 = 1`, if `a₁` is a fundamental solution (meaning `a₁.x > 1`, `a₁.y > 0` and `a₁.x` is the smallest possible among solutions with `x > 1`), and `a.x > 1` and `a.y > 0`, then the `x`-coordinate of the product of `a` and the inverse of `a₁` is greater than zero. In other words, multiplying a positive solution by the inverse of a fundamental solution retains the positivity of the `x`-coordinate.
More concisely: If `a₁` is a fundamental solution to the Pell equation `x^2 - d*y^2 = 1` and `a` is another solution with `x > 1` and `y > 0`, then `(a * inv(a₁)).x > 0`.
|
Pell.IsFundamental.subsingleton
theorem Pell.IsFundamental.subsingleton :
∀ {d : ℤ} {a b : Pell.Solution₁ d}, Pell.IsFundamental a → Pell.IsFundamental b → a = b
The theorem `Pell.IsFundamental.subsingleton` states that if there exists a fundamental solution to the Pell equation `x^2 - d*y^2 = 1`, then it is unique. Here, a fundamental solution is one where `x > 1`, `y > 0`, and among all the solutions with `x > 1`, `x` is the smallest possible. In other words, if there are two fundamental solutions `a` and `b` to the Pell equation for a given integer `d`, then `a` equals `b`.
More concisely: If `d` is an integer and `(x₁, y₁)` and `(x₂, y₂)` are fundamental solutions to the Pell equation `x^2 - d*y^2 = 1`, then `x₁ = x₂`.
|
Pell.Solution₁.x_mul_pos
theorem Pell.Solution₁.x_mul_pos : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, 0 < a.x → 0 < b.x → 0 < (a * b).x
The theorem `Pell.Solution₁.x_mul_pos` states that for any integer `d` and any two solutions `a` and `b` to the Pell equation `x^2 - d*y^2 = 1` (represented as elements of type `Pell.Solution₁ d`), if both solutions have positive `x` values, then the `x` value of their product (obtained by multiplying `a` and `b` as elements of the type `Pell.Solution₁ d`) is also positive. In other words, the set of solutions to the Pell equation with positive `x` values is closed under multiplication.
More concisely: If `a` and `b` are solutions to the Pell equation `x^2 - d*y^2 = 1` with positive `x` values (of type `Pell.Solution₁ d`), then the `x` value of their product `a * b` is also positive.
|
Pell.Solution₁.d_nonsquare_of_one_lt_x
theorem Pell.Solution₁.d_nonsquare_of_one_lt_x : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 1 < a.x → ¬IsSquare d
This theorem states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, if the `x` component of the solution `a` is greater than 1, then `d` cannot be a perfect square. Here, "perfect square" means that `d` is equal to `r*r` for some integer `r`.
More concisely: If an integer `d` has a solution `(x, y)` to the Pell equation `x^2 - d*y^2 = 1` with `x > 1`, then `d` is not a perfect square.
|
Pell.IsFundamental.y_le_y
theorem Pell.IsFundamental.y_le_y :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → a₁.y ≤ a.y
This theorem states that for any integer `d` and any fundamental solution `a₁` of the Pell equation `x^2 - d*y^2 = 1`, the `y`-coordinate of `a₁` is less than or equal to the `y`-coordinate of any other solution `a` with a positive `x`-coordinate greater than 1 and a positive `y`-coordinate. In other words, the `y`-coordinate of a fundamental solution provides a lower bound for the `y`-coordinates of all other solutions of the same equation that have positive `x` and `y`-coordinates.
More concisely: For any integer `d` and fundamental solution `a₁` of the Pell equation `x^2 - d*y^2 = 1`, the `y`-coordinate of `a₁` is the smallest positive `y`-coordinate of any solution `a` with `x > 1` and `y > 0` for that equation.
|
Pell.IsFundamental.y_strictMono
theorem Pell.IsFundamental.y_strictMono :
∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → StrictMono fun n => (a ^ n).y
The theorem `Pell.IsFundamental.y_strictMono` states that for any integer `d` and any fundamental solution `a` to the Pell equation `x^2 - d*y^2 = 1`, the function that maps an integer `n` to the `y`-coordinate of `a^n` is strictly increasing. That means, given a fundamental solution `a` and two different integers `n` and `m` such that `n < m`, the `y`-coordinate of `a^n` is strictly less than the `y`-coordinate of `a^m`.
More concisely: The function that maps an integer `n` to the `y`-coordinate of a fundamental solution `a` raised to the power of `n` in the Pell equation `x^2 - d*y^2 = 1` is strictly increasing for any integer `d`.
|
Pell.IsFundamental.mul_inv_y_nonneg
theorem Pell.IsFundamental.mul_inv_y_nonneg :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → 0 ≤ (a * a₁⁻¹).y
The theorem `Pell.IsFundamental.mul_inv_y_nonneg` states that for any integer 'd' and any solution 'a₁' to the Pell equation `x^2 - d*y^2 = 1`, if 'a₁' is a fundamental solution (meaning its `x` value is greater than 1, its `y` value is positive, and its `x` value is the smallest possible among solutions with `x` value greater than 1), then for any other solution 'a' to the Pell equation with `x` value greater than 1 and `y` value positive, the `y` coordinate of the product of 'a' and the inverse of 'a₁' remains nonnegative.
More concisely: If 'a₁' is a fundamental solution to the Pell equation 'x^2 - d*y^2 = 1' and 'a' is any other solution with x > 1 and y > 0, then the product of 'a' and the multiplicative inverse of 'a₁' has non-negative y-coordinate.
|
Pell.IsFundamental.d_pos
theorem Pell.IsFundamental.d_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → 0 < d
This theorem states that if a fundamental solution to the Pell equation `x^2 - d*y^2 = 1` exists, then the parameter `d` must be positive. A fundamental solution is defined as one where `x > 1` and `y > 0`, and the `x` value of this solution is the smallest among all solutions with `x > 1`. Therefore, if such a solution exists, it implies that `d` cannot be zero or negative.
More concisely: If a positive integer `d` has a fundamental solution for the Pell equation `x^2 - d*y^2 = 1`, then `d` must be positive.
|
Pell.IsFundamental.d_nonsquare
theorem Pell.IsFundamental.d_nonsquare : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ¬IsSquare d := by
sorry
This theorem states that if there exists a fundamental solution to the Pell equation `x^2 - d*y^2 = 1`, then the integer `d` cannot be a perfect square. A fundamental solution is defined as a solution where `x > 1` and `y > 0`, and among solutions with `x > 1`, `x` is the smallest possible. A number is defined as a perfect square if it can be expressed as the product of an integer with itself.
More concisely: If `d` is a positive integer such that the Pell equation `x^2 - d*y^2 = 1` has a fundamental solution, then `d` cannot be a perfect square.
|
Pell.exists_of_not_isSquare
theorem Pell.exists_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0
The theorem `Pell.exists_of_not_isSquare` states that for any positive integer `d` which is not a perfect square (an integer `a` is a perfect square if there exists an integer `r` such that `a = r * r`), there exists a pair of integers `x` and `y`, where `y` is non-zero, such that the Pell equation `x^2 - d*y^2 = 1` holds true. This is related to the theory of Pell's equations in number theory.
More concisely: For any positive integer not being a perfect square, there exist integers x and y (with y non-zero) such that x^2 - d*y^2 = 1.
|
Pell.Solution₁.eq_one_of_x_eq_one
theorem Pell.Solution₁.eq_one_of_x_eq_one : ∀ {d : ℤ}, d ≠ 0 → ∀ {a : Pell.Solution₁ d}, a.x = 1 → a = 1
This theorem states that for a solution of the Pell equation `x^2 - d*y^2 = 1`, where `d` is a non-zero integer, if the 'x' value of the solution is '1', then the solution itself is the trivial one '1'.
More concisely: If `d` is a non-zero integer and `x = 1` is a solution to the Pell equation `x^2 - d*y^2 = 1`, then `(1, 0)` is the trivial solution.
|
Pell.exists_iff_not_isSquare
theorem Pell.exists_iff_not_isSquare : ∀ {d : ℤ}, 0 < d → ((∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d) := by
sorry
The theorem `Pell.exists_iff_not_isSquare` states that for any positive integer `d`, there exists a nontrivial solution to the Pell equation `x^2 - d*y^2 = 1` if and only if `d` is not a perfect square. Here, a "nontrivial solution" means that `y` is not equal to zero. The `IsSquare` function is used to denote that a number is a perfect square, which means there exists some number `r` such that `r * r` equals the number.
More concisely: The Pell equation x^2 - d*y^2 = 1 has a nontrivial solution for a positive integer d if and only if d is not a perfect square.
|
Pell.IsFundamental.exists_of_not_isSquare
theorem Pell.IsFundamental.exists_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ a, Pell.IsFundamental a := by
sorry
This theorem states that for any positive integer `d` that is not a perfect square (an integer `a` is said to be a perfect square if there exists an integer `r` such that `a = r * r`), there exists a fundamental solution to the Pell equation. A solution is considered fundamental if it satisfies the conditions that `x > 1`, `y > 0`, and `x` is the smallest possible among solutions with `x > 1`.
More concisely: For any positive integer `d` not being a perfect square, the Pell equation `x² - d*y² = 1` has a fundamental solution `(x, y)` with `x > 1` and `y > 0`.
|
Pell.Solution₁.y_ne_zero_of_one_lt_x
theorem Pell.Solution₁.y_ne_zero_of_one_lt_x : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 1 < a.x → a.y ≠ 0
The theorem `Pell.Solution₁.y_ne_zero_of_one_lt_x` states that for any integer `d` and any solution `a` of the Pell equation `x^2 - d*y^2 = 1`, if `x` is greater than 1, then `y` cannot be 0. In other words, any solution to the Pell equation in which `x` exceeds 1 must have a non-zero `y` value. This theorem is a property of solutions to the Pell equation, a fundamental equation in the study of Diophantine equations in number theory.
More concisely: For any integer `d` and solution `(a, b)` of the Pell equation `x^2 - d*y^2 = 1` with `x > 1`, it holds that `y ≠ 0`.
|
Pell.Solution₁.exists_pos_variant
theorem Pell.Solution₁.exists_pos_variant :
∀ {d : ℤ}, 0 < d → ∀ (a : Pell.Solution₁ d), ∃ b, 0 < b.x ∧ 0 ≤ b.y ∧ a ∈ {b, b⁻¹, -b, -b⁻¹}
The theorem `Pell.Solution₁.exists_pos_variant` states that for any integer `d` greater than zero, given any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, there exists a solution `b` such that `b.x` is greater than zero, `b.y` is nonnegative, and `a` equals `b`, `b⁻¹` (the multiplicative inverse of `b`), `-b` (the additive inverse of `b`), or `-b⁻¹` (the additive inverse of `b⁻¹`).
More concisely: For any positive integer `d` and solution `a` to the Pell equation `x^2 - d*y^2 = 1`, there exists a solution `b` with `b.x > 0` and `b.y ≥ 0` such that `{a, b, -b, -a}` is a set of pairwise multiplicative and additive inverses.
|
Pell.Solution₁.ext
theorem Pell.Solution₁.ext : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, a.x = b.x → a.y = b.y → a = b
The theorem `Pell.Solution₁.ext` states that for any integer `d` and any two solutions `a` and `b` to the Pell equation `x^2 - d*y^2 = 1`, if the `x` component of `a` is equal to the `x` component of `b` and the `y` component of `a` is equal to the `y` component of `b`, then the solutions `a` and `b` themselves are equal. In other words, two solutions to the Pell equation are identical if they have the same `x` and `y` components.
More concisely: If two solutions (x₁, y₁) and (x₂, y₂) satisfy x₁^2 - d*y₁^2 = 1 and x₂^2 - d*y₂^2 = 1 with x₁ = x₂ and y₁ = y₂, then (x₁, y₁) = (x₂, y₂).
|
Pell.Solution₁.d_pos_of_one_lt_x
theorem Pell.Solution₁.d_pos_of_one_lt_x : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 1 < a.x → 0 < d
This theorem asserts that for every integer `d` and every solution `a` to the Pell equation `x^2 - d*y^2 = 1` (where x and y are elements of the set of integers, and d is non-zero), if the x-value of the solution `a` is greater than one, then `d` must be positive. In other words, if a solution to the Pell equation has its x-coordinate larger than 1, then the parameter `d` associated with that solution is guaranteed to be positive.
More concisely: If a solution exists to the Pell equation `x^2 - d*y^2 = 1` with `x > 1`, then `d` is positive.
|
Pell.IsFundamental.zpow_ne_neg_zpow
theorem Pell.IsFundamental.zpow_ne_neg_zpow :
∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → ∀ {n n' : ℤ}, a ^ n ≠ -a ^ n'
The theorem `Pell.IsFundamental.zpow_ne_neg_zpow` asserts that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1` that is fundamental, meaning `a.x > 1`, `a.y > 0`, and `a.x` is the smallest possible among solutions with `x > 1`, for any integers `n` and `n'`, the `n`-th power of `a` is never equal to the negative of the `n'`-th power of `a`.
More concisely: For any fundamental solution `a` to the Pell equation `x^2 - d*y^2 = 1`, `a.x^n` and `a.x^(-n')` are never equal for any integers `n` and `n'`.
|
Pell.Solution₁.y_pow_succ_pos
theorem Pell.Solution₁.y_pow_succ_pos :
∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → ∀ (n : ℕ), 0 < (a ^ n.succ).y
The theorem `Pell.Solution₁.y_pow_succ_pos` states that for any solution `(x, y)` to the Pell equation `x^2 - d*y^2 = 1`, where both `x` and `y` are positive integers, and for any positive natural number exponent `n`, the `y` component of the `n`-th power of the solution will also be a positive integer. This means that raising a positive solution of the Pell equation to any positive power will always yield a solution with a positive `y` component.
More concisely: For any positive solution `(x, y)` of the Pell equation `x^2 - d*y^2 = 1` with `d > 0`, the `y` component of the `n`-th power `(x, y)^n` is a positive integer.
|
Pell.Solution₁.x_pow_pos
theorem Pell.Solution₁.x_pow_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → ∀ (n : ℕ), 0 < (a ^ n).x
The theorem `Pell.Solution₁.x_pow_pos` states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1`, if `x` is positive in that solution, then `x` will also be positive for all natural number powers of that solution. In other words, if `a` is a solution to the Pell equation and the `x` value of `a` is positive, then the `x` value of `a` raised to any natural number power will also be positive.
More concisely: If a solution to the Pell equation `x^2 - d*y^2 = 1` has a positive `x` value, then `x` raised to any natural power remains positive.
|
Pell.Solution₁.y_zpow_pos
theorem Pell.Solution₁.y_zpow_pos :
∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → ∀ {n : ℤ}, 0 < n → 0 < (a ^ n).y
This theorem states that for any integer `d` and any solution `a` to the Pell equation `x^2 - d*y^2 = 1` with `x` and `y` being positive, the `y` component of `a` raised to any positive integer power `n` is also positive. In other words, for positive `x` and `y` in the Pell equation, computing `a^n` for any positive `n` will always result in a positive `y` component.
More concisely: For any positive integer `d` and solution `(x, y)` of the Pell equation `x^2 - d*y^2 = 1`, the `y` component `y^n` of `(x, y)` raised to any positive integer power `n` is also positive.
|
Pell.IsFundamental.eq_zpow_or_neg_zpow
theorem Pell.IsFundamental.eq_zpow_or_neg_zpow :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ (a : Pell.Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n
The theorem `Pell.IsFundamental.eq_zpow_or_neg_zpow` states that for any integer `d` and any solution `a₁` to the Pell equation `x^2 - d*y^2 = 1` that is fundamental (meaning `x > 1`, `y > 0`, and `x` is the smallest possible among solutions with `x > 1`), for any other solution `a` to the Pell equation, there exists some integer `n` such that `a` is either the `n`th power of `a₁` or the `n`th power of `-a₁`. In other words, every solution to the Pell equation can be expressed as a power (or the negative of a power) of a given fundamental solution.
More concisely: For every fundamental solution `a₁` of the Pell equation `x^2 - d*y^2 = 1`, any other solution `a` to the equation can be expressed as `a = k^n * a₁` or `a = k^n * (-a₁)` for some integers `k` and `n`.
|
Pell.Solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos
theorem Pell.Solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos :
∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → ∀ (n : ℤ), (a ^ n).y.sign = n.sign
The theorem `Pell.Solution₁.sign_y_zpow_eq_sign_of_x_pos_of_y_pos` states that for any integer `d` and a solution `a` to the Pell equation `x^2 - d*y^2 = 1` where `x` and `y` are both positive, the sign of the `y` component of any power of `a` is the same as the sign of the exponent. In other words, if we raise the solution `a` to any integer power `n`, then the sign of the `y` component of the resulting solution is the same as the sign of `n`.
More concisely: For any positive integer solution `a` of the Pell equation `x^2 - d*y^2 = 1`, the sign of the `y` component of `a` raised to any integer power `n` is equal to the sign of `n`.
|
Pell.Solution₁.x_zpow_pos
theorem Pell.Solution₁.x_zpow_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → ∀ (n : ℤ), 0 < (a ^ n).x
The theorem `Pell.Solution₁.x_zpow_pos` states that for every integer `d` and every solution `a` to the Pell equation `x^2 - d*y^2 = 1` (where the solutions are represented as elements of the integer ring extended by the square root of `d` with norm one), if the `x` component of the solution is positive, then the `x` component of any power of the solution (where the power is an integer) is also positive. In other words, raising a solution with a positive `x` component to any integer power retains the positivity of the `x` component.
More concisely: For every integer `d` and solution `a` of the Pell equation `x^2 - d*y^2 = 1` with positive `x` component, the `x` component of any integer power of `a` is also positive.
|
Pell.Solution₁.exists_pos_of_not_isSquare
theorem Pell.Solution₁.exists_pos_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ a, 1 < a.x ∧ 0 < a.y
The theorem `Pell.Solution₁.exists_pos_of_not_isSquare` states that if `d` is a positive integer that is not a perfect square (i.e., there is no integer `r` such that `d = r * r`), then there exists a solution to the Pell equation `x^2 - d*y^2 = 1` where `x > 1` and `y > 0`. In other words, for any positive non-square integer `d`, there are integers `x` and `y` satisfying the Pell equation such that `x` is greater than 1 and `y` is positive.
More concisely: For any positive integer `d` not being a perfect square, there exist integers `x > 1` and `y > 0` satisfying the Pell equation `x^2 - d*y^2 = 1`.
|
Pell.IsFundamental.mul_inv_x_lt_x
theorem Pell.IsFundamental.mul_inv_x_lt_x :
∀ {d : ℤ} {a₁ : Pell.Solution₁ d},
Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → 0 < a.y → (a * a₁⁻¹).x < a.x
The theorem `Pell.IsFundamental.mul_inv_x_lt_x` states that for any integer 'd' and any solution 'a₁' to the Pell equation `x^2 - d*y^2 = 1`, if 'a₁' is a fundamental solution (i.e., it has `x > 1` and `y > 0` and it is the solution with the smallest `x` among those with `x > 1`), then for any other solution 'a' of the Pell equation with `x > 1` and `y > 0`, when we multiply 'a' with the inverse of 'a₁', the `x`-coordinate of the product is strictly less than the `x`-coordinate of 'a'. In other words, multiplying a positive solution by the inverse of a fundamental solution reduces the `x`-coordinate.
More concisely: For any integer d and fundamental solution (x₁, y₁) of the Pell equation x² - d*y² = 1 with x₁ > 1 and y₁ > 0, the product of any other solution (x, y) with x > 1 and y > 0 and the inverse of (x₁, y₁) has an x-coordinate strictly smaller than x.
|
Pell.Solution₁.y_mul_pos
theorem Pell.Solution₁.y_mul_pos :
∀ {d : ℤ} {a b : Pell.Solution₁ d}, 0 < a.x → 0 < a.y → 0 < b.x → 0 < b.y → 0 < (a * b).y
The theorem `Pell.Solution₁.y_mul_pos` states that for any integer `d` and any two solutions `a` and `b` to the Pell equation `x^2 - d*y^2 = 1` (where `Pell.Solution₁ d` represents such solutions), if the `x` and `y` components of both `a` and `b` are positive, then the `y` component of the product of `a` and `b` is also positive. In other words, the set of solutions to the Pell equation where both `x` and `y` are positive, is closed under multiplication.
More concisely: For any integers `d`, if `a` and `b` are solutions to the Pell equation `x^2 - d*y^2 = 1` with positive `x` components, then the `y` component of their product `a * b` is also positive.
|