~/bend-docscommunity

fermat4.bend checks

raw source on the hub · import 0xd5e9362591c1667c9894b781190e1ac9/fermat4.bend as Fermat4

demos/math/fermat4.bend -- Fermat's Last Theorem for exponent 4.

x^4 + y^4 = z^4 has no solution in positive naturals

This is Fermat's own case, and the only one he left a proof of. It is proved here as he proved it, by infinite descent, on the stronger statement that x^4 + y^4 is never a perfect SQUARE.

THE ARGUMENT, in words.

Suppose x^4 + y^4 = z^2 with x, y, z > 0 and gcd(x, y) = 1, and take a solution with z as small as possible (here: run a fuel down from z). Then (x^2)^2 + (y^2)^2 = z^2 is a PRIMITIVE Pythagorean triple. One of x, y is even -- not both, since they are coprime, and not neither, since odd^2 + odd^2 is 2 mod 4 and never a square (lib/pythag.bend's py.odd_odd) -- so name them with y even. The parametrisation of primitive triples (lib/pythag.bend's py.pyth) gives coprime m > n > 0 with

x^2 = m^2 - n^2, y^2 = 2 m n, z = m^2 + n^2.

Now x^2 + n^2 = m^2 is a second primitive triple. Its odd leg is x, so n is the even one -- again because odd^2 + odd^2 is no square -- and x is coprime to n because a common divisor would divide m^2 and n^2. Parametrising it gives coprime r, s > 0 with

x = r^2 - s^2, n = 2 r s, m = r^2 + s^2.

Then y^2 = 2 m n = 4 r s m, and y is even, say y = 2Y, so

Y^2 = r * s * m

with r, s, m pairwise coprime (r and s by construction, and each of them with m = r^2 + s^2 because a common divisor would divide the other square). A product of pairwise coprime numbers is a square only if each factor is (lib/gcd.bend's gc.sq_of_cop), so

r = a^2, s = b^2, m = c^2,

and therefore a^4 + b^4 = r^2 + s^2 = m = c^2: a NEW solution. It is smaller: c <= c^2 = m <= m^2 < m^2 + n^2 = z. Descent, contradiction.

The general case then follows: divide x and y by their gcd G. Since G^4 divides z^4 and (G^2)^2 | (z^2)^2 forces G^2 | z^2 and then G | z (lib/gcd.bend's gc.sq_dvd), the reduced triple is again a solution.

The statement at the bottom is in the vocabulary of demos/math/mathlib.bend, so the website's math card can quote it directly.

6 imports
import Base
import ./mathlib.bend as M
import ./nat.bend as N
import ./sqrt2.bend as S2
import ./gcd.bend as G
import ./pythag.bend as PY

Definitions

def f4.add_bridge source · line 61 · raw

@a:Nat -> @-b:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.add(a, b) == Nat.add(a, b) : Nat}

def f4.mul_bridge source · line 68 · raw

@a:Nat -> @+b:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.mul(a, b) == Nat.mul(a, b) : Nat}

def f4.pow4_bridge source · line 78 · raw

@+a:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(a, 4n) == Nat.mul(Nat.mul(a, a), Nat.mul(a, a)) : Nat}

a^4, mathlib's way and Base's, are the same number

def f4.nat_eq_false source · line 96 · raw

@a:Nat -> @b:Nat -> @ne:(@_:{a == b : Nat} -> Empty) -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_eq(a, b) == False{} : Bool}

the Bool test is faithful: a proof that the equation is impossible makes nat_eq return False

def f4.Rec source · line 116 · raw

@g:Nat -> Type

def f4.rot3 source · line 121 · raw

@+p:Nat -> @+q:Nat -> @+t:Nat -> {Nat.mul(p, Nat.mul(q, t)) == Nat.mul(q, Nat.mul(t, p)) : Nat}

p (q t) = q (t p)

def f4.s4 source · line 128 · raw

