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

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

[前50を表示]
400:￥ ◆2VB8wsVUoo
16/05/24 22:59:49.43 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

401:￥ ◆2VB8wsVUoo
16/05/24 23:00:06.58 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

402:￥ ◆2VB8wsVUoo
16/05/24 23:00:23.53 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

403:￥ ◆2VB8wsVUoo
16/05/24 23:00:41.20 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

404:￥ ◆2VB8wsVUoo
16/05/24 23:00:58.88 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

405:￥ ◆2VB8wsVUoo
16/05/24 23:01:17.09 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

406:￥ ◆2VB8wsVUoo
16/05/24 23:02:01.29 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

407:￥ ◆2VB8wsVUoo
16/05/24 23:02:18.83 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

408:￥ ◆2VB8wsVUoo
16/05/24 23:17:55.21 98ujCcPg.net
￥

409:￥ ◆2VB8wsVUoo
16/05/24 23:18:14.02 98ujCcPg.net
￥

410:tai
16/05/24 23:38:41.03 374dBI4a.net
一応直しておきました
まだ途中ですので
まちがっているかもしれません

411:￥ ◆2VB8wsVUoo
16/05/24 23:54:36.02 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

412:￥ ◆2VB8wsVUoo
16/05/24 23:54:53.79 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

413:￥ ◆2VB8wsVUoo
16/05/24 23:55:08.89 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者　増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>

414:righ1113 ◆OPKWA8uhcY
16/05/25 20:06:38.89 EB6pp118.net
まだCoq練習フェーズです。
Theorem m11_isnot_prime01:
forall (P Q R :Prop), (P->Q) -> (Q->R) -> (~R->~Q).
(* proof. *)
intros.
cbv.
intro.
cbv in H1.
apply H0 in H2.
apply H1 in H2.
apply H2.
Qed.
Theorem m11_isnot_prime01':
forall (P Q R :Prop), (P->Q) -> (Q->R) -> (~R->~Q).
(* proof. *)
intro.
intro.
intro.
intro.
auto.
Qed.
Theorem m11_isnot_prime02:
forall (Q R :Prop), (Q->R) -> (~R->~Q).
(* proof. *)
auto.
Qed.
Theorem m11_isnot_prime03:
forall (P Q R :Prop), (P=Q) -> (P->R) -> (Q->R).
(* proof. *)
intros.
rewrite H in H0.
apply H0 in H1.
apply H1.
Qed.

415:righ1113 ◆OPKWA8uhcY
16/05/31 13:18:55.66 MldWQZrV.net
やったーカリーのパラドックスが解けたよー
Lemma l1:
forall (X Y Z:Prop), (X->X->Y) -> X=(X->Y) -> X.
Proof.
intros.
rewrite H0.
intro.
apply H in H1.
apply H1.
apply H1.
Qed.
Theorem curry's_paradox:
forall (X Y:Prop), X=(X->Y) -> Y.
Proof.
intros.
assert(X->X).
auto.
pattern X at 2 in H0.
rewrite H in H0.
apply (l1 X Y) in H0.
pose H0.
rewrite H in x.
apply x in H0.
apply H0.
apply X.
apply H.
Qed.

416:righ1113 ◆OPKWA8uhcY
16/05/31 13:46:31.08 MldWQZrV.net
Zいらないっすね。
Lemma l1:
forall (X Y:Prop), (X->X->Y) -> X=(X->Y) -> X.
Proof.
intros.
rewrite H0.
intro.
apply H in H1.
apply H1.
apply H1.
Qed.
Theorem curry's_paradox:
forall (X Y:Prop), X=(X->Y) -> Y.
Proof.
intros.
assert(X->X).
auto.
pattern X at 2 in H0.
rewrite H in H0.
apply (l1 X Y) in H0.
pose H0.
rewrite H in x.
apply x in H0.
apply H0.
apply H.
Qed.

417:１３２人目の素数さん
16/05/31 16:43:04.58 Q9drQ/Ad.net
なかなか頑張ってますな。
正直すぐ投げ出すんじゃないかと侮っていたよ。

418:righ1113 ◆OPKWA8uhcY
16/05/31 23:37:09.87 5ZwDxW8h.net
証明で詰まると苦しいけど、
Coqで証明できると楽しいです。

419:righ1113 ◆OPKWA8uhcY
16/06/04 21:52:45.29 1pZXMfoL.net
のんびりと、Coqでのコラッツ予想検証に取り掛かりたいと思います。
>>322の僕の証明の流れは、次のようになっています。
1.イントロダクション
2.コラッツパターンXsの定義
3.左端を伸ばすパターンYsの定義
4-1.コラッツパターンと左端を伸ばすパターンのずれを定義する
4-2.シミュレーションA－xsAを定義する
4-3.シミュレーションB－ysBを定義する
4-4.[log Xs] - [log Ys] <= [log(xsA * 2^pxs)] - [log(ysB * 2^pys)]
　　　　　を証明する　（この式の右辺が有限値なら、コラッツパターンと左端を伸ばすパターンのずれも有限値となる。）
5.ずれが有限という仮定で、コラッツ予想で4-2-1以外のLoopがない事を証明する
6.ずれが有限という仮定で、コラッツ予想で無限大に発散する数がない事を証明する
7.　4-4の右辺が有限値であることを、Haskellで証明する
「繰り上がりがあったりなかったりするから」とか、図から補題を証明していたりするので、
全てをCoqで検証・証明するのは難しいと考えています。
まずは4-4からやっていこうと思います。

