X



トップページ数学
1002コメント517KB
コラッツ予想がとけたらいいな
■ このスレッドは過去ログ倉庫に格納されています
0001132人目の素数さん
垢版 |
2012/10/14(日) 10:32:39.71
525 名前:132人目の素数さん[sage] 投稿日:2012/09/03(月) 18:24:27.22
http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。
0417413
垢版 |
2016/06/08(水) 21:39:10.48ID:lYAR2M8u
俺は>>1>>1証明のほころびからコラッツ予想の反例を見つけるというストーリーを期待しているw
0418132人目の素数さん
垢版 |
2016/06/08(水) 22:23:08.13ID:WkHIclqp
ブールピタゴラス問題も真っ青の反例ループのサイズが200TB超えとかを希望w
0419righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/08(水) 23:36:44.69ID:aPj7A/ik
ビット数を増やしても、ずれが際限なく増えていく〜〜
0420132人目の素数さん
垢版 |
2016/06/09(木) 02:17:55.30ID:Z2BPqjfW
ずれの計算では上手く行くわけがないって、ずっと前に指摘されてたじゃん。
何をいまさら。こんなやり方でコラッツの予想が解けるわけがない。
0421132人目の素数さん
垢版 |
2016/06/09(木) 19:53:16.16ID:OutW5kLL
仮にずれの計算でうまくいかなかったとしても>>1は修正してくるだろう。
Coqがあれば間違った証明は通らないだろうしいくらでも頑張れる環境がある。
コラッツの予想が解けるのは時間の問題だな。
0422righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/10(金) 05:50:42.64ID:oOXw5TlH
まだ思いつきのレベルなんであれですが……
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なのはご容赦を。
0424righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/11(土) 03:48:47.75ID:6GM2rdQN
単純に僕のCoq歴が3週間、Haskell歴が5年くらいだからだと思います。
0425132人目の素数さん
垢版 |
2016/06/11(土) 18:00:38.27ID:p56I7Lto
Haskell 5年もやってんのか凄いな。
5年間で何行くらいHaskellでコード書いたの?
0426righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/11(土) 20:46:46.40ID:6GM2rdQN
Haskellはコード量が短くすむこともあって、
5年間で2000〜3000行ぐらいじゃないでしょうか。
0427132人目の素数さん
垢版 |
2016/06/11(土) 20:59:42.80ID:p56I7Lto
100行のプログラム20〜30本書いてるってことか
なかなか大したもんだ。
0428righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 02:40:18.56ID:6i9eMAsV
大幅に証明を変えます。
左端を伸ばすパターン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が言えます。図参照。
http://cdn-ak.f.st-hatena.com/images/fotolife/r/righ1113/20160613/20160613021641.jpg
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以下に押さえられる事になります。

(※)は後で書きます。
0429righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 05:34:28.73ID:6i9eMAsV
× (初期値11111) < (初期値000001)
○ (初期値011111) < (初期値0000001)
0430righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 09:53:52.64ID:6i9eMAsV
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は無い事も分かる)
0431righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/13(月) 09:57:29.37ID:6i9eMAsV
次に、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
[]
空リストになったので、(※)が証明できました。
0432righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:36:32.33ID:GDyexPn/
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).
0433righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:41:24.87ID:GDyexPn/
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.
0434righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:46:24.20ID:GDyexPn/
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.
0435righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/14(火) 09:49:36.01ID:GDyexPn/
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.が通ると気持ちが良いですね。
0440132人目の素数さん
垢版 |
2016/06/19(日) 05:13:52.50ID:R9PbWXF5
>>1
コラッツパターンとかライトエッジパターンとかよくわからん。
もし余力があればideoneにプログラム上げてくれんか?
好きな数を入力してそれに対してそのパターンを出力してほしい。

http://ideone.com/

haskellも選べるからたぶんもうすでに書いたものがあるだろ?
0443132人目の素数さん
垢版 |
2016/06/19(日) 08:36:15.00ID:R9PbWXF5
エクセルマクロはうごきました。
サンクス。

