Skip to Content.
Sympa Menu

coq-club - [Coq-Club] What I actually want to enter..

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] What I actually want to enter..


chronological Thread 
  • From: Tambet <qtvali AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] What I actually want to enter..
  • Date: Mon, 19 Jul 2010 06:12:18 +0300
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=aJTLsRyE5Ri6HH4PRiH1PHstNm7rz0idIa1MNocnaQ0ASdhzcCJAppPnDM0xcDocZO Sbry9SlSggkz5sBOrswqZePH6isL5YVCF1exFrPZY65FvQ3zJymNULfmlq3k75s2+5UK 9tN7k05og4WStY9GWErJyTHZQpOfzd4hqmwUA=

I also played with Isabelle and playing with both helped to formalize, what I want to prove. Anyway, I am unable to enter this proof to either of those ...at leas reading this would help you to help me ;) This needs creating some class, defining Collatz sequence next number, "follows" concept and "is followed by 1" concept; also it needs, possibly, a binary analysis of a number?

Thus, the following is what I want to formalize (and check):


fun p(a) = if (p(a) % 2 = 0) then (p(a div 2)) else (a).
The greatest divisor of a, which is power of two = p(a).

I want to show that the number of multiplication-addition series always equals p(a+1) and gives odd result for odd, even result for even and follows the formula (((3/2)**(p(a+1)))*a+1)-1.
This should be trivial by binary analysis.

I want to show that because of this even-odd differentiation, 3n+1 series is never called more than twice in a row. This follows from upper.

I want to show that for any even number, all following even numbers will have p(n) >= a(n) and that when looked from the position of n/2, that will come back to even if n/2 it started with was odd and vice versa, because div2 can't possibly change oddity of any upper level.

Thus, starting from even it leads to odd (next number) and starting from odd it leads to even (smaller number). Modulus is built in such way that p(n) for each even number is p(n)+1 related to it's division by two and this p(n) is how many times it will be divided by two, thus p(n) for any following even is big enough to lead to smaller number (n/2+1 for next one, as numbers grow, also this p(n) grows and thus, even leads to following(n)<=n+1).

I want, thus, to show that the sequence always eventually leads to smaller number than it started from or 1.


Python check for those claims for first 100000 numbers (or just make the constant larger) is available.

Tambet



Archive powered by MhonArc 2.6.16.

Top of Page