コラッツ予想がとけたらいいな

**１３２人目の素数さん** · 2012/10/14(日) 10:32:39.71

525 名前：１３２人目の素数さん[sage] 投稿日：2012/09/03(月) 18:24:27.22
http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。

**righ1113** ◆OPKWA8uhcY · 2016/06/26(日) 23:31:32.04

110101101011は除外出来ない事が分かりました。
そこで証明を次のように修正します。

12区切りのライトエッジパターンに110101101011が現れたとする。
末尾は1なので、次の12区切りは先頭が0である。
「先頭が1」「2連続の0」「3連続の1」「1,1,0,1,1」を除外した、12区切りで1が7個入るパターンは、
次の6つしかない。（Haskellで確認済み）

[0,1,0,1,0,1,1,0,1,0,1,1]
[0,1,0,1,1,0,1,0,1,0,1,1]
[0,1,1,0,1,0,1,0,1,0,1,1]
[0,1,1,0,1,0,1,1,0,1,0,1]
[0,1,1,0,1,0,1,0,1,1,0,1]
[0,1,0,1,1,0,1,0,1,1,0,1]

1~3個目は11で終わっているため、次の12区切りも0始まりとなってループする。
再び110101101011が来る余地は無い。
4~6個目は、次の12区切りで1始まりが可能なので、さらに調べる。

**righ1113** ◆OPKWA8uhcY · 2016/06/26(日) 23:35:20.57

「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した、12区切りで1が7個入るパターンは、
次の8つしかない。（Haskellで確認済み）

[1,0,1,0,1,0,1,0,1,0,1,1]
[1,0,1,0,1,0,1,1,0,1,0,1]
[1,0,1,0,1,1,0,1,0,1,0,1]
[1,0,1,1,0,1,0,1,0,1,0,1]
[1,0,1,0,1,0,1,0,1,1,0,1]
[1,0,1,1,0,1,0,1,1,0,1,0]
[1,0,1,1,0,1,0,1,0,1,1,0]
[1,0,1,0,1,1,0,1,0,1,1,0]

1個目は11で終わっているため、次の12区切りも0始まりとなってループする。
2~5個目は1で終わっているため、次の12区切りも1or0始まりとなってループする。
6,7個目は、連続して並べると、
110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,1,0,1,0,1,1,0,1,0]
110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,1,0,1,0,1,0,1,1,0]
となって「1,1,0,1,1」が現れるので除外される。
8個目は、連続して並べると、
110101101011 [0,1,*,*,*,*,*,*,*,1,0,1] [1,0,1,0,1,1,0,1,0,1,1,0] 110101101011
となって「1,1,0,1,1」が現れるので110101101011にはならない。
よって、二回以上110101101011が現れることはない。

初期値をX0 とy0B * 2^(py0+2)（1ずらし→2ずらし）から始めれば、
Xs はysB * 2^(pys+2) を超えないので、Xs < ysB * 2^(pys+2) である。

さて、これをCoqでどうやってやろう……