@+g:Nat -> @+zv:Nat -> @+mv:Nat -> @+nv:Nat -> @+rv:Nat -> @+sv:Nat -> @+av:Nat -> @+bv:Nat -> @+cv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hc1:{1n+zv == Nat.add(Nat.mul(1n+mv, 1n+mv), Nat.mul(1n+nv, 1n+nv)) : Nat} -> @hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @ha:{Nat.mul(1n+av, 1n+av) == 1n+rv : Nat} -> @hb:{Nat.mul(1n+bv, 1n+bv) == 1n+sv : Nat} -> @+hcc:{Nat.mul(1n+cv, 1n+cv) == 1n+mv : Nat} -> @hcopab:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+av, 1n+bv> -> @rec:f4.Rec(g) -> Empty

THE LAST STEP: a^4 + b^4 = c^2 with c < z, handed to the induction hypothesis. c <= c^2 = m <= m^2 < m^2 + n^2 = z.

def f4.copRM.k source · line 150 · raw

@+rv:Nat -> @+sv:Nat -> @+mv:Nat -> @+hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @+hcop_rs:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+sv> -> @+gg:Nat -> @d1:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<gg, 1n+rv> -> @d2:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<gg, 1n+mv> -> {gg == 1n : Nat}

r and m = r^2 + s^2 are coprime: a common divisor divides r^2, hence s^2

def f4.copRM source · line 159 · raw

@+rv:Nat -> @+sv:Nat -> @+mv:Nat -> @+hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @+hcop_rs:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+sv> -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+mv>

def f4.copSM.k source · line 162 · raw

@+rv:Nat -> @+sv:Nat -> @+mv:Nat -> @+hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @+hcop_rs:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+sv> -> @+gg:Nat -> @d1:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<gg, 1n+sv> -> @d2:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<gg, 1n+mv> -> {gg == 1n : Nat}

def f4.copSM source · line 173 · raw

@+rv:Nat -> @+sv:Nat -> @+mv:Nat -> @+hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @+hcop_rs:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+sv> -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+sv, 1n+mv>

def f4.s3b source · line 177 · raw

@+g:Nat -> @+zv:Nat -> @+mv:Nat -> @+nv:Nat -> @+rv:Nat -> @+sv:Nat -> @+yy:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hc1:{1n+zv == Nat.add(Nat.mul(1n+mv, 1n+mv), Nat.mul(1n+nv, 1n+nv)) : Nat} -> @+hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @+hcop_rs:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+sv> -> @+key:{Nat.mul(yy, yy) == Nat.mul(1n+mv, Nat.mul(1n+rv, 1n+sv)) : Nat} -> @rec:f4.Rec(g) -> Empty

Y^2 = r s m with r, s, m pairwise coprime: each is a square

def f4.s3a source · line 216 · raw

@+g:Nat -> @+yv:Nat -> @+zv:Nat -> @+mv:Nat -> @+nv:Nat -> @+rv:Nat -> @+sv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hc1:{1n+zv == Nat.add(Nat.mul(1n+mv, 1n+mv), Nat.mul(1n+nv, 1n+nv)) : Nat} -> @hc2:{1n+mv == Nat.add(Nat.mul(1n+rv, 1n+rv), Nat.mul(1n+sv, 1n+sv)) : Nat} -> @hb1:{Nat.mul(1n+yv, 1n+yv) == Nat.double(Nat.mul(1n+mv, 1n+nv)) : Nat} -> @hb2:{1n+nv == Nat.double(Nat.mul(1n+rv, 1n+sv)) : Nat} -> @hcop_rs:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+rv, 1n+sv> -> @hyeven:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == True{} : Bool} -> @rec:f4.Rec(g) -> Empty

y = 2Y, and Y^2 = m (r s)

def f4.n1even source · line 235 · raw