420:righ1113 ◆OPKWA8uhcY
16/06/04 22:01:11.07 1pZXMfoL.net
4-4その１
前提として、コラッツパターンXsよりシミュレーションAが大きい、というのがあります。
理由は、コラッツパターンの下位からの繰り上がりがあったりなかったりするのに対して、
シミュレーションAは、常に下位からの繰り上がりがあるからです。
なので、pxs=log Xs - bit + aが成り立つのですが、前述の理由によりa>=0です。
（これは>>322には書いてないです。Coqで証明するために変えました。）
という訳でCoqでの証明です。
Require Import Omega.
Theorem Xs_ge_xsA:
forall (Xs a bit pxs xsA: nat), 0<xsA -> 0<=pxs
-> Nat.log2 Xs +1 <= Nat.log2 Xs +1 +a
-> pxs = Nat.log2 Xs +1 -bit +a
-> bit = Nat.log2 xsA +1
-> Nat.log2 Xs +1 <= Nat.log2 (xsA*(2^pxs)) +1.
Proof.
intros.
rewrite (Nat.log2_mul_pow2 xsA pxs).
all: cycle 1.
apply H.
apply H0.
rewrite H2.
rewrite H3.
omega.
Qed.
これで、コラッツパターンよりシミュレーションAが大きいという事実のもとで、
[log Xs] <= [log xsA*(2^pxs)]が示せました。

421:righ1113 ◆OPKWA8uhcY
16/06/04 22:03:58.52 1pZXMfoL.net
4-4その２
前提として、シミュレーションBより左端を伸ばすパターンが大きい、というのがあります。
理由は、左端を伸ばすパターンの下位からの繰り上がりがあったりなかったりするのに対して、
シミュレーションBは、常に下位からの繰り上がりがないからです。
なので、pys=log Ys - bit - aが成り立つのですが、前述の理由によりa>=0です。
（これは>>322には書いてないです。Coqで証明するために変えました。）
という訳でCoqでの証明です。こちらはZ_scopeで証明しています。
Require Import Omega.
Open Scope Z_scope.
Theorem ysB_ge_Ys:
forall (Ys a bit pys ysB:Z), 0<ysB -> 0<=pys
-> Z.log2 Ys +1 -a <= Z.log2 Ys +1
-> pys = Z.log2 Ys +1 -bit -a
-> bit = Z.log2 ysB +1
-> Z.log2 (ysB*(2^pys)) +1 <= Z.log2 Ys +1.
Proof.
intros.
rewrite (Z.log2_mul_pow2 ysB pys).
all: cycle 1.
apply H.
apply H0.
rewrite H2.
rewrite H3.
omega.
Qed.
Open Scope nat_scope.
これで、シミュレーションBより左端を伸ばすパターンが大きいという事実のもとで、
[log ysB*(2^pys)] <= [log Ys]が示せました。
Ys<=Xsは自明なので、
よって[log Xs] - [log Ys] <= [log(xsA * 2^pxs)] - [log(ysB * 2^pys)]となります。
4-4は以上になります。

422:righ1113 ◆OPKWA8uhcY
16/06/05 18:56:49.96 yXCfmuqW.net
次に7.をやろうと思います。>>231-240あたりです。
ビット数はbit=10です。
xsAの0ステップ目を1111111111、ysBの0ステップ目を0000000001として
（ずれが0で一番差が開いている数）ステップを重ねると、
xsAは115ステップ目が3ステップ目と一致して以後繰り返しになります。
xsBは93ステップ目が3ステップ目と一致して以後繰り返しになります。
その区間の最上位繰り上がりの可否を、大きい繰り返しになるまで調べます。
Haskellでやった時は、ずれの最大値は2でした。
Coqはこれからやります。

423:righ1113 ◆OPKWA8uhcY
16/06/07 16:41:02.76 MtRwR70U.net
微妙にステップ数が違ってました。
xsAの0ステップ目を1111111111、ysBの0ステップ目を0000000001として　
（ずれが0で一番差が開いている数）ステップを重ねると、　
xsAは113ステップ目が2ステップ目と一致して以後繰り返しになります。　
xsBは91ステップ目が2ステップ目と一致して以後繰り返しになります。　
colPattAの第二要素でHaskellとCoqでdiffを取ったので大丈夫だと思います。

424:righ1113 ◆OPKWA8uhcY
16/06/07 16:45:19.93 MtRwR70U.net
Coqですが、関数定義は省略します。Haskellのとそんなに変わらないです。
Theorem colPattA_2_eq_113:
last (iterate 2 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0))
= last (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)).
Proof.
compute.
reflexivity.
Qed.
Theorem colPattB_2_eq_91:
last (iterate 2 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0))
= last (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)).
Proof.
compute.
reflexivity.
Qed.
これで小さい繰り返しはクリアできました。

425:righ1113 ◆OPKWA8uhcY
16/06/07 20:12:15.58 MtRwR70U.net
なんかうまくいきません。
ずれが際限なく増えていきます。

426:１３２人目の素数さん
16/06/07 20:14:39.10 KJBV85MD.net
頑張って修正するんだっ

427:righ1113 ◆OPKWA8uhcY
16/06/07 21:33:31.73 MtRwR70U.net
>>409
ありがとうございます。がんば�

428:閧ﾜす。

429:righ1113 ◆OPKWA8uhcY
16/06/07 22:06:33.54 MtRwR70U.net
なんとかできました。
colPattAは繰り返しの項数が111、colPattBは繰り返しの項数が89です。
colPattA*89=9879項、colPattB*111=9879項にして大きい繰り返しにします。
倍の19758項も用意しておきます。
これを初期ずれx=1、x+colPattA-colPattB < 定数　かを9879項、19758項調べるのですが、
途中colPattBが勝ってxが負になる可能性があるので、初期ずれx=2とします。
Definition colPattA2nd_1 : list nat :=
cycle 89 nil
(tail (tail (tail (map snd (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)))))).
Definition colPattA2nd_2 : list nat :=
cycle (89*2) nil
(tail (tail (tail (map snd (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)))))).
Definition colPattB2nd_1 : list nat :=
cycle 111 nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).
Definition colPattB2nd_2 : list nat :=
cycle (111*2) nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).

430:righ1113 ◆OPKWA8uhcY
16/06/07 22:32:18.95 MtRwR70U.net
やっぱだめかも……

431:１３２人目の素数さん
16/06/07 23:18:10.94 KJBV85MD.net
逆に証明を突き詰めていったら反例がみつかったなんてこともあるかもね。
それならそれで面白いが。

432:righ1113 ◆OPKWA8uhcY
16/06/08 00:37:23.48 JADn1FP5.net
>>231-240の通り、手計算ではうまくいくんです。
それをCoqに落とし込むのに手間取っています。