左端がどう決まってるのかいまいち分かってないんだけど
2で割れた回数とかだよね?
>>439のは英語だったからいまいち自信がもてない。
0444righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/19(日) 12:31:44.57ID:o4I0V/Mj
コラッツパターンの左側は、
コラッツ操作で<2で割った回数-1>を蓄積しているものです。
>>173にもあります。
(マクロやpdfでは0を書いてないけど)
0445132人目の素数さん
垢版 |
2016/06/20(月) 20:49:50.82ID:AO/P2Y9A
左端を伸ばすパターンの説明で

3. Becomes the next x from the left end of the 1 to 1 on the right.

てのがあるんだけど、どう訳せばいいのかよくわからんw
教えて〜
0446righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/20(月) 22:36:36.36ID:IBPpfU1W
「次のxとして、左端の1から右端の1までを取る」という意味です。
_111111001 =x0が
1011110111 =x1になった時、
x1は左端の1から右端の1までを取るね、という事です。

実は英語は苦手で、いつも赤点でしたwww
0449132人目の素数さん
垢版 |
2016/06/21(火) 20:10:09.84ID:shTmSKB6
まだ理解できてないが左端を伸ばすパターンもエクセルマクロあるの?
あるならオクレ。
0450righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/21(火) 20:18:58.92ID:w+gnd+8K
左端を伸ばすパターンは数が左に伸びるのと、
ステップが無限に続くので、作れてないです。すみません。
0452132人目の素数さん
垢版 |
2016/06/21(火) 21:05:09.09ID:shTmSKB6
んー左に伸ばすパターンって出力のサイズを制限したらプログラム書ける?
制限しても難しい?
0453righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/21(火) 21:34:19.98ID:w+gnd+8K
ちょっとやってみます。
気長にお待ちください。
0455righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/22(水) 06:06:53.11ID:kg3XYDgA
https://drive.google.com/file/d/0B_FTpAj7C52FVHlFNWt4UU1Vb3M/view?usp=sharing
A列に10進数で数を入れて、「計算」ボタンを押すと、
B列にコラッツパターンのライトエッジパターンが、
C列に左端を伸ばすパターンのライトエッジパターンが、
D列からにコラッツパターンと左端を伸ばすパターンが表示されます。
B,C列で色が変わっている所は、コラッツパターンと左端を伸ばすパターンの右端がずれている所です。

大きい数を入れると「列が足りない」エラーが出るかもしれませんが、
Excel2007以降を使っているならば、Officeボタンから「変換」を選んで開きなおすと、
最大列が256列から16384列になります。
0457132人目の素数さん
垢版 |
2016/06/22(水) 20:08:21.63ID:3ACjIS1K
>>455
おおう、乙カレ。やるね。
左端を伸ばすパターンの正体がいまいちわかってないんだけどどういう思想で出来たものなの?
説明できるなら説明クレクレ。
0458132人目の素数さん
垢版 |
2016/06/22(水) 20:25:08.09ID:3ACjIS1K
333入れたら結果が出てこなかったんだが?
なんか制限とかあるんだっけ?
よくわかってなくてスマン。
0459righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/22(水) 20:27:44.55ID:SAQFF6Ga
コラッツ予想を2進数で考える、というのは前々からあって、
コラッツパターンを見出した時に、最後のルール
「最後に、左端に+1する」
を外したら面白いんじゃね、と思って左端を伸ばすパターンが出来ました。
まあ、偶然の産物ですね。
0460righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/22(水) 20:32:36.93ID:SAQFF6Ga
>>458
自分の環境では出てきます。
・マクロを有効にする
・数字を入れた後一回Enterを押して、カーソルを合わせ直して実行する
あたりを試してみてください。
0463132人目の素数さん
垢版 |
2016/06/22(水) 21:22:24.14ID:3ACjIS1K
ライトエッジを12個づつに区切ったとき8個以上1が入らないことが言えると
なぜコラッツ予想が証明されたことになるの?