@+xv:Nat -> @+nv:Nat -> @+mv:Nat -> @hxodd:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == False{} : Bool} -> @ha1:{Nat.add(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+nv, 1n+nv)) == Nat.mul(1n+mv, 1n+mv) : Nat} -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+nv) == c : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+nv) == True{} : Bool}

the second triple x^2 + n^2 = m^2: n is even, x is coprime to n

def f4.copXN.k source · line 243 · raw

@+xv:Nat -> @+nv:Nat -> @+mv:Nat -> @+ha1:{Nat.add(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+nv, 1n+nv)) == Nat.mul(1n+mv, 1n+mv) : Nat} -> @+hcop_mn:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+mv, 1n+nv> -> @+gg:Nat -> @d1:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<gg, 1n+xv> -> @d2:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<gg, 1n+nv> -> {gg == 1n : Nat}

def f4.copXN source · line 251 · raw

@+xv:Nat -> @+nv:Nat -> @+mv:Nat -> @+ha1:{Nat.add(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+nv, 1n+nv)) == Nat.mul(1n+mv, 1n+mv) : Nat} -> @+hcop_mn:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+mv, 1n+nv> -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+xv, 1n+nv>

def f4.s2b source · line 254 · raw

@+g:Nat -> @+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+mv:Nat -> @+nv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hb1:{Nat.mul(1n+yv, 1n+yv) == Nat.double(Nat.mul(1n+mv, 1n+nv)) : Nat} -> @hc1:{1n+zv == Nat.add(Nat.mul(1n+mv, 1n+mv), Nat.mul(1n+nv, 1n+nv)) : Nat} -> @hyeven:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == True{} : Bool} -> @rec:f4.Rec(g) -> @pt:0xd5e9362591c1667c9894b781190e1ac9/pythag.Pyth<1n+xv, 1n+nv, 1n+mv> -> Empty

def f4.s2 source · line 259 · raw

@+g:Nat -> @+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+mv:Nat -> @+nv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hcop_mn:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+mv, 1n+nv> -> @+ha1:{Nat.add(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+nv, 1n+nv)) == Nat.mul(1n+mv, 1n+mv) : Nat} -> @hb1:{Nat.mul(1n+yv, 1n+yv) == Nat.double(Nat.mul(1n+mv, 1n+nv)) : Nat} -> @hc1:{1n+zv == Nat.add(Nat.mul(1n+mv, 1n+mv), Nat.mul(1n+nv, 1n+nv)) : Nat} -> @hxodd:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == False{} : Bool} -> @hyeven:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == True{} : Bool} -> @rec:f4.Rec(g) -> Empty

def f4.s1b source · line 265 · raw

@+g:Nat -> @+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hxodd:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == False{} : Bool} -> @hyeven:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == True{} : Bool} -> @rec:f4.Rec(g) -> @pt:0xd5e9362591c1667c9894b781190e1ac9/pythag.Pyth<Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+yv, 1n+yv), 1n+zv> -> Empty

def f4.s1 source · line 271 · raw

@+g:Nat -> @+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+xv, 1n+yv> -> @hxodd:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == False{} : Bool} -> @+hyeven:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == True{} : Bool} -> @e:{Nat.add(Nat.mul(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+xv, 1n+xv)), Nat.mul(Nat.mul(1n+yv, 1n+yv), Nat.mul(1n+yv, 1n+yv))) == Nat.mul(1n+zv, 1n+zv) : Nat} -> @rec:f4.Rec(g) -> Empty

THE STEP: the first parametrisation

def f4.yeven source · line 279 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+hxodd:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == False{} : Bool} -> @e:{Nat.add(Nat.mul(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+xv, 1n+xv)), Nat.mul(Nat.mul(1n+yv, 1n+yv), Nat.mul(1n+yv, 1n+yv))) == Nat.mul(1n+zv, 1n+zv) : Nat} -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == c : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == True{} : Bool}

exactly one of x, y is even: both even contradicts coprimality, and neither even contradicts py.odd_odd applied to (x^2)^2 + (y^2)^2 = z^2