433:righ1113 ◆OPKWA8uhcY
16/06/08 02:03:36.44 JADn1FP5.net
>>411は無しでお願いします。
>>236-237を見て、colPattA*5=555項、colPattB*6=534項にして大きい繰り返しにします。
この区間のずれの最大値が2、末項が1になったので、大きい繰り返しを何度繰り返しても、ずれは2以下です。
Definition colPattA2nd : list nat :=
cycle 5 nil
(tail (tail (tail (map snd (iterate 113 colPattA ((1::1::1::1::1::1::1::1::1::1::nil),0)))))).
Definition colPattB2nd_1 : list nat :=
cycle 1 nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).
Definition colPattB2nd_2 : list nat :=
cycle 6 nil
(tail (tail (tail (map snd (iterate 91 colPattB ((0::0::0::0::0::0::0::0::0::1::nil),0)))))).
Theorem p_misalignment_first:
misalignment_max_last 1 1 colPattA2nd colPattB2nd_1 = (2, 1).
Proof.
compute.
reflexivity.
Qed.
Theorem p_misalignment_second:
misalignment_max_last 1 1 colPattA2nd colPattB2nd_2 = (2, 1).
Proof.
compute.
reflexivity.
Qed.
7.もできました。

434:righ1113 ◆OPKWA8uhcY
16/06/08 09:39:08.70 JADn1FP5.net
やっぱりうまくいってないみたいです。
>>236-237の手計算も間違っていました。
ビット数を増やすという切り札があるので、それをやってみます。
Coqはウソつかないんですねー

435:413
16/06/08 21:39:10.48 lYAR2M8u.net
俺は>>1が>>1証明のほころびからコラッツ予想の反例を見つけるというストーリーを期待しているｗ

436:１３２人目の素数さん
16/06/08 22:23:08.13 WkHIclqp.net
ブールピタゴラス問題も真っ青の反例ループのサイズが200TB超えとかを希望w

437:righ1113 ◆OPKWA8uhcY
16/06/08 23:36:44.69 aPj7A/ik.net
ビット数を増やしても、ずれが際限なく増えていく～～

438:１３２人目の素数さん
16/06/09 02:17:55.30 Z2BPqjfW.net
ずれの計算では上手く行くわけがないって、ずっと前に指摘されてたじゃん。
何をいまさら。こんなやり方でコラッツの予想が解けるわけがない。

439:１３２人目の素数さん
16/06/09 19:53:16.16 OutW5kLL.net
仮にずれの計算でうまくいかなかったとしても>>1は修正してくるだろう。
Coqがあれば間違った証明は通らないだろうしいくらでも頑張れる環境がある。
コラッツの予想が解けるのは時間の問題だな。