今はそこで悩んでる。
0464132人目の素数さん
垢版 |
2016/06/22(水) 21:31:10.84ID:3ACjIS1K
左端パターンとコラッツパターンのずれが有限だとコラッツの予想が証明されたことになるの?
やっぱまだよくわからん。
0465righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/22(水) 22:01:29.56ID:SAQFF6Ga
>>463
X0とy0B*2^(py0+1)は右端が1ずれた(y0Bが大きい)状態からスタートします。
y0Bの12区切りのライトエッジパターンは1が7個はいっていて、
もしX0の12区切りのライトエッジパターンに1が8個以上入らなければ、初期値の1ずれがずっと維持されるので、
X0 < y0B*2^(py0+1)が言えるわけです。
これ自体でコラッツ予想は証明されないです。
0466righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/22(水) 22:05:31.40ID:SAQFF6Ga
>>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がない」「コラッツ予想で無限大に発散する数はない」
事を個別に証明しています。
0469132人目の素数さん
垢版 |
2016/06/23(木) 21:56:11.47ID:tqdQH9fb
>>1
頑張ってもらってるのにスマンが俺の頭じゃいまいち理解が追いつかない。
面白そうではあるんだけど。
まあ、ボチボチ読んでみます。
0470132人目の素数さん
垢版 |
2016/06/23(木) 22:55:11.53ID:tqdQH9fb
5章の(14)(15)の式なんだけど

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って何なの?
0471righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/23(木) 23:37:45.96ID:2td5n7de
スレでは>>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と矛盾します。
0472132人目の素数さん
垢版 |
2016/06/24(金) 00:02:13.23ID:iaaPmoqS
よくわからん。

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と矛盾しないの?
0474righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/24(金) 00:37:22.10ID:4KA2vNvp
つまり、コラッツ操作で1にたどり着いた後は、
(1+1/(3*x0))...(1+1/(3*x_s-1)) < 2^3
が成り立たなくなります。
0475132人目の素数さん
垢版 |
2016/06/26(日) 02:47:49.92ID:vn9j7NkJ
とりあえず、色々コンピュータで検証してます。

4.1 Xsを12ステップで区切ったときライトエッジパターンに8個以上1が入ることはない、についてだけど

2連続の0はない
3連続の1はない
11011のパターンはない

で計算したところ以下のパターンが出てきたんだが。

110101101011

これは問題になる?
0476righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/26(日) 12:47:06.84ID:ONsv4xjJ
110101101011は、二回繰り返すと
110101101011110101101011となって、
3連続の1が出てくるので、除外されます。

