Zulip Chat Archive

Stream: general

Topic: Two is not a cube


view this post on Zulip Ruben Van de Velde (Oct 11 2020 at 12:33):

Is there any easier way to prove this?

lemma two_not_cube {r : } : r ^ 3  2 :=
begin
  rcases r with (rfl|rfl|k),
  {norm_num},
  {norm_num},
  apply ne_of_gt,
  calc 2 < 2 ^ 3 : by norm_num
  ...  (k + 2) ^ 3 : nat.pow_le_pow_of_le_left (nat.le_add_left _ _) _
end

view this post on Zulip Kevin Buzzard (Oct 11 2020 at 13:17):

For me the lemma in the library should be that if f from nat to some ordered thing is monotone, and if f(n) <t<f(n+1) then t is not in the range of f

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:19):

i.e. the philosophy is "generalize"

view this post on Zulip Mario Carneiro (Oct 11 2020 at 13:19):

lemma not_cube {a} (n : ) (h1 : n ^ 3 < a) (h2 : a < (n+1) ^ 3) (r) : r ^ 3  a :=
begin
  cases le_or_lt r n,
  { linarith [nat.pow_le_pow_of_le_left h 3] },
  { linarith [show (n+1)^3  _, from nat.pow_le_pow_of_le_left h 3] },
end

lemma two_not_cube {r : } : r ^ 3  2 :=
not_cube 1 (by norm_num) (by norm_num) r

view this post on Zulip Kevin Buzzard (Oct 11 2020 at 13:20):

There's no pow_n_mono?

view this post on Zulip Mario Carneiro (Oct 11 2020 at 13:20):

nat.pow is oldschool

view this post on Zulip Kevin Buzzard (Oct 11 2020 at 13:21):

Lol

view this post on Zulip Mario Carneiro (Oct 11 2020 at 13:21):

But it's pretty direct from nat.pow_le_pow_of_le_left

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:24):

We should also have a tactic "descends to zmod n and norm_num working in zmod n.

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:25):

what's the n that works for this case?

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:25):

Then the proof would be something like:

begin
  go_mod 4,
  fin_cases r ; norm_num
end

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:25):

I guess 7

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:25):

oh right, 4 also works

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:26):

probably go_mod should also take r as an argument.

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:27):

Or else ask to revert r first.

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:28):

(modified from Mario's code)

import tactic

lemma two_not_cube {r : } : r ^ 3  2 :=
begin
  cases le_or_lt r 2 with h h,
  { revert r, exact dec_trivial },
  { refine ne_of_gt (lt_trans _ $ pow_lt_pow_of_lt_left h _ _); norm_num }
end

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:32):

(Patrick's suggestion)

import tactic data.zmod.basic

lemma two_not_cube {r : } : r ^ 3  2 :=
begin
  intro h,
  apply_fun (coe :   zmod 4) at h,
  norm_cast at h,
  rw nat.cast_pow at h, -- why didn't norm_cast do this?
  generalize_hyp : (r : zmod 4) = r4 at h,
  revert r4, dec_trivial
end

view this post on Zulip Mario Carneiro (Oct 11 2020 at 13:33):

is go_mod a tactic?

view this post on Zulip Kenny Lau (Oct 11 2020 at 13:33):

it's a tactic Patrick's proposed just now

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:33):

Mario, you get to choose the name if you write that tactic.

view this post on Zulip Mario Carneiro (Oct 11 2020 at 13:36):

I have no objections to the name (well..) but I was just double checking that it hadn't been added when I wasn't looking

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:36):

I used "go" because "descend" or "lift" are so controversial here.

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:37):

But it should obviously be "descend".

view this post on Zulip Mario Carneiro (Oct 11 2020 at 13:37):

zmod_bash?

view this post on Zulip Patrick Massot (Oct 11 2020 at 13:37):

That would be the combination of go_mod and fin_cases

view this post on Zulip Kevin Buzzard (Oct 11 2020 at 14:41):

p works iff it's 1 mod 3 and not of the form x^2+27y^2 -- a passing number theorist.

view this post on Zulip Oliver Nash (Oct 11 2020 at 15:53):

I was really hoping this was a question over rather than so that I could suggest this approach.

view this post on Zulip Floris van Doorn (Oct 11 2020 at 23:51):

@Mario Carneiro's not_cube can be easily proven with ne_of_monotone_of_lt_of_lt after #4482 is merged.

view this post on Zulip Floris van Doorn (Oct 11 2020 at 23:53):

Oliver Nash said:

I was really hoping this was a question over rather than so that I could suggest this approach.

r ^ 3 = 1 ^ 3 + 1 ^ 3 has no solutions by FLT, so the same proof appoach still works :)

view this post on Zulip Kevin Buzzard (Oct 12 2020 at 06:18):

Wiles' proof only works for p>=5 because the Frey curve can have torsion when p=3, so really you're relying on something much older (Euler I guess)

view this post on Zulip Ruben Van de Velde (Oct 12 2020 at 07:59):

Not finding a way to do Euler without this fact, though

view this post on Zulip Ruben Van de Velde (Oct 12 2020 at 07:59):

And thanks for the suggestions, everyone!


Last updated: May 13 2021 at 06:15 UTC