440:righ1113 ◆OPKWA8uhcY
16/06/10 05:50:42.64 oOXw5TlH.net
まだ思いつきのレベルなんであれですが……
5bitで考えて、さらに命題を一つ考えます。
（★）「下位からの繰り上がりは、2ステップ連続では起こらない」
これでcollatzPatternA2とBを計算すると、Loopが両方とも7項で4繰り上がりになって、
いくら繰り返してもずれは増大しません。
*CollatzPatt> collatzPatternA2 繰り上がりなし、あり、なし、あり、……
[([1,1,1,1,1],0,0),([1,1,1,0,1],1,1),([1,0,0,0,1],1,0),([1,0,0,1,1],0,1),([1,1,0,0,1],1,0),([0,0,1,1,1],0,1),([1,0,1,0,1],1,0),([1,1,1,1,1],0,1)]
*CollatzPatt> map snd3 collatzPatternA2
[0,#1,1,0,1,0,1,0]
*CollatzPatt> collatzPatternB
[([0,0,0,0,1],0),([0,0,0,1,1],0),([0,1,0,0,1],1),([1,1,0,1,1],0),([0,0,1,0,1],1),([0,1,1,1,1],0),([0,1,1,0,1],1),([0,0,0,0,1],1)]
*CollatzPatt> map snd collatzPatternB
[0,#0,1,0,1,0,1,1]
まだHaskellなのはご容赦を。

441:１３２人目の素数さん
16/06/11 01:05:42.63 p56I7Lto.net
CoqよりHaskellのほうが書きやすいのか。
どっちも難しそうだが。

442:righ1113 ◆OPKWA8uhcY
16/06/11 03:48:47.75 6GM2rdQN.net
単純に僕のCoq歴が3週間、Haskell歴が5年くらいだからだと思います。

443:１３２人目の素数さん
16/06/11 18:00:38.27 p56I7Lto.net
Haskell　5年もやってんのか凄いな。
5年間で何行くらいHaskellでコード書いたの？

444:righ1113 ◆OPKWA8uhcY
16/06/11 20:46:46.40 6GM2rdQN.net
Haskellはコード量が短くすむこともあって、
5年間で2000～3000行ぐらいじゃないでしょうか。

445:１３２人目の素数さん
16/06/11 20:59:42.80 p56I7Lto.net
100行のプログラム20～30本書いてるってことか
なかなか大したもんだ。

446:righ1113 ◆OPKWA8uhcY
16/06/13 02:40:18.56 6i9eMAsV.net
大幅に証明を変えます。
左端を伸ばすパターンYs=x0(3/2)^sに対して、Zs=2^p(3/2)^sを考えます。
ここで2^pは、x0と右端を揃えるものです。
例えば、2進数でx0=11001なら、2^p=00001となります。
2^p < x0なので、Zs < Ysが言えます。
Ys <= コラッツパターンXsは自明です。
x0=11001なら、y0B=11111で、pysはx0と右端を揃えるものです。
X0とy0Bは1ずれた状態からスタートします。
ysBの繰り返しは8bitでおこなって[1,1,#0,1,0,1,1,0,1,0,1,0,1,1]です。12ステップ中7個が1です。
Xsの先頭2ステップは最大で1,1ですから、2ステップ目でX2とy2Bのずれは1以上です。
次に、Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
よってXsはysB*2^(pys+1)を超えないので、Xs < ysB*2^(pys+1)です。
（初期値11111） < （初期値000001）
ysB*2^(pys+1) < 2^(p+2)(3/2)^sが言えます。図参照。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)
2^(p+2)(3/2)^s < 2*2^(p+2)(3/2)^sなので、ysB*2^(pys+2) < 8Zsです。
まとめると、Zs < Ys <= Xs < ysB*2^(pys+1) < 8Zsとなります。
Zsと8Zsのずれは3で、これがずっと変わらないです。
よって、YsとXsのずれも3以下に押さえられる事になります。
(※)は後で書きます。

447:righ1113 ◆OPKWA8uhcY
16/06/13 05:34:28.73 6i9eMAsV.net
×　（初期値11111）　<　（初期値000001）
○　（初期値011111） < （初期値0000001）

448:righ1113 ◆OPKWA8uhcY
16/06/13 09:53:52.64 6i9eMAsV.net
Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
まずは補題から。
・2連続の0は無い。　0.585+0.585=1.135より、必ず1繰り上がるから
・3連続の1は無い。
・1,1,0,1,1パターンは無い。
1つ前　　　　　　　　1,　　　　　1,　　　　　　0,　　　　　　　1,　　　　　　　1
.415~.999 .000~584
　　　　　　　　.000~414は脱落
.830~.999 .415~584 .000~.169 .585~.754 .170~.339 全部脱落
　　　　　　　　　　　　　　　　　　　　　　　　　（↑3連続の1は無い事も分かる）

449:righ1113 ◆OPKWA8uhcY
16/06/13 09:57:29.37 6i9eMAsV.net
次に、8個1/12ステップの[0,0,0,0,1,1,1,1,1,1,1,1]の全ての順列に対して、上3つを除外します。
またもやHaskellですwww
import Data.List (permutations, nub)
cycleN :: Int -> [Int] -> [Int] -> [Int]
cycleN 0 la _ = la
cycleN x la lb = cycleN (x-1) (la++lb) lb
remove_0_0 :: [Int] -> Bool
remove_0_0 [_] = True
remove_0_0 (0:0:xs) = False
remove_0_0 (_:x1:xs) = remove_0_0 (x1:xs)
remove_1_1_1 :: [Int] -> Bool
remove_1_1_1 [_,_] = True
remove_1_1_1 (1:1:1:xs) = False
remove_1_1_1 (_:x1:x2:xs) = remove_1_1_1 (x1:x2:xs)
remove_1_1_0_1_1 :: [Int] -> Bool
remove_1_1_0_1_1 [_,_,_,_] = True
remove_1_1_0_1_1 (1:1:0:1:1:xs) = False
remove_1_1_0_1_1 (_:x1:x2:x3:x4:xs) = remove_1_1_0_1_1 (x1:x2:x3:x4:xs)
*CollatzPatt> let multi=filter remove_1_1_1 $ filter remove_0_0 $
nub $ permutations [0,0,0,0,1,1,1,1,1,1,1,1]　←1時間ぐらいかかる
*CollatzPatt> filter remove_1_1_0_1_1 $ filter remove_1_1_1 $ map (cycleN 2 []) multi
[]
空リストになったので、(※)が証明できました。

450:righ1113 ◆OPKWA8uhcY
16/06/14 09:36:32.33 GDyexPn/.net
Xsを12ステップで区切った時、8個以上1が入る事はありません。(※)
Coq版できました。
ただnub permutationsの部分がCoqでは12時間計算しても終わらなかったので、
そこだけHaskellで495行出力して（それでも1時間かかる）、permu.vに書いています。
permu.v
Require Import List.
Definition nub_permu: list (list nat) :=
((0::0::0::0::1::1::1::1::1::1::1::1::nil)::
(1::0::0::0::0::1::1::1::1::1::1::1::nil)::
---略---
(1::1::1::1::1::0::1::0::0::1::1::0::nil)::
(1::1::1::1::1::1::0::0::0::1::1::0::nil)::nil).

451:righ1113 ◆OPKWA8uhcY
16/06/14 09:41:24.87 GDyexPn/.net
collatz06.v
Require Import Omega.
Require Import List.
Require Import Coq.Program.Wf.
Require Import permu.
Fixpoint cycle{A} (n:nat) (la:list A) (lb:list A) :list A :=
match n with
| 0 => la
| S m => cycle m (app la lb) lb
end.
Fixpoint remove_0_0 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| 0::0::_ => false
| l1::ls => remove_0_0 ls
end.
Fixpoint remove_1_1_1 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| _::_::nil => true
| 1::1::1::_ => false
| l1::ls => remove_1_1_1 ls
end.
Fixpoint remove_1_1_0_1_1 (l:list nat): bool :=
match l with
| nil => true
| _::nil => true
| _::_::nil => true
| _::_::_::nil => true
| _::_::_::_::nil => true
| 1::1::0::1::1::_ => false
| l1::ls => remove_1_1_0_1_1 ls
end.

452:righ1113 ◆OPKWA8uhcY
16/06/14 09:46:24.20 GDyexPn/.net
Fixpoint beq_list (l:list nat) (m:list nat): bool :=
match l,m with
| nil, nil => true
| nil, _ => false
| _, nil => false
| l1::ls, m1::ms => if beq_nat l1 m1 then beq_list ls ms else false
end.
Fixpoint elem (x:list nat) (l:list (list nat)): bool :=
match l with
| nil => false
| l1::ls => if beq_list x l1 then true else elem x ls
end.
Fixpoint nub (l:list (list nat)): list (list nat) :=
match l with
| nil => nil
| l1::ls => (if elem l1 ls then nil else (l1::nil)) ++ (nub ls)
end.
Definition bnt_nat (x:nat) (y:nat): bool :=
if beq_nat x y then false else true.
Fixpoint concatMap (f:nat->list (list nat)) (l:list nat): list (list nat) :=
match l with
| nil => nil
| l1::ls => (f l1) ++ concatMap f ls
end.
Fixpoint replace (x y:nat) (l m:list nat): list nat :=
match m with
| nil => l
| m1::ms => if beq_nat x m1 then replace x y (y::l) ms else replace x y (m1::l) ms
end.
Program Fixpoint permutations (l:list nat) (cnt:nat) {measure cnt}: (list (list nat)) :=
match cnt with
| 0 => ((nil)::nil)
| _ =>
match l with
| nil => ((nil)::nil)
| ls => concatMap (fun x => (map (fun y => x::y) (permutations (filter (bnt_nat x) ls) (cnt-1)))) ls
end
end.
Next Obligation.
omega.
Qed.

453:righ1113 ◆OPKWA8uhcY
16/06/14 09:49:36.01 GDyexPn/.net
Definition multi1: list (list nat) :=
filter remove_1_1_1
(filter remove_0_0
(* (nub (map (replace 2 0 nil)
(map (replace 3 0 nil)
(map (replace 4 0 nil)
(map (replace 5 1 nil)
(map (replace 6 1 nil)
(map (replace 7 1 nil)
(map (replace 8 1 nil)
(map (replace 9 1 nil)
(map (replace 10 1 nil)
(map (replace 11 1 nil)
(permutations (0::1::2::3::4::5::6::7::8::9::10::11::nil) 12)))))))))))) *)
nub_permu).
Definition multi2: list (list nat) :=
filter remove_1_1_0_1_1 (filter remove_1_1_1 (map (cycle 2 (nil)) multi1)).
Theorem multi2_is_nil:
multi2 = nil.
Proof.
compute.
reflexivity.
Qed.
やっぱQed.が通ると気持ちが良いですね。

454:righ1113 ◆OPKWA8uhcY
16/06/14 17:28:23.76 GDyexPn/.net
pdf修正しました。
まだpre版で、日本語と英語が混ざってて気持ち悪いですが、
良かったら見てみてください。
URLﾘﾝｸ(drive.google.com)

455:１３２人目の素数さん
16/06/14 20:06:46.34 mUIjFDF1.net
俺じゃ理解できないけどどうやら進んでるようで、おめ

456:righ1113 ◆OPKWA8uhcY
16/06/15 22:55:25.35 s5Jlp8vN.net
ありがとうございます。

457:righ1113 ◆OPKWA8uhcY
16/06/19 03:31:16.15 HPZ4uwl5.net
ちょっとは読みやすくなったと思います。
URLﾘﾝｸ(drive.google.com)
-----
「ライトエッジパターン」というものを定義する。
これは、右端が繰り上がった時は1、そうでない時は0を置くものである。
x=319のライトエッジパターンは、[-,0,1,1,0,1,0,1,1,0,1,0,1,0,1,1,0,1,1]である。
-----

458:１３２人目の素数さん
16/06/19 05:13:52.50 R9PbWXF5.net
>>1
コラッツパターンとかライトエッジパターンとかよくわからん。
もし余力があればideoneにプログラム上げてくれんか？
好きな数を入力してそれに対してそのパターンを出力してほしい。
URLﾘﾝｸ(ideone.com)
haskellも選べるからたぶんもうすでに書いたものがあるだろ？

459:righ1113 ◆OPKWA8uhcY
16/06/19 06:49:14.93 HPZ4uwl5.net
Excelマクロでも良いですか？
URLﾘﾝｸ(drive.google.com)
A列に10進数で数を入れて、「計算」ボタンを押すと、
B列にライトエッジパターンが、
C列からにコラッツパターンが表示されます。
ideoneはよく分かりませんでした。 <

460:righ1113 ◆OPKWA8uhcY
16/06/19 06:55:07.24 HPZ4uwl5.net
あ、ダウンロードして使って下さいね。

461:１３２人目の素数さん
16/06/19 08:36:15.00 R9PbWXF5.net
エクセルマクロはうごきました。
サンクス。
左端がどう決まってるのかいまいち分かってないんだけど
２で割れた回数とかだよね？
>>439のは英語だったからいまいち自信がもてない。

462:righ1113 ◆OPKWA8uhcY
16/06/19 12:31:44.57 o4I0V/Mj.net
コラッツパターンの左側は、
コラッツ操作で＜2で割った回数-1＞を蓄積しているものです。
>>172にもあります。
（マクロやpdfでは0を書いてないけど）

463:１３２人目の素数さん
16/06/20 20:49:50.82 AO/P2Y9A.net
左端を伸ばすパターンの説明で
3. Becomes the next x from the left end of the 1 to 1 on the right.
てのがあるんだけど、どう訳せばいいのかよくわからんｗ
教えて～

464:righ1113 ◆OPKWA8uhcY
16/06/20 22:36:36.36 IBPpfU1W.net
「次のxとして、左端の1から右端の1までを取る」という意味です。
_111111001　=x0が
1011110111　=x1になった時、
x1は左端の1から右端の1までを取るね、という事です。
実は英語は苦手で、いつも赤点でしたwww

465:righ1113 ◆OPKWA8uhcY
16/06/21 06:10:35.56 pnfuA33J.net
>>439を更新しました。

466:righ1113 ◆OPKWA8uhcY
16/06/21 14:05:46.27 w+gnd+8K.net
今日扇風機を出しました。すずしいです。

467:１３２人目の素数さん
16/06/21 20:10:09.84 shTmSKB6.net
まだ理解できてないが左端を伸ばすパターンもエクセルマクロあるの？
あるならオクレ。

468:righ1113 ◆OPKWA8uhcY
16/06/21 20:18:58.92 w+gnd+8K.net
左端を伸ばすパターンは数が左に伸びるのと、
ステップが無限に続くので、作れてないです。すみません。

469:１３２人目の素数さん
16/06/21 20:27:44.17 shTmSKB6.net
ないのか、残念。
まあしょうがない。

470:１３２人目の素数さん
16/06/21 21:05:09.09 shTmSKB6.net
んー左に伸ばすパターンって出力のサイズを制限したらプログラム書ける？
制限しても難しい？

471:righ1113 ◆OPKWA8uhcY
16/06/21 21:34:19.98 w+gnd+8K.net
ちょっとやってみます。
気長にお待ちください。

472:１３２人目の素数さん
16/06/21 21:48:26.05 shTmSKB6.net
すまんね、クレクレ言って。

473:righ1113 ◆OPKWA8uhcY
16/06/22 06:06:53.11 kg3XYDgA.net
URLﾘﾝｸ(drive.google.com)
A列に10進数で数を入れて、「計算」ボタンを押すと、
B列にコラッツパターンのライトエッジパターンが、
C列に左端を伸ばすパターンのライトエッジパターンが、
D列からにコラッツパターンと左端を伸ばすパターンが表示されます。
B,C列で色が変わっている所は、コラッツパターンと左端を伸ばすパターンの右端がずれている所です。
大きい数を入れると「列が足りない」エラーが出るかもしれませんが、
Excel2007以降を使っているならば、Officeボタンから「変換」を選んで開きなおすと、
最大列が256列から16384列になります。

474:成清愼
16/06/22 18:39:08.04 dJB43qU2.net
以前より進化しました。
諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。
URLﾘﾝｸ(koubeichizoku.ix-web.tk)

475:１３２人目の素数さん
16/06/22 20:08:21.63 3ACjIS1K.net
>>455
おおう、乙カレ。やるね。
左端を伸ばすパターンの正体がいまいちわかってないんだけどどういう思想で出来たものなの？
説明できるなら説明クレクレ。

476:１３２人目の素数さん
16/06/22 20:25:08.09 3ACjIS1K.net
333入れたら結果が出てこなかったんだが？
なんか制限とかあるんだっけ？
よくわかってなくてスマン。

477:righ1113 ◆OPKWA8uhcY
16/06/22 20:27:44.55 SAQFF6Ga.net
コラッツ予想を2進数で考える、というのは前々からあって、
コラッツパターンを見出した時に、最後のルール
「最後に、左端に+1する」
を外したら面白いんじゃね、と思って左端を伸ばすパターンが出来ました。
まあ、偶然の産物ですね。

478:righ1113 ◆OPKWA8uhcY
16/06/22 20:32:36.93 SAQFF6Ga.net
>>458
自分の環境では出てきます。
・マクロを有効にする
・数字を入れた後一回Enterを押して、カーソルを合わせ直して実行する
あたりを試してみてください。

479:１３２人目の素数さん
16/06/22 20:39:44.54 3ACjIS1K.net
>>460
でました。
カーソル合わせてなかったのかな？多分。

480:１３２人目の素数さん
16/06/22 20:55:10.79 3ACjIS1K.net
あとは論文を読むだけか
読めるかな～

481:１３２人目の素数さん
16/06/22 21:22:24.14 3ACjIS1K.net
ライトエッジを１２個づつに区切ったとき８個以上１が入らないことが言えると
なぜコラッツ予想が証明されたことになるの？
今はそこで悩んでる。

482:１３２人目の素数さん
16/06/22 21:31:10.84 3ACjIS1K.net
左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの？
やっぱまだよくわからん。

483:righ1113 ◆OPKWA8uhcY
16/06/22 22:01:29.56 SAQFF6Ga.net
>>463
X0とy0B*2^(py0+1)は右端が1ずれた（y0Bが大きい）状態からスタートします。
y0Bの12区切りのライトエッジパターンは1が7個はいっていて、
もしX0の12区切りのライトエッジパターンに1が8個以上入らなければ、初期値の1ずれがずっと維持されるので、
X0 < y0B*2^(py0+1)が言えるわけです。
これ自体でコラッツ予想は証明されないです。

484:righ1113 ◆OPKWA8uhcY
16/06/22 22:05:31.40 SAQFF6Ga.net
>>464
＞左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの？
次のセクションで、ずれが有限であることを利用して、
「5 there is no loop other than 4-2-1 in Collatz conjecture」
「6 Collatz conjecture is not the number that diverges to infinity」
で、「コラッツ予想に4-2-1以外のLoopがない」「コラッツ予想で無限大に発散する数はない」
事を個別に証明しています。

485:righ1113 ◆OPKWA8uhcY
16/06/22 22:11:13.67 SAQFF6Ga.net
>>465
2個目のX0 < y0B*2^(py0+1)は間違いで
Xs < ysB*2^(pys+1)
です。

486:righ1113 ◆OPKWA8uhcY
16/06/23 05:02:38.13 ta0z2vBC.net
最新版のpdfをご覧ください。
URLﾘﾝｸ(drive.google.com)

487:１３２人目の素数さん
16/06/23 21:56:11.47 tqdQH9fb.net
>>1
頑張ってもらってるのにスマンが俺の頭じゃいまいち理解が追いつかない。
面白そうではあるんだけど。
まあ、ボチボチ読んでみます。

488:１３２人目の素数さん
16/06/23 22:55:11.53 tqdQH9fb.net
５章の（１４）（１５）の式なんだけど
By the product of the loop 1 cycle X
X x X x X ...
It will be but , X > 1 so, either
X x X x X x ... > 2 ^ 3
てのがよくわからないんだけど、つまりXって何なの？

489:righ1113 ◆OPKWA8uhcY
16/06/23 23:37:45.96 2td5n7de.net
スレでは>>92ですが、
実際は違いますが、9→7→11→17→9とループしたとすると、
X=(1+1/(3*9))*(1+1/(3*7))*(1+1/(3*11))*(1+1/(3*17))となります。
これは明らかに1より大きいので、
X*X*X*... > 2^3となって、
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3と矛盾します。

490:１３２人目の素数さん
16/06/24 00:02:13.23 iaaPmoqS.net
よくわからん。
1→1のループは
X=(1+1/(3*1))=4/3>1
となって
X * X * X * >2^3となって
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3と矛盾しないの？

491:righ1113 ◆OPKWA8uhcY
16/06/24 00:31:18.91 4KA2vNvp.net
1→1のループは除外します。
全体的にこの論文は、コラッツ操作で1にたどり着く直前までを考えます。
1になった後のコラッツパターンを考えると、左端を伸ばすパターンとのずれは際限なく大きくなりますから。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)

492:righ1113 ◆OPKWA8uhcY
16/06/24 00:37:22.10 4KA2vNvp.net
つまり、コラッツ操作で1にたどり着いた後は、
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3
が成り立たなくなります。

493:１３２人目の素数さん
16/06/26 02:47:49.92 vn9j7NkJ.net
とりあえず、色々コンピュータで検証してます。
4.1 Xsを12ステップで区切ったときライトエッジパターンに８個以上１が入ることはない、についてだけど
2連続の0はない
3連続の1はない
11011のパターンはない
で計算したところ以下のパターンが出てきたんだが。
110101101011
これは問題になる？

494:righ1113 ◆OPKWA8uhcY
16/06/26 12:47:06.84 ONsv4xjJ.net
110101101011は、二回繰り返すと
110101101011110101101011となって、
3連続の1が出てくるので、除外されます。
Coqでは、>>468のpdfで、25ページ

495:の下の方の (filter remove_1_1_1 (map (cycle 2 nil) remove_8_12’)で、 cycle 2でパターンを二回繰り返して、filter remove_1_1_1で3連続の1を除外しています。

496:１３２人目の素数さん
16/06/26 13:09:08.17 vn9j7NkJ.net
どゆこと？
ライトエッジパターンは必ず周期１２のループになるの？

497:righ1113 ◆OPKWA8uhcY
16/06/26 14:12:10.81 ONsv4xjJ.net
そっかー、ならないですね。
二周期目を調べる時は、
12ステップで除外しきれなかったパターンの直積を取って、filterをかけないとダメですね。
……と思ったら「12ステップで除外しきれなかったパターン」って上の110101101011しかないんですね。
だったらcycle 2も直積も同じことで、110101101011110101101011となって、やはり除外されます。
これでどうでしょうか？

498:righ1113 ◆OPKWA8uhcY
16/06/26 14:41:21.46 ONsv4xjJ.net
いや、なんか怪しいです。
もうちょっと考え直してみます。

499:成清愼
16/06/26 18:26:22.61 0JPNDOFj.net
他スレのご指摘により数式だけでなく日本語の説明を加えました。
諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。
URLﾘﾝｸ(koubeichizoku.ix-web.tk)

500:成清愼
16/06/26 18:55:58.84 0JPNDOFj.net
ここで論じられているビットパターンは拙論では
2^p×3^m×ｇ±1　（ｇは 6a±1) として捉えており、これらは素因数分解の一意性
からユニークな数であることに着目しています。
コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを
≫+で表せば　2・2＾p・ｇ－1　≫+　2・2＾（p-1）・3＾1・ｇ－1≫+　2・2＾（p-2）・3＾2・ｇ－1　...
≫+　2・2＾1・3＾（p-1）・ｇ－1　≫+　2・3＾p・ｇ－1　となって
L(p，g)：＝｛2・2＾p・ｇ－1，2・2＾（p-1）・3＾1・ｇ－1，　2・2＾（p-2）・3＾2・ｇ－1　...
，+　2・2＾1・3＾（p-1）・ｇ－1　，2・3＾p・ｇ－1｝　となって　相異なる（p，g）のL集合同士は互いに素
また同じく相異なるLの和集合同士も互いに素となります。（L（p,g）∪ L(p',g')=φ）（p≠p’）∨（g≠g’）

501:成清愼
16/06/26 18:57:28.09 0JPNDOFj.net
ここで論じられているビットパターンは拙論では
2^p×3^m×ｇ±1　（ｇは 6a±1) として捉えており、これらは素因数分解の一意性
からユニークな数であることに着目しています。
コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを
≫+で表せば　2・2＾p・ｇ－1　≫+　2・2＾（p-1）・3＾1・ｇ－1≫+　2・2＾（p-2）・3＾2・ｇ－1　...
≫+　2・2＾1・3＾（p-1）・ｇ－1　≫+　2・3＾p・ｇ－1　となって
L(p，g)：＝｛2・2＾p・ｇ－1，2・2＾（p-1）・3＾1・ｇ－1，　2・2＾（p-2）・3＾2・ｇ－1　...
，+　2・2＾1・3＾（p-1）・ｇ－1　，2・3＾p・ｇ－1｝　とすれば、　相異なる（p，g）のL集合同士は互いに素
また同じく相異なるLの和集合同士も互いに素となります。（L（p,g）∪ L(p',g')=φ）（p≠p’）∨（g≠g’）