def f4.yodd source · line 290 · raw

@+xv:Nat -> @+yv:Nat -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+xv, 1n+yv> -> @+hxe:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == True{} : Bool} -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == c : Bool} -> {0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+yv) == False{} : Bool}

def f4.branch source · line 302 · raw

@+g:Nat -> @+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, 1n+g) -> @+hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+xv, 1n+yv> -> @+e:{Nat.add(Nat.mul(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+xv, 1n+xv)), Nat.mul(Nat.mul(1n+yv, 1n+yv), Nat.mul(1n+yv, 1n+yv))) == Nat.mul(1n+zv, 1n+zv) : Nat} -> @rec:f4.Rec(g) -> @c:Bool -> @ec:{0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.even(1n+xv) == c : Bool} -> Empty

name the odd leg first, swapping x and y if necessary

def f4.absurd_le21 source · line 319 · raw

@h:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(2n, 1n) -> Empty

def f4.go source · line 324 · raw

@f:Nat -> @+xv:Nat -> @+yv:Nat -> @zv:Nat -> @bound:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Le(zv, f) -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+xv, 1n+yv> -> @e:{Nat.add(Nat.mul(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+xv, 1n+xv)), Nat.mul(Nat.mul(1n+yv, 1n+yv), Nat.mul(1n+yv, 1n+yv))) == Nat.mul(1n+zv, 1n+zv) : Nat} -> Empty

THE DESCENT. The fuel bounds z and every step produces a strictly smaller z, so the fuel really runs down.

def f4.no_coprime source · line 343 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<1n+xv, 1n+yv> -> @e:{Nat.add(Nat.mul(Nat.mul(1n+xv, 1n+xv), Nat.mul(1n+xv, 1n+xv)), Nat.mul(Nat.mul(1n+yv, 1n+yv), Nat.mul(1n+yv, 1n+yv))) == Nat.mul(1n+zv, 1n+zv) : Nat} -> Empty

no coprime solution

def f4.p4 source · line 350 · raw

@+t:Nat -> Nat

def f4.p4_mul source · line 354 · raw

@+a:Nat -> @+b:Nat -> {f4.p4(Nat.mul(a, b)) == Nat.mul(f4.p4(a), f4.p4(b)) : Nat}

(a b)^4 = a^4 b^4

def f4.pos_mul source · line 359 · raw

@a:Nat -> @pa:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, a) -> @b:Nat -> @pb:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, b) -> 0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, Nat.mul(a, b))

def f4.gsum source · line 371 · raw

@+xv:Nat -> @+yv:Nat -> @+gp:Nat -> @+x1:Nat -> @+y1:Nat -> @ex:{Nat.mul(1n+gp, x1) == 1n+xv : Nat} -> @ey:{Nat.mul(1n+gp, y1) == 1n+yv : Nat} -> {Nat.mul(f4.p4(1n+gp), Nat.add(f4.p4(x1), f4.p4(y1))) == Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) : Nat}

G^4 (x1^4 + y1^4) = x^4 + y^4, where x = G x1 and y = G y1

def f4.gdvd source · line 384 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+gp:Nat -> @+x1:Nat -> @+y1:Nat -> @ex:{Nat.mul(1n+gp, x1) == 1n+xv : Nat} -> @ey:{Nat.mul(1n+gp, y1) == 1n+yv : Nat} -> @e:{Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) == Nat.mul(1n+zv, 1n+zv) : Nat} -> 0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<Nat.mul(1n+gp, 1n+gp), 1n+zv>

G^4 divides z^2, so (G^2)^2 | z^2 and therefore G^2 | z

def f4.no_coprime_pos source · line 390 · raw

@x:Nat -> @px:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, x) -> @y:Nat -> @py:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, y) -> @z:Nat -> @pz:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, z) -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<x, y> -> @e:{Nat.add(f4.p4(x), f4.p4(y)) == Nat.mul(z, z) : Nat} -> Empty

