Valuation

[Jim Kingdon]

I'd like to formalize the proof at
https://en.wikipedia.org/wiki/Square_root_of_2#Constructive_proof and
I'm not sure how to tackle the very first step, which is that given
positive integers a and b , ( 2 x. ( b ^ 2 ) ) =/= ( a ^ 2 ) . The proof
given there relies on valuation (highest power of 2 dividing a number):
do we have that concept in set.mm? Or something else which could prove
this lemma? I didn't see anything relevant but I don't really know the
number theory parts of set.mm super well.

Of course this is for iset.mm but if it exists in set.mm it should be
intuitionizable (being about integers and all).

[Thierry Arnoux]

Hi Jim,

I've used this concept in my proof of Euler's partition theorem, see ~oddpwdc.

It states that the function mapping an odd integer `x` and a non-negative integer `y` to ` ( 2 ^ y ) x. x ` is a bijection to the positive integers.

In other terms, any positive integer can be uniquely decomposed into the product of a power of two and an odd integer.

I think that may be what you're looking for.

I'm not sure if this is intuitionizable though (I could not find ~f1od in iset.mm)

BR,
_
Thierry

[Kyle Wyonch]

I was able to find ~f1od in iset.mm.  However for ~oddpwdc, I wasn't able to find ~dvdsle, ~uzsupss, ~supcl, ~fzfi, ~ssfi, ~1dvds, ~divmul2, ~supub, ~dvds0lem, ~mulcanad, ~expne0d, ~divcld, ~dvdsmultr2, ~iddvdsexp.  As well, it would require recreating the four other theorems in Thierry's mathbox: ~nexple, ~f1od2, ~cnvoprab, and ~spc2ed.  It would seem like using this would require a significant amount of library building, all of which may or may not be intuitionizable.

[Jim Kingdon]

Ah, thanks for looking at this in that much detail.

To go down the list of what isn't in iset.mm:

* ~dvdsle , ~1dvds , ~dvds0lem , ~dvdsmultr2, ~iddvdsexp - I had been planning to formalize http://us.metamath.org/mpeuni/df-dvds.html and related theorems and I'm guessing they'll intuitionize. This might be my next project - certainly one I assumed I'd take on before taking up that square root of two is irrational.

* ~uzsupss This, as well as some of the others you couldn't find, is listed at the "Metamath Proof Explorer cross reference" at http://us.metamath.org/ileuni/mmil.html#setmm . The big issue with supremum, even for sets of integers, is.... I guess I can sum it up with http://us.metamath.org/ileuni/nnregexmid.html . Likewise ~supcl and ~supub

* ~fzfi As listed in mmil.html, this is standard intuitionizing of the "add a condition we are within the domain" sort - http://us.metamath.org/ileuni/fzfig.html

* ~ssfi Famously not possible - http://us.metamath.org/ileuni/ssfiexmid.html . But I think we probably can prove the particular set in this proof is finite.

* ~divmul2 , ~mulcanad , ~divcld These are all listed in mmil.html and have equivalents which use "apart from zero" rather than "not equal to zero". The distinction isn't an issue for integers given http://us.metamath.org/ileuni/zapne.html .

* ~expne0d Likewise this exists as http://us.metamath.org/ileuni/expap0d.html

> It would seem like using this would require a significant amount of library building, all of which may or may not be intuitionizable.

Hmm, yeah, I'm in the business of library building but because this looks a bit difficult/large I've put a version of these thoughts into https://github.com/metamath/set.mm/issues/2298 which may be an easier way to keep track of what is done or not done than an email thread.

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/98de7f4c-3e3a-408c-a733-a098e2de8ae2n%40googlegroups.com.