502:１３２人目の素数さん
16/06/26 20:18:08.07 EbU1sa9O.net
>>479
coqが通ったのに何が怪しいの？
なんのためのcoqなの？
coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと？

503:righ1113 ◆OPKWA8uhcY
16/06/26 20:34:28.45 ONsv4xjJ.net
＞coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと？
まあ、そういう事です。
Coqに通すまでの論証に穴があったという事です。

504:１３２人目の素数さん
16/06/26 21:05:16.83 vn9j7NkJ.net
そうならないように始めの命題からCoqで一気通貫で証明を通すことが望ましいね。
実際には難しいだろうけど。

505:righ1113 ◆OPKWA8uhcY
16/06/26 23:31:32.04 ONsv4xjJ.net
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始まりが可能なので、さらに調べる。

506:righ1113 ◆OPKWA8uhcY
16/06/26 23:35:20.57 ONsv4xjJ.net
「先頭が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でどうやってやろう……

507:１３２人目の素数さん
16/06/27 01:06:26.26 aRJFqPL1.net
どうせその論証にも穴がある。
都合の悪い並びはいつまで経ってもなくならない。
穴を埋めようとすると
＞「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した
こんな感じの細かい条件がさらに追加される。
それでもなお、都合の悪い並びはなくならない。
キリがないどころか、そもそもこのやり方では本質的に不可能。
0と1の並び方の規則を探求すること自体が全くの無駄。
こいつらは基本的にランダム列に近づきたがっている。
途中で不完全燃焼を起こしてループに陥るだけで、
それまでの間はランダム列に近づきたがっている。
そうやって規則がない方向に行こうとしている対象について
規則を探求しても、うまく行くわけないだろ。
それよりも、「ランダム列に近づきたがってる」ことを
実際に証明した方が早い(もちろん現状では未解決)。