Coqでは、>>468のpdfで、25ページの下の方の
(filter remove_1_1_1 (map (cycle 2 nil) remove_8_12’)で、
cycle 2でパターンを二回繰り返して、filter remove_1_1_1で3連続の1を除外しています。
0477132人目の素数さん
垢版 |
2016/06/26(日) 13:09:08.17ID:vn9j7NkJ
どゆこと?
ライトエッジパターンは必ず周期12のループになるの?
0478righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/26(日) 14:12:10.81ID:ONsv4xjJ
そっかー、ならないですね。
二周期目を調べる時は、
12ステップで除外しきれなかったパターンの直積を取って、filterをかけないとダメですね。

……と思ったら「12ステップで除外しきれなかったパターン」って上の110101101011しかないんですね。
だったらcycle 2も直積も同じことで、110101101011110101101011となって、やはり除外されます。
これでどうでしょうか?
0479righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/26(日) 14:41:21.46ID:ONsv4xjJ
いや、なんか怪しいです。
もうちょっと考え直してみます。
0480成清愼
垢版 |
2016/06/26(日) 18:26:22.61ID:0JPNDOFj
他スレのご指摘により数式だけでなく日本語の説明を加えました。
諸兄におかれましては何卒よろしくご査収の上ご批評賜りたくよろしくお願い申し上げます。
http://koubeichizoku.ix-web.tk/collatz/
0481成清愼
垢版 |
2016/06/26(日) 18:55:58.84ID:0JPNDOFj
ここで論じられているビットパターンは拙論では
2^p×3^m×g±1 (gは 6a±1) として捉えており、これらは素因数分解の一意性
からユニークな数であることに着目しています。
コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを
≫+で表せば 2・2^p・g−1 ≫+ 2・2^(p-1)・3^1・g−1≫+ 2・2^(p-2)・3^2・g−1 ...
≫+ 2・2^1・3^(p-1)・g−1 ≫+ 2・3^p・g−1 となって
L(p,g):={2・2^p・g−1,2・2^(p-1)・3^1・g−1, 2・2^(p-2)・3^2・g−1 ...
,+ 2・2^1・3^(p-1)・g−1 ,2・3^p・g−1} となって 相異なる(p,g)のL集合同士は互いに素
また同じく相異なるLの和集合同士も互いに素となります。(L(p,g)∪ L(p',g')=φ)(p≠p’)∨(g≠g’)
0482成清愼
垢版 |
2016/06/26(日) 18:57:28.09ID:0JPNDOFj
ここで論じられているビットパターンは拙論では
2^p×3^m×g±1 (gは 6a±1) として捉えており、これらは素因数分解の一意性
からユニークな数であることに着目しています。
コラッツ予想の題意に従った奇数から奇数への変化のうち奇数間で増大するものを
≫+で表せば 2・2^p・g−1 ≫+ 2・2^(p-1)・3^1・g−1≫+ 2・2^(p-2)・3^2・g−1 ...
≫+ 2・2^1・3^(p-1)・g−1 ≫+ 2・3^p・g−1 となって
L(p,g):={2・2^p・g−1,2・2^(p-1)・3^1・g−1, 2・2^(p-2)・3^2・g−1 ...
,+ 2・2^1・3^(p-1)・g−1 ,2・3^p・g−1} とすれば、 相異なる(p,g)のL集合同士は互いに素
また同じく相異なるLの和集合同士も互いに素となります。(L(p,g)∪ L(p',g')=φ)(p≠p’)∨(g≠g’)
0483132人目の素数さん
垢版 |
2016/06/26(日) 20:18:08.07ID:EbU1sa9O
>>479
coqが通ったのに何が怪しいの?
なんのためのcoqなの?

coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと?
0484righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/26(日) 20:34:28.45ID:ONsv4xjJ
>coqは通ったけど、通った命題そのものがトンチンカンな主張だったってこと?
まあ、そういう事です。
Coqに通すまでの論証に穴があったという事です。
0485132人目の素数さん
垢版 |
2016/06/26(日) 21:05:16.83ID:vn9j7NkJ
そうならないように始めの命題からCoqで一気通貫で証明を通すことが望ましいね。
実際には難しいだろうけど。
0486righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/26(日) 23:31:32.04ID:ONsv4xjJ
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始まりが可能なので、さらに調べる。
0487righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/26(日) 23:35:20.57ID:ONsv4xjJ
「先頭が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でどうやってやろう……
0488132人目の素数さん
垢版 |
2016/06/27(月) 01:06:26.26ID:aRJFqPL1
どうせその論証にも穴がある。
都合の悪い並びはいつまで経ってもなくならない。
穴を埋めようとすると

>「先頭が10」で、「2連続の0」「3連続の1」「1,1,0,1,1」を除外した

こんな感じの細かい条件がさらに追加される。
それでもなお、都合の悪い並びはなくならない。
キリがないどころか、そもそもこのやり方では本質的に不可能。

0と1の並び方の規則を探求すること自体が全くの無駄。
こいつらは基本的にランダム列に近づきたがっている。
途中で不完全燃焼を起こしてループに陥るだけで、
それまでの間はランダム列に近づきたがっている。
そうやって規則がない方向に行こうとしている対象について
規則を探求しても、うまく行くわけないだろ。

それよりも、「ランダム列に近づきたがってる」ことを
実際に証明した方が早い(もちろん現状では未解決)。
0490132人目の素数さん
垢版 |
2016/06/27(月) 20:20:15.84ID:q11mMK/q
>>489
これ検証すんの結構つらいわw
Coqでなんとかならんか?

1が7個のパターンだけ考えてるみたいだけど
1が6個以下のパターンを除外していい理由がよくわからん。
0491righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/27(月) 20:37:30.69ID:QoZs645r
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が含まれるので、
全て除外されます。
0492132人目の素数さん
垢版 |
2016/06/27(月) 21:31:29.20ID:q11mMK/q
>>こんなパターンは無いかなあと。

数学の証明しようってのにずいぶんずぼらだなw
まあ気持ちはわかるが。
0494132人目の素数さん
垢版 |
2016/06/27(月) 22:43:04.85ID:j3iC4IAi
ポエムのうちは読む気はないけど証明されたら眺めてみようかくらいに思ってる人はそれなりにいると思うからがんばってね。
0497132人目の素数さん
垢版 |
2016/06/28(火) 15:36:10.76ID:7Qb0mD6N
>>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 (傾きが垂直に近づくので) 」

のところは自動的に間違いとなる。
0499righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/28(火) 18:10:44.75ID:QhVmHp3u
こういうのはどうでしょうか。

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 と矛盾する。
0500132人目の素数さん
垢版 |
2016/06/28(火) 19:21:07.89ID:7Qb0mD6N
>>499
>t=saと置き、(1+3/t)^t < (1+1/3x_1)…(1+1/3x_s)が成り立つようにaを定める。

問題外。x_sの発散スピードが大きいとき、そのようなaは取れない。
コラッツの問題を舐めるな。
0501righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/28(火) 20:08:23.00ID:QhVmHp3u
t=e^sとか、t=s!とかにしてもダメなんでしょうか?
0502132人目の素数さん
垢版 |
2016/06/28(火) 20:15:33.20ID:7Qb0mD6N
>>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)

