Congruum

Stream: Is there code for X?

[Wouter Smeenk]

Is there a proof for https://en.m.wikipedia.org/wiki/Congruum#Parameterized_solution in mathlib?

[Johan Commelin]

I don't think so.

[Alex J. Best]

It sounds related to the parameterization of pythagorean triples though, which we do have

[Kevin Buzzard]

It would be a nice lean exercise to show that an integer c is a solution to c=x^2-y^2=y^2-z^2 iff c can be written as 4t^2mn(m^2-n^2).

[Yury G. Kudryashov]

Or you can add a rational parametrization of any quadric over any field, not necessarily the sphere.

[Kevin Buzzard]

There is an integrality question too (up to squares these are just the congruent numbers, but it's not true that you can cast squares out of congruum numbers eg 24 is congruum but 6 isn't)

[Wouter Smeenk]

I am trying to formalize this. I am wondering if this is the correct thing to prove in this case:

lemma congruum : (∃ x y z : ℤ, c = x^2 - y^2 ∧ c = y^2 - z^2) ↔
                 ∃ m n : ℤ, m > n ∧ c = 4 * m * n * (m^2-n^2) := by
  constructor
  . intro h
    rcases h with ⟨x, y, z, hcxy, hcxz⟩
    sorry
  . intro h
    rcases h with ⟨m, n, hmn, hc⟩
    use m^2 + 2 * m * n - n^2
    use m^2 + n^2
    use m^2 - 2 * m * n - n^2
    constructor
    . rw [hc]; ring
    . rw [hc]; ring

[Kevin Buzzard]

As it stands this might be false, right? Do you know a maths proof of the sorry? I don't. My version above had a t^2 in.

[Wouter Smeenk]

No I don't. I could not find a public source for the proof. You are right about the t^2 I think. I will try to incorporate it. I was specifically wondering if the use of the iff and exists is correct (matches the description of the wiki)

[Kevin Buzzard]

It looks fine other than the t issue. It might be good if you named c explicitly

[Wouter Smeenk]

Updated version:

lemma congruum : ∀ c : ℤ, (∃ x y z : ℤ, c = x^2 - y^2 ∧ c = y^2 - z^2) ↔
                 ∃ m n t: ℤ, m > n ∧ c = 4 * t^2 * m * n * (m^2-n^2) := by
  intro c
  constructor
  . intro h
    rcases h with ⟨x, y, z, hcxy, hcxz⟩
    sorry
  . intro h
    rcases h with ⟨m, n, t, hmn, hc⟩
    use t * (m^2 + 2 * m * n - n^2)
    use t * (m^2 + n^2)
    use t * (m^2 - 2 * m * n - n^2)
    constructor
    . rw [hc]; ring
    . rw [hc]; ring

[Wouter Smeenk]

Thanks for the help so far! If anyone knows of a proof for this or where to find it that would be great!

[Kevin Buzzard]

You mean a maths proof or a lean proof?

[Kevin Buzzard]

I would drop the m > n by the way, this is if you're dealing with naturals but you have used integers. A maths proof of the harder direction is: given x y z, we have $(x/y)^2+(z/y)^2=2$ (deal with $y=0$ case separately). Now set $\lambda=(x-y)/(z-y)$ (deal with $z=y$ case separately) so $(x/y)-1=\lambda((z/y)-1)$. Think of this as a line $b-1=\lambda (a-1)$ meeting the circle $a^2+b^2=2$ in two points, namely $a=b=1$ and $a=x/y$, $b=z/y$. Eliminating $b$ gives $(\lambda^2+1)a^2+2\lambda (1-\lambda)a+(-1-2\lambda+\lambda^2)=0$. This quadratic has two roots and their sum is $2\lambda(\lambda-1)/(\lambda^2+1)$, so this must be $z/y+1$. This gives you a formula for $z/y$ in terms of $\lambda$ (it's $(\lambda^2-2\lambda-1)/(\lambda^2+1)$), and using $b-1=\lambda(a-1)$ you also get a formula for $x/y$ (it's $(-\lambda^2-2\lambda+1)/(\lambda^2+1)$). Now write $\lambda=m/n$ in lowest terms and tidy up; the $t$ is the gcd of $x$ and $y$.

[Alex Kontorovich]

You can use this: https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/PythagoreanTriples.html
Set $a=(z-x)/2$ and $b=(z+x)/2$. Then $(a,b,y)$ is a Pythagorean triple, and apply the classification PythagoreanTriple.coprime_classification.

[Kevin Buzzard]

aah this is a better route: I'm parametrising the conic but apparently we already have it parametrised.

[Wouter Smeenk]

Thanks! I meant a maths proof indeed. I will try to make sense of this :P. Has been a long time since I did any serious math...;)