508:righ1113 ◆OPKWA8uhcY
16/06/27 06:17:35.12 QoZs645r.net
>>486-487の状態遷移図を作ってみました。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)
これを見ると穴は無いと思うんんですけどねー

509:１３２人目の素数さん
16/06/27 20:20:15.84 q11mMK/q.net
>>489
これ検証すんの結構つらいわｗ
Coqでなんとかならんか？
１が７個のパターンだけ考えてるみたいだけど
１が６個以下のパターンを除外していい理由がよくわからん。

510:righ1113 ◆OPKWA8uhcY
16/06/27 20:37:30.69 QoZs645r.net
Coqは考え中です。
（ちゃんとやってないですけど）
1が6個のパターンは、0,0が除外されるので
[0,1,0,1,0,1,0,1,0,1,0,1]
[1,0,1,0,1,0,1,0,1,0,1,0]
しかないんんですけど、こんなパターンは無いかなあと。
（どこかで1,1,が現れるはず）
1が5個以下のパターンは、必ず0,0が含まれるので、
全て除外されます。

511:１３２人目の素数さん
16/06/27 21:31:29.20 q11mMK/q.net
>>こんなパターンは無いかなあと。
数学の証明しようってのにずいぶんずぼらだなｗ
まあ気持ちはわかるが。