なんて成り立たないでしょ。
0504132人目の素数さん
垢版 |
2016/06/28(火) 20:42:18.49ID:7Qb0mD6N
>>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)

が成り立つということ。しかし、この不等式は自明なので、何の役にも立たない。
結局、この方針では原理的に不可能。
0505132人目の素数さん
垢版 |
2016/06/28(火) 21:02:38.37ID:pww1LGSL
ん〜識者乱入か?
俺じゃよくわからんし勘違いを防ぐためにも
なるべくCoqで証明を通してほしいよね。
0506righ1113 ◆OPKWA8uhcY
垢版 |
2016/06/28(火) 21:52:49.95ID:QhVmHp3u
もしちゃんとZs < Ys <= Xs < ysB * 2^(pys+2) < 8Zs
が言えたら、
   Zsと8Zsのずれは3で、これがずっと変わらない
って無限大までいっても変わらないって事だから
xsが発散してもずれは3以下なんだと、今気づかせてもらった。

という訳で、無限大に発散する方はあきらめます。
4-2-1以外のLoopがない方に注力します。
0508righ1113 ◆OPKWA8uhcY
垢版 |
2016/07/09(土) 09:54:12.67ID:3emnwfEb
>>489の状態遷移図の穴が埋められないんです。
ちょっと休憩中です。
0510132人目の素数さん
垢版 |
2016/07/09(土) 19:28:48.04ID:xlO52T1E
>>489の状態遷移図の穴が埋められないんです。

穴は埋まらないよ。この方針じゃ原理的に不可能。
なんで分からないのかなあ。>>506のときみたいに
「これじゃ本質的にダメなんだ」って心の底から悟れよ。
ダメなんだよこれじゃ。ダメなの。このやり方じゃ解けないの。
0511132人目の素数さん
垢版 |
2016/07/09(土) 19:38:05.16ID:9+qw8rwI
本質的に解けないことちゃんと数学的に証明をしてあげないと。
頭ごなしに否定するだけじゃ納得するはずないでしょ。
0512132人目の素数さん
垢版 |
2016/07/09(土) 20:14:55.98ID:xlO52T1E
>>511
数学的に証明するのはムリ。
しかし、ほぼ確実な状況証拠はある。