def f4.main_sq.fin source · line 405 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+gp:Nat -> @+x1:Nat -> @+y1:Nat -> @+z1:Nat -> @+ex:{Nat.mul(1n+gp, x1) == 1n+xv : Nat} -> @+ey:{Nat.mul(1n+gp, y1) == 1n+yv : Nat} -> @+ez:{Nat.mul(Nat.mul(1n+gp, 1n+gp), z1) == 1n+zv : Nat} -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<x1, y1> -> @+e:{Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) == Nat.mul(1n+zv, 1n+zv) : Nat} -> Empty

def f4.main_sq.dz source · line 419 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+gp:Nat -> @+x1:Nat -> @+y1:Nat -> @+ex:{Nat.mul(1n+gp, x1) == 1n+xv : Nat} -> @+ey:{Nat.mul(1n+gp, y1) == 1n+yv : Nat} -> @hcop:0xd5e9362591c1667c9894b781190e1ac9/gcd.Cop<x1, y1> -> @+e:{Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) == Nat.mul(1n+zv, 1n+zv) : Nat} -> @dz:0xd5e9362591c1667c9894b781190e1ac9/gcd.Dvd<Nat.mul(1n+gp, 1n+gp), 1n+zv> -> Empty

def f4.main_sq.op source · line 424 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+e:{Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) == Nat.mul(1n+zv, 1n+zv) : Nat} -> @sp:0xd5e9362591c1667c9894b781190e1ac9/gcd.Split<1n+xv, 1n+yv> -> Empty

def f4.main_sq source · line 436 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @+e:{Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) == Nat.mul(1n+zv, 1n+zv) : Nat} -> Empty

x^4 + y^4 is never a square, for positive x and y

def f4.main_sq_pos source · line 439 · raw

@x:Nat -> @px:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, x) -> @y:Nat -> @py:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, y) -> @z:Nat -> @pz:0xd5e9362591c1667c9894b781190e1ac9/nat.Nat.Lt(0n, z) -> @e:{Nat.add(f4.p4(x), f4.p4(y)) == Nat.mul(z, z) : Nat} -> Empty

def f4.main source · line 455 · raw

@+xv:Nat -> @+yv:Nat -> @+zv:Nat -> @e:{Nat.add(f4.p4(1n+xv), f4.p4(1n+yv)) == f4.p4(1n+zv) : Nat} -> Empty

and in particular x^4 + y^4 = z^4 is impossible: z^4 is the square of z^2

def f4.carry source · line 463 · raw

@+x2:Nat -> @+y2:Nat -> {Nat.add(f4.p4(1n+x2), f4.p4(1n+y2)) == 0xd5e9362591c1667c9894b781190e1ac9/mathlib.add(0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+x2, 4n), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+y2, 4n)) : Nat}

the equation carried from mathlib's operators to Base's

def fermat_n4 source · line 473 · raw

@x:Nat -> @y:Nat -> @z:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_eq(0xd5e9362591c1667c9894b781190e1ac9/mathlib.add(0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+x, 4n), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+y, 4n)), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+z, 4n)) == False{} : Bool}

x^4 + y^4 = z^4 has no solution in positive naturals (Fermat's own case, by infinite descent). The 1n+ makes each variable positive.

def fermat_n4_square source · line 486 · raw

@x:Nat -> @y:Nat -> @z:Nat -> {0xd5e9362591c1667c9894b781190e1ac9/mathlib.nat_eq(0xd5e9362591c1667c9894b781190e1ac9/mathlib.add(0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+x, 4n), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.pow(1n+y, 4n)), 0xd5e9362591c1667c9894b781190e1ac9/mathlib.mul(1n+z, 1n+z)) == False{} : Bool}

the stronger statement the descent actually proves: x^4 + y^4 is never a perfect square, for positive x and y