512:righ1113 ◆OPKWA8uhcY
16/06/27 21:44:48.79 QoZs645r.net
後でちゃんと証明しますねw

513:１３２人目の素数さん
16/06/27 22:43:04.85 j3iC4IAi.net
ポエムのうちは読む気はないけど証明されたら眺めてみようかくらいに思ってる人はそれなりにいると思うからがんばってね。

514:righ1113 ◆OPKWA8uhcY
16/06/28 02:37:55.06 yHVq8lhZ.net
12区切りで1が6個入るパターンは除外される証明ができました。
>>468の7ページを見ながらご覧下さい。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)
ライトエッジパターンでは「2連続の0」「3連続の1」「1,1,0,1,1」に加えて「0,1,0,1,0,1,0」
も除外されるという事です。

515:righ1113 ◆OPKWA8uhcY
16/06/28 14:15:43.06 QhVmHp3u.net
次の補題も証明します。
11010 11010 11010 11010 11ライトエッジパターンは無い。
URLﾘﾝｸ(cdn-ak.f.st-hatena.com)

516:１３２人目の素数さん
16/06/28 15:36:10.76 7Qb0mD6N.net
>>468
発散する初期値がないことの証明も間違ってるように見える。
実際に (log_2 x_s)/s の挙動を計算してみると、
発散する初期値があろうがなかろうが、無条件で有界であることが分かる。
まず、9ページ目の(3)式はコラッツの軌道のsステップ目を表現しただけだから、
何の条件もなしに成り立っている。以下、(3)式から出発して
x_s ＝ x_0(3^s/2^t)(1＋1/(3x_0))・・・(1＋1/(3x_{s－1}))
≦ x_0(3^s/2^t)(1＋1/3)・・・(1＋1/3)
＝ x_0(3^s/2^t)(1＋1/3)^s
＝ x_0(3^s/2^t)(4/3)^s
≦ x_0(3^s)(4/3)^s
＝ x_0 4^s
となるので、log_2 x_s ≦ log_2 x_0＋slog_2 4 となって、
(log_2 x_s)/s ≦(log_2 x0)/s ＋ 2 となる。よって、
発散する初期値があろうがなかろうが、無条件で有界になっている。
このことから、pdfの10ページ目にある
「 Here, from Fig.3 (傾きが垂直に近づくので) 」
のところは自動的に間違いとなる。

