Zulip Chat Archive

Stream: new members

Topic: advice on pen+paper maths proof before I create a lean proof


rzeta0 (Jan 30 2025 at 20:31):

I'm doing the MoP Exercise on strong induction - there is only one exercise for that section, ex 6.4.3:

Show that for all natural numbers n>0n>0 , there exist natural numbers  aa and $$$x$, with  xx odd, such that n=2axn=2^{a}x.

Start with a case split on the parity of nn, using the lemma even_or_odd.

I wanted to check that my pen-n-paper maths strategy was correct before I try writing the code:

  • for nn odd we need to show there exists aa and odd xx such that 2ax2^{a}x. This only works if a=0a=0 otherwise 2ax2^{a}x is always even. For the "there exists" we can choose $x=n$ since n is odd.
  • There is no need for induction for the above first case ?!
  • for nn even we need to show there exists aa and odd xx such that [2ax][2^{a}x]. We can't have a=0a=0 because xx is odd and we need 2ax=x2^{a}x=x to be even, but xx is odd. We can use a=2a=2 and choose x=nx=n, which works.
  • Again there was no need for induction for this second case ?!

Clearly I must be deeply in error somewhere?

Edward van de Meent (Jan 30 2025 at 20:34):

if nn is even, choosing a=2a = 2 and x=nx = n results in you needing to prove that n=2ax=22n=4nn = 2 ^ a x = 2 ^ 2 n = 4 n. This is false, so the choices are wrong.

Ruben Van de Velde (Jan 30 2025 at 20:35):

And if nn is even, you can't set xx to be nn anyway, because xx has to be odd

Ruben Van de Velde (Jan 30 2025 at 20:35):

Your argument for nn odd is correct, though

rzeta0 (Jan 30 2025 at 20:35):

silly me !

Ruben Van de Velde (Jan 30 2025 at 20:36):

Maybe it helps to take an example - say n=12n = 12, what are the values for xx and aa?

Edward van de Meent (Jan 30 2025 at 20:40):

(spoiler, these are unique)


Last updated: May 02 2025 at 03:31 UTC