PNat.XgcdType.step_v
theorem PNat.XgcdType.step_v : ∀ (u : PNat.XgcdType), u.r ≠ 0 → u.step.v = u.v.swap
This theorem states that for any positive natural number of a certain type (`PNat.XgcdType`), given that `u.r` is not equal to `0`, the vector after a reduction step (`u.step.v`) is the same as the vector before the reduction step (`u.v`), but with its elements swapped. This implies that the process of reduction, in the context of the Extended Euclidean Algorithm which `PNat.XgcdType` is based on, does not affect the 'value' of the vector but merely swaps its elements.
More concisely: For any `u` of type `PNat.XgcdType` with `u.r ≠ 0`, the reduction step `u.step` results in the vector `u.v` being swapped with `u.step.v`.
|
PNat.XgcdType.reduce_b
theorem PNat.XgcdType.reduce_b : ∀ {u : PNat.XgcdType}, u.r ≠ 0 → u.reduce = u.step.reduce.flip
The theorem `PNat.XgcdType.reduce_b` states that for any positive natural number type `u`, if the remainder `r` of `u` (computed as `(u.ap + 1) % (u.bp + 1)`) is not zero, then the result of the function `PNat.XgcdType.reduce` on `u` is equivalent to flipping (`PNat.XgcdType.flip`) the result of `PNat.XgcdType.reduce` on the next step (`PNat.XgcdType.step u`) of the Euclidean algorithm. This encapsulates one of the key steps in the Euclidean algorithm for finding the greatest common divisor, namely that when the remainder is not zero, the algorithm proceeds by reducing the larger number by the remainder and then switching the roles of the two numbers.
More concisely: If the remainder of the Euclidean algorithm for positive natural numbers `u` is non-zero, then `PNat.XgcdType.reduce u` is equivalent to `PNat.XgcdType.flip (PNat.XgcdType.reduce (PNat.XgcdType.step u))`.
|
PNat.XgcdType.reduce_a
theorem PNat.XgcdType.reduce_a : ∀ {u : PNat.XgcdType}, u.r = 0 → u.reduce = u.finish
The theorem `PNat.XgcdType.reduce_a` states that for any positive natural number `u` of the type `PNat.XgcdType`, if the remainder function `PNat.XgcdType.r u` equals to zero, implying that `(u.ap + 1)` is divisible by `(u.bp + 1)`, then the `reduce` operation on `u` is equivalent to the `finish` operation on `u`. This theorem is essentially a rule about the relationship between the `reduce` and `finish` operations in the context of the Euclidean algorithm for positive natural numbers.
More concisely: If `u` is a positive natural number with `PNat.XgcdType.r u = 0` implying `(u.ap + 1)` divides `(u.bp + 1)`, then `PNat.XgcdType.reduce u = PNat.XgcdType.finish u`.
|
PNat.XgcdType.step_wf
theorem PNat.XgcdType.step_wf : ∀ (u : PNat.XgcdType), u.r ≠ 0 → sizeOf u.step < sizeOf u
The theorem `PNat.XgcdType.step_wf` asserts for all values of type `PNat.XgcdType` denoted as `u`, if the remainder (`PNat.XgcdType.r u`) is not equal to 0, then the size of the `PNat.XgcdType` object produced by the `PNat.XgcdType.step` function on `u` is strictly smaller than the size of `u`. This theorem is crucial in ensuring that the recursive application of the `PNat.XgcdType.step` function eventually terminates.
More concisely: For all `PNat.XgcdType` values `u`, if the remainder `PNat.XgcdType.r u` is non-zero, then the size of `PNat.XgcdType.step u` is strictly smaller than the size of `u`.
|
PNat.gcd_props
theorem PNat.gcd_props :
∀ (a b : ℕ+),
let d := a.gcdD b;
let w := a.gcdW b;
let x := a.gcdX b;
let y := a.gcdY b;
let z := a.gcdZ b;
let a' := a.gcdA' b;
let b' := a.gcdB' b;
w * z = (x * y).succPNat ∧
a = a' * d ∧
b = b' * d ∧
z * a' = (x * ↑b').succPNat ∧ w * b' = (y * ↑a').succPNat ∧ ↑z * ↑a = x * ↑b + ↑d ∧ ↑w * ↑b = y * ↑a + ↑d
This theorem, `PNat.gcd_props`, asserts a collection of properties about the greatest common divisor operation on positive natural numbers. For every two positive natural numbers `a` and `b`, it provides a set of equations involving the results of several functions applied to `a` and `b`.
Firstly, it states that the product of the final values of `w` and `z` from the extended GCD operation is equal to one plus the product of the final values of `x` and `y`. Secondly, it states that `a` and `b` are each equal to the product of the final value of `a / d` (`a'`) or `b / d` (`b'`) and the GCD `d` respectively.
It also provides two equations relating `a'`, `x`, `b'`, `y`, `z`, `w` with conversions of `b'` and `a'` to natural numbers. Lastly, it asserts two equations that relate `z`, `a`, `x`, `b`, `d` and `w`, `b`, `y`, `a`, `d`. These equations are key properties in the theory of greatest common divisors.
More concisely: The theorem `PNat.gcd_props` in Lean 4 establishes the properties of the greatest common divisor `d` of positive natural numbers `a` and `b`, including the equations: `a * d * z + b * d * w = a' * b' + 1`, `a = a' * d` and `b = b' * d`, where `a'`, `b'`, `x`, `y`, `z`, `w` are the results of the extended GCD algorithm.
|
PNat.gcd_eq
theorem PNat.gcd_eq : ∀ (a b : ℕ+), a.gcdD b = a.gcd b
The theorem `PNat.gcd_eq` states that for any two positive natural numbers `a` and `b`, the value of the greatest common divisor computed using the `gcdD` function, which is defined as the `a` value of the extended greatest common divisor, is equal to the greatest common divisor computed using the standard `gcd` function.
More concisely: For all natural numbers `a` and `b` greater than 0, `gcd a b` equals the `a`-th component of the extended greatest common divisor of `a` and `b`.
|
PNat.XgcdType.rq_eq
theorem PNat.XgcdType.rq_eq : ∀ (u : PNat.XgcdType), u.r + (u.bp + 1) * u.q = u.ap + 1
This theorem states that for all positive natural numbers u represented by the type `PNat.XgcdType`, the sum of the remainder (`r = a % b`) and the product of `u.bp + 1` and the quotient (`q = ap / bp`) equals `u.ap + 1`. This essentially captures the properties of Euclidean division, where the dividend is equal to the divisor times the quotient plus the remainder.
More concisely: For all positive natural numbers u represented by `PNat.XgcdType`, the theorem asserts that `u.ap + 1 = u.bp * q + r`, where `q` is the quotient, `r` is the remainder, and `a = u.ap * b` and `b = u.bp`.
|