517:righ1113 ◆OPKWA8uhcY
16/06/28 15:53:05.99 QhVmHp3u.net
あちゃー
確かにその通りですね。

518:righ1113 ◆OPKWA8uhcY
16/06/28 18:10:44.75 QhVmHp3u.net
こういうのはどうでしょうか。
xは発散するとする。
(1+1/3x_0)…(1+1/3x_{s-1}) < 2^4 だから (1+1/3x_1)…(1+1/3x_s) < 2^4 も成り立つ。
t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。
s→∞でt→∞だから、
lim[t→∞](1+3/t)^t = e^3 ≒ 20 > 16 だから、
無限大に辿り着く前に16を超える。越えた所をs'と置くと、
(1+1/3x_1)…(1+1/3x_s') > 16 となって、(1+1/3x_1)…(1+1/3x_s') < 2^4 と矛盾する。

519:１３２人目の素数さん
16/06/28 19:21:07.89 7Qb0mD6N.net
>>499
＞t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。
問題外。x_sの発散スピードが大きいとき、そのようなaは取れない。
コラッツの問題を舐めるな。

520:righ1113 ◆OPKWA8uhcY
16/06/28 20:08:23.00 QhVmHp3u.net
t=e^sとか、t=s!とかにしてもダメなんでしょうか？

521:１３２人目の素数さん
16/06/28 20:15:33.20 7Qb0mD6N.net
>>501
どうも君は不等式に対する感覚がイカれてるね。
パッと見てすぐに分かる間違いに全く気づいてない。
tが大きければ大きいほど、(1＋3/t)^t は e^3 に近づくのだから、余計に
(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)
が成り立ちにくくなるだけだろ。
ていうか、x_1からx_sまでが物凄い勢いで大きければ、
(1+1/3x_1)…(1+1/3x_s) はほとんど 1 に等しいのだから、もはや
(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)
なんて成り立たないでしょ。

522:righ1113 ◆OPKWA8uhcY
16/06/28 20:29:39.54 QhVmHp3u.net
そうですか……
ありがとうございます……

523:１３２人目の素数さん
16/06/28 20:42:18.49 7Qb0mD6N.net
>>503
より詳しく説明しよう。
もし発散する初期値が存在するならば、次が成り立つことが証明できる。
∀ε＞0, ∃x_0 s.t.
x_0は発散する初期値であり、かつ (1+1/3x_1)…(1+1/3x_s) ＜ 1＋ε (s∈N).
このことから、(1+1/3x_1)…(1+1/3x_s) を統一的に下から押さえることができる定数は
「 1 」しかないことが分かる。つまり、x_0が発散する初期値ならば、
1 ＜ (1+1/3x_1)…(1+1/3x_s) (s∈N)
が成り立つということ。しかし、この不等式は自明なので、何の役にも立たない。
結局、この方針では原理的に不可能。

524:１３２人目の素数さん
16/06/28 21:02:38.37 pww1LGSL.net
ん～識者乱入か？
俺じゃよくわからんし勘違いを防ぐためにも
なるべくCoqで証明を通してほしいよね。

次ページ