3n+1版ではなく、an+1版のコラッツ予想を考える(ただしaは7以上の奇数)。
この場合、ほとんどの初期値でコラッツの軌道が発散することが予想されている。
軌道上に出現する各々の値の偶奇を0,1で横一列に並べると、
どうもその列は、ほとんどの初期値で2進正規になっているように見える。
もし2進正規になってることが証明できたならば、コラッツ予想でおなじみの
「軌道上では偶数と奇数が1/2ずつの確率で出現しそう」というヒューリティクスが
実際に正しいことが分かり、「ほとんどの初期値で発散する」という予想も正しいことが確定する。

おそらく、コラッツの軌道は本質的にランダムになりたがってる。
もともとの3n+1版でも同じことで、やはりランダムになりたがってる。
しかし、こちらの場合は掛ける数が「3」であるがゆえに、十分大きな数になれず、
それゆえに自由度が低下し、途中で不完全燃焼を起こしてループに陥る。
が、それまでの間はランダム列に近づきたがっている。初期値を大きく取れば取るほど、
ランダム列に近づきたがる期間も長くなるので、その間で幾らでも抜け穴となるパターンが生じうる。
だから本質的にムリなのだ。(続く)
0513132人目の素数さん
垢版 |
2016/07/09(土) 20:20:54.10ID:xlO52T1E
(続き)
ライトエッジの「抜け穴」と似たような現象は、以下の箇所にも見られる。
英語版のコラッツ予想の記事を見ると、

>In particular, Krasikov and Lagarias showed that the number of integers in the interval [1,x]
>that eventually reach one is at least proportional to x^0.84.[19]

という記述がある。区間[1,x]に属する自然数のうち、コラッツの変換によって1になる数の比率は、
少なくとも x^{0.84} はある、という驚くべき文章である。
文献[19]をかいつまんで説明すると、「コラッツの変換によって1になる自然数の集合」を、
ある種のパラメータで分割して、いくつかの集合に分けるところから始まる。
それらの集合の間に定まる漸化式を使って、x^{0.84}という評価を得ている。
この漸化式が完全に制御できれば、もっといい結果が出るわけだが、
漸化式がイジワルな形をしており、漸化式を展開するたびにランダム性が増してしまって制御できなくなる。
そこで、途中で評価を落として不等式の形にすることで、不等式の左辺と右辺に何とかパターン性を
出現させ、それによって問題を対処する。その結果、x^{0.84} という中途半端な数字になってしまう。

ライトエッジの抜け穴は、この「評価を落としてパターン性を出現させる」ところに
どことなく対応しているように見える。ライトエッジを完全に解析すると、まず間違いなく、
そのパターンは有限通りには収まらず、複雑な形の漸化式で記述されることになる。
その漸化式を展開するたびにランダム性が増してしまい、結局は制御できなくなる。

逆に、もしライトエッジが有限通りに収まったら、文献[19]の漸化式も実際には
上手くパターンに落とし込めることになると予想される。が、今のところそういう話は見てないし、
[19]を読んで漸化式を触ってみても、もう本能的に「こりゃムリだわ」っていう感想しか出てこない。

そんなわけで、ライトエッジの方針もムリに決まってるのだ。
0514132人目の素数さん
垢版 |
2016/07/09(土) 20:34:04.39ID:xlO52T1E
(補足)

結局、>>512の話でも、>>513の話でも、
コラッツの変換を深く深く弄れば弄るほど、
ランダム性が増していく感触が確かな手ごたえとして観測される。
どこまでいっても、パターンに収まってくれる気配が全く出てこない。
「本質的にランダムになりたがっている」としか思えないのだ。
また、コラッツ予想の難しさはまさにこの部分にあるはずだ。

>>488にも書いたが、コラッツ予想に取り組むなら、
「ランダムになりたがってる」という感触を
どうやって解析したらいいかを真正面から考えるしかないだろう。
そして、そのこと自体が既に難しく、だからこその未解決問題なのだろう。
0516132人目の素数さん
垢版 |
2016/07/10(日) 01:04:15.98ID:p/ut3oXY
コラッツ予想で毎回思うんだけど
プログラムでいうif文を扱える数学って存在すんのかなあ
■ このスレッドは過去ログ倉庫に格納されています

ニューススポーツなんでも実況