0001１３２人目の素数さん垢版
2012/10/14(日) 10:32:39.71http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。
探検
コラッツ予想がとけたらいいな
■ このスレッドは過去ログ倉庫に格納されています
http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。
・前準備1
例えばx_sが7,11,17,13,5,17,13,5……とループするなら、先頭2項は外して、
さらに最小値をx_0とおいて、5,17,13,5,17,13……にします。
例ではx_3=x_0になります。
・前準備2
x_0~x_s-1がループ1周期として（x_0=x_s）、コラッツパターンX_sと左端を伸ばすパターンY_sのビット長は
[logY_s] = [log(x_0*(3/2)^s)]
[logX_s] = [log(x_0*(3/2)^s)+log(1+1/3x_0)…(1+1/3x_s-1)]
です。このときの[logY_s]と[logX_s]のずれがあってもなくても、周期を重ねるごとに[logX_s]と[logY_s]の差は
2log(1+1/3x_0)…(1+1/3x_s-1)、3log(1+1/3x_0)…(1+1/3x_s-1)、……と増大するので、
ずれも際限なく増大していきます。
x_s=x_0*3^s/2^t*(1+1/3x_0)…(1+1/3x_s-1) なので
1<(1+1/3x_0)…(1+1/3x_s-1)=2^t/3^s
3^s < 2^t です。
ここから
2^t > 3^s
tlog2 > slog3
t/s > log3 = log(3/2)+log2
(t-s)/s > log(3/2)
です。
(t-s)/sはコラッツパターンの左端傾きで、log(3/2)は左端を伸ばすパターンの右端傾きです。
https://drive.google.com/file/d/0B_FTpAj7C52FUVFicGpUUnlWSzQ/view?usp=sharing
(t-s)/sとlog(3/2)の交点をs'とおくと、
0=logx_0+s'log(3/2)-(t-s)/s*s' より
[s']=[logx_0/(t/s-log3)] < 3x_0 ……(1)
です。
左端を伸ばすパターンの
大域的傾きは、左端を伸ばすパターンの式Y_s=x_0*(3/2)^sに対して
2の対数目盛をとってlogY_s=logx_0+slog(3/2)となるので、log(3/2)です。
局所的傾きは、初期値x_0のsステップ目で
([logx_0+slog(3/2)]-[logx_0]+1)/(s+1)
になります。
[logx_0+slog(3/2)]-[logx_0]+1 > (s+1)log(3/2) で、
左辺が最大になるのは
[logx_0]+[slog(3/2)]-[logx_0]+1 > (s+1)log(3/2)
[slog(3/2)]+1 > (s+1)log(3/2) ……(2)
です。
例えばslog(3/2)=1.9とすると
(2)は 3 > 2.485 となります。
slog(3/2)=1.1とすると
(2)は 3 > 1.685 となります。
よって最大2の差が生まれます。
従ってlogx_0を5bit以上にとれば、
ずれは3以上になります。
X_[s']を3ビット(以上)下位へシフトしてずれを消します。これをXX_[s']とおきます。
XX_[s']=x_0*(3/2)^[s']*(1+1/3x_0)…(1+1/3x_[s']-1)/k とします。
[logXX_[s']] - [logY_[s']] = 0 から始めて
[log(x_0*(3/2)^[s'])+log(1+1/3x_0)…(1+1/3x_[s']-1)/k] - [log(x_0*(3/2)^[s'])] = 0
切り上げを外して
-1 < log(1+1/3x_0)…(1+1/3x_[s']-1)/k < 1
logを外して
1/2 < (1+1/3x_0)…(1+1/3x_[s']-1)/k < 2
ここで、
x_0からx_s-1のうちで最小はx_0かつ、(1)より
(1+1/3x_0)…(1+1/3x_[s']-1) < ((1+1/3x_0)^3x_0)^([s']/3x_0) < (1+1/3x_0)^3x_0 < e
なので、
(1+1/3x_0)…(1+1/3x_[s']-1)/k < e/8 ≒ 0.339
となって1/2を下回って矛盾します。
よって、4-2-1ループを除いて、ループする数はない
と言えるのではないかと思うのですが、どうでしょうか。
局所的傾きが大域的傾きより大きいとすると、
[logx_0+slog(3/2)]-[logx_0]+1 > (s+1)log(3/2) で、
天井関数の定義から
logx_0+slog(3/2)+1 -logx_0-1 +1 > [logx_0+slog(3/2)]-[logx_0]+1 > (s+1)log(3/2)
slog(3/2)+1 > (s+1)log(3/2)
1 > log(3/2)
となって、最大で約0.415大きい事になります。
従ってlogx_0を4bit以上にとれば、
ずれは3以上になります。
このイコールが成り立つ理由がよくわからないです。
(1+1/3x_0)…(1+1/3x_s-1)=2^t/3^s
現状ここは真偽不明なんでしょうか？
局所的傾きが大域的傾きより大きくても小さくても問題ないという事です。
局所的傾き<大域的傾きの場合は、
ずれがlogx_0になって、これが3以上なら問題ないです。
局所的傾き>大域的傾きの場合は、
ずれがlogx_0より小さくなるので、検討が必要です。
これでも問題ない事を言ったのが、>>625です。
やっぱ俺にはついていけないorz orz orz.
だれか頭の良い奴が来てくれればいいんだが。
思ってたより薄くて良い感じです。
パラパラとめくったところ、
自分の考察やコラッツパターンに似たものは無いですねえ。
こんなところですかね。
(W1)5*2^60までは反例がない
(W2)非自明なループがあればその周期は10439860591以上、奇数周期では6586818670以上
(W3)無限に多くの正の整数nは、コラッツ操作で1にたどり着くまでに、少なくとも6.143lognステップかかる（(3x+1)/2でやる）
(W4)The positive integer n with the largest currently known value of C,
such that it takes Clogn iterations of the 3x+1 function T(x)（(3x+1)/2でやる） to reach 1,
is n=7219136416377236271195 with C ≒ 36.7169. わかんねえ
(W5) >>513
後は細かい成果がつらつらと載っているんですが、僕の頭じゃ追えないです。
1.>>620-625の細切れCoq証明とpdf化
2.無限大に発散する方をぼんやり考える
2.だけど>>504を考えています。
（これを書いてくれた事はとてもありがたいです。自分ではとても思いつかなかった）
詳細は書けませんが、>>504から、
無限大に発散する初期値があれば、それは無限個存在するのか？などと思っております。
あと、「ランダムになりたがってる」の方のレスを読み返したりしています。
これはペアノ算術では証明も否定もできないらしいんだが
コラッツの予想もペアノ算術では証明も否定もできないとかあり得るんだろうか
ループの反例はないと言えるかな
すまんｗ。俺も全然詳しくはないんだが
ループの反例があれば、それを具体的に示せばいいだけだからペアノ算術の範疇かなと思った。
然詳しくはないんだが
・ペアノ算術で証明できない→ループはない
ですか。
ペアノ算術で証明できないと一口に言っても肯定が証明できないのか否定が証明できないのかで微妙に違うのかもしれん。
正直よくわからん。
誰か詳しい人help
停止性問題
https://ja.wikipedia.org/wiki/%E5%81%9C%E6%AD%A2%E6%80%A7%E5%95%8F%E9%A1%8C と
不動点コンビネータfix f = f (fix f)を参考にして。
そうでなければ走り続ける関数とします。
このとき、以下の関数Hは存在しません。
・Af(xs)の実行は停止する ⇒ H(Af,xs)はTrueを出力する。
・Af(xs)の実行は停止しない ⇒ H(Af,xs)はFalseを出力する。
Hが存在すると仮定して、
M(B(fix B))を、H(M,B(fix B))=TrueならM(B(fix B))自身は停止せず（無限リストを吐く）、
H(M,B(fix B))=Falseなら[1]を出力してM(B(fix B))を停止するプログラムとする。
・M(M(fix M))が停止したとすると、Mの定義よりH(M,M(fix M))=False。
Hの定義より H(M,M(fix M))=FalseとなるのはM(M(fix M))が停止しないときのみなので、矛盾。
・M(M(fix M))が停止しないとすると、Mの定義よりH(M,M(fix M))=True。
Hの定義より、H(M,M(fix M))=TrueとなるのはM(M(fix M))が停止するときのみなので、矛盾。
よってHは存在しない。⇒コラッツ遷移を上から押さえる関数を決定するプログラムは存在しない。
いかがでしょうか。
module Collatz08 where
import Control.Monad.Fix
col :: Integer -> Integer
col 1 = 1
col x = if odd x then 3*x+1 else x `div` 2
af :: [Integer] -> [Integer]
af xs = concat $ map af' xs
af' :: Integer -> [Integer]
af' x = (\z -> z ++ [1])
$ takeWhile (1/=)
-- x*100を任意の関数にする
$ takeWhile (\y -> if x*100 > y then True else error "over!")
$ iterate col x
-- この関数が定義できない
h :: ([Integer] -> [Integer]) -> [Integer] -> Bool
h _ _ = False
m :: [Integer] -> [Integer]
m xs = if h m xs then [1..] else [1]
*Collatz08> af [1..]
[1,2,1,3,…,2158,1079*** Exception: over!
*Collatz08> h af [1..]
False
*Collatz08> m (m (fix m))
[1]
実際の挙動とは異なりますが、型が合っている事は確認できます。
これじゃコラッツの予想に関しては何も言えないはずと思うが？？？
コラッツ予想について言えると思うのですが……
Af(xs)で仮定してるのは「発散したら停止し、そうでなければ走り続ける関数」だけだろ？
発散するかどうかだけが問題でコラッツの特性は全く使われてないじゃん？
コラッツを使っていると言えるのではないでしょうか。
この部分をほかの式にしても同様の議論が成り立っちゃうんじゃないの？ってこと
同様の議論が成り立つなら特にコラッツの予想について特別なことが言えてるんじゃなくて
もっと一般的なことしか言えてないってことになると思った。
考え直してみます。
フェルマーは停止しないからH(フェルマー)は定義できる。
一般のHが存在しないからといって、個別のH(コラッツ)やH(ゴールドバッハ)が存在しないとは言えないのですね。
ダメということで、ありがとうございました。
個別の知識を振り回しても正しい議論はできない
「この議論にはコラッツ由来の性質が使われてないから何かがおかしい」
という嗅覚が働かない人間はスタートラインにも立てない
コラッツ予想に限らんがね
永遠に低レベルな領域をぐるぐる回り続けて間違え続けるだけ
時間の無駄だな
人生は死ぬまでの暇潰しだからいいんだよ。そんなもんで。
Require Import Arith.
Require Import Omega.
Require Import Rbase.
は共通です。
(** 1<(1+1/3x_0)…(1+1/3x_s-1)=2^t/3^s -> 3^s<2^t *)
Theorem t1:
forall (x_0 x_s multi s t :nat),
x_0=x_s -> x_s<>0 -> 3^s<>0 ->
3^s*multi > 1 ->
multi > 1 ->
2^t * x_s = x_0 * (3^s * multi) -> 2^t/3^s > 1.
Proof.
intros.
rewrite H in H4.
apply Nat.div_unique_exact in H4.
rewrite Nat.div_mul in H4.
assert(forall (a b:nat), a=b -> b=a).
intros.
omega.
apply H5 in H4.
apply Nat.div_unique_exact in H4.
rewrite H4 in H3.
auto.
auto.
auto.
auto.
Qed.
(** tlog2>slog3 -> (t-s)/s>log(3/2) *)
Variable log2 : nat -> nat.
Theorem t2:
forall (s t:nat),
s<>0 -> log2 2=1 -> t*log2 2 >= s*log2 3 -> t/s-1 >= log2 3 -1.
Proof.
intros.
rewrite H0 in H1.
ring_simplify in H1.
apply Nat.div_le_lower_bound in H1.
apply (Nat.sub_le_mono_r (log2 3) (t/s) 1) in H1.
auto.
auto.
Qed.
(** 0=logx_0+s'log(3/2)-(t-s)/s*s' -> s'=logx_0/(t/s-log3) *)
Variable log2Z : Z -> Z.
Open Scope Z.
Theorem t3:
forall (x0 s t s':Z),
s <> 0 ->
t/s -log2Z 3 <> 0 ->
0=log2Z x0+s'*(log2Z 3 -1)-(t+(-1)*s)/s*s' -> s'=log2Z x0/(t/s-log2Z 3).
Proof.
intros.
rewrite (Z.div_add t (-1) s) in H1.
ring_simplify in H1.
apply (Zplus_minus_eq) in H1.
ring_simplify in H1.
apply (Zplus_minus_eq) in H1.
assert(forall (a b c:Z), -a=-b-c -> a=b+c).
intros.
omega.
assert(forall (a b:Z), -a*b = -(a*b)).
intros.
ring_simplify.
auto.
rewrite H3 in H1.
apply (H2 (log2Z x0) (s'*(t/s)) (-s'*log2Z 3)) in H1.
ring_simplify in H1.
rewrite <- (Zmult_minus_distr_l (t/s) (log2Z 3) s') in H1.
assert(forall (a b:Z), a*b=b*a).
intros.
ring_simplify.
auto.
rewrite H4 in H1.
apply Z.div_unique_exact in H1.
auto.
auto.
auto.
Qed.
Close Scope Z.
(** [logx_0+slog(3/2)]-[logx_0]+1 > (s+1)log(3/2) -> 1 > log(3/2) *)
Variable up : nat -> nat.
Theorem t4:
forall (x0 s:nat),
(forall (x y z:nat), up(x)-up(y)+1>z -> x-y+1>z ) ->
up(log2 x0 + s*(log2 3 -1)) -up(log2 x0) +1 > (s+1)*(log2 3 -1) ->
1 > (log2 3 -1).
Proof.
intros.
apply (H (log2 x0 +s*(log2 3 -1)) (log2 x0) ((s+1)*(log2 3 -1))) in H0.
assert(forall (a b c:nat), a+b-a+1>c -> b+1>c).
intros.
omega.
apply H1 in H0.
ring_simplify in H0.
omega.
Qed.
(** [logXX_[s']]-[logY_[s']]=0 -> 1/2<(1+1/3x_0)…(1+1/3x_[s']-1)/k *)
Theorem t5:
forall (XX A multi k:nat),
(forall (x y z:nat), up(x+(log2 y)/z)-up((log2 y)/z)=0 -> 1<2*y/z ) ->
XX=A+(log2 multi)/k ->
up(XX)-up((log2 multi)/k)=0 -> 1<2*multi/k.
Proof.
intros.
rewrite H0 in H1.
apply H in H1.
auto.
Qed.
(** k<2*multi -> multi*100<271 -> k>=8 -> False *)
Theorem t6:
forall (k multi:nat),
k<2*multi ->
multi*100<271 ->
k>=8 -> False.
Proof.
intros.
omega.
Qed.
以上になります。
コラッツの式はどこにあるんだろう
2^t * x_s = x_0 * (3^s * multi) -> 2^t/3^s > 1.
なのですが、左の式を変形すると
x_s = x_0 * 3^s / 2^t * (1+1/3x_0)…(1+1/3x_s-1)
です。 (1+1/3x_0)…(1+1/3x_s-1)=multiです。
このようなこすい変形が随所に出てきます。
（そうしないと解けなかった）
スマンなよく分かってなくて
x_0=x_sです。
もうちょっと追ってみる
http://www.ni covideo.jp/watch/sm30573682
110ルールというのが面白い
チューリング完全なら計算が停止しないパターンがあるはず？
それをコラッツパターンにどう繋げたら良いか分からないです。
現状なんにも出来てないです。
ループのほうのpdfはゆっくりと書いています。
今は別の事を考えているので中断します。
やる気がなくてすみません。
4-2-1以外のループが無い事の証明
https://drive.google.com/open?id=0B_FTpAj7C52FczVBdmNNZWYwR1k
俺の実力じゃ読み解けないけど読みやすさを意識して書いたんだろなてのは伝わってくるよ。
ごちゃごちゃ式変形してるけど一見、そこからは特別な情報は出てこなさそうに見えるんだよなぁ
俺にもうちょっと実力があれば付き合ってやれるんだが、すまんな。
胆は5ページ目の
(1+1/3x_0)...(1+1/3x_{[s']-1})がeより小さい
ところかな、と思います。
コラッツパターンの左端傾き(t-s)/sと、 左端を伸ばすパターンの右端傾きlog(3/2)
が交差する事も重要だと思います。
この証明は一周する度に何が減るって議論してるような？
何が減ってるんだろう？
>>620の前準備2より、ループを重ねるたびに、
コラッツパターンと左端を伸ばすパターンのずれが「増える」のです。
で、コラッツパターンの左端と、左端を伸ばすパターンの右端が交差する所で
ずれが3以上になって、
その場所で矛盾するのです。
すまん、この記号[ ]の意味はなんだっけ？切り上げ？
[ ]はガウスの記号、つまり端数を丸めて（絶対値で見た時に切り捨てて）整数にする演算のことじゃないの？
すまん、ガウスの記号の意味は正負どちらでもそれ以下の最大の整数にする演算、つまりfloorと同じ意味だった
ともかく[ ]はガウスの記号だと思うよ
（なぜかガウスの記号には高校数学だと[ ]を使うのに対して、大学以上の数学だと下だけに爪が出てる記号（つまり」とその左右反転形）を使うよね）
複雑すぎて手に負えない。
左端を伸ばすパターンは、コラッツパターンから
情報を落とすことで得られるポンコツな指標。
操作を進めるごとに情報が落ちていくので、どんどん精度が悪くなる。
こんなものがコラッツパターンの実態を捉えているなんてあり得ないので、
コラッツパターンと比較したところで大して得るものは無い。
「左端傾き」「右端傾き」といった考え方もゴミである。
離散的な対象に対して、大域的にであれ局所的にであれ「傾き」に相当する量を
定義したところで、それは極めて大雑把な荒い指標にしかならない。
そんな頼りない道具だけでコラッツ予想が制御できるわけがない。
>>677の(17)の不等式が完全に間違っている。(17)では
[s']＝[(log_2 x_0)/(t/s−log_2 3)] ＜ 3x_0
となっているが、分母の (t/s−log_2 3) が非常にゼロに近い場合、
[s']
＝ [(log_2 x_0)/(t/s−log_2 3)]
＝ [(log_2 x_0)/(ほぼゼロ)]
＝ [(log_2 x_0) * (1/ほぼゼロ)]
＝ [(log_2 x_0) * 滅茶苦茶デカイ係数 ]
＞ 3x_0
となり得るので、この場合、不等号が逆転することになる。
「このような可能性は実際には起こらず、確実に [s'] ＜ 3x_0 が成り立つ」
と言うのであれば、そのことを証明しなければならない。
しかし、末尾の coq では証明されていない。
「図を使って傾きを比較することで [s'] ＜ 3x_0 が成り立つ」
と言っているようにも見えるが、図が無い上に、それぞれのパターンを
どのように配置してどこを原点としてどのようにして直線の傾きを
比較するのか文章からは読み取れないので判断のしようがない。
(1)〜(23)のうち、(17),(22),(23)を除く全ての式は
おそらく正しいと思われる。なぜなら、これらの式では
・ 記号の定義
・ 単なる等式の変形
・ 自明な評価による自明な不等式の導出
のいずれかの行為しか行っていないからだ。
パターンのずれとか傾きの違いがどうこうなどと
御託を並べているものの、その実態は上記の3項目のみである。
ちなみに、(22),(23)で間違っている箇所は、途中で(17)を使っているところであり、
それゆえに間違いとなる。従って、実質的には(17)のみが間違いとなる。
そして、それ以外の個所では上記の3項目による自明な行為しか行っていないので、
結局、>>677ではコラッツ予想の難しさを(17)に責任転嫁しているだけということになり、
コラッツ予想について何も言えていないことになる。
(t/s−log_2 3) > 0 のところを、
(t/s−log_2 3) > 1 と勘違いしていました。
またしてもダメでした……
お騒がせしました。
頭の良い奴が来てくれたか。
俺も力になれればいいんだが、なかなか難しい。
￥
珍しく自分なりに数学をやっている人がその研究経過について報告してくれているのですから
数学板のすべてのスレが腐っているわけではありません
他の板でも腐っているスレもあれば数学板でもこのスレのように「数学」という言葉本来の目的で使用されているスレもあるのですから
また数学板の全てのスレで各スレの投稿者や読者の集合が一致しているわけでもありません
（もしそうだと主張なさるならば数学の証明として通用するレベルの論理的な証明か又は２ちゃんねる数学板のログのような客観的で確実な証拠でもご提示ください）
板で腐っているかいないか決めつけるのは人の知性の有無を国籍や肌の色で判断するのと同じ乱雑で反知性的な判断であって
数学や知性を愛する￥さんに相応しい行動とは思えません
スレ主さんや他の住人の方々、スレ違いの投稿失礼しました
基地外に言葉が通じると思ってるのか？
￥
現代数学の系譜スレでは￥氏はちゃんと会話をなさってるので
こちらが適切に発言すれば言葉は通じると思ったわけです
■ このスレッドは過去ログ倉庫に格納されています
ニュース
- 【米国】反ユダヤ事案、２３年に過去最多 [樽悶★]
- 埼玉の在日クルド人に差別や攻撃 県外からも電話「SNSで見た」 [少考さん★]
- 慶應義塾長が国立大の学費増額を提言「年55万→150万に」 文科省の会合で [少考さん★]
- 【サッカー】U-23日本代表、UAE代表に完封勝ちで2連勝！日韓戦を前に決勝トーナメント進出を決める [久太郎★]
- 【理研】日本人の祖先は「縄文系」「関西系」「東北系」の３系統か、ゲノム分析で従来の説「縄文と弥生」に疑問 ★2 [樽悶★]
- ロシア出身YouTuber、経済的困窮で「国ガチャ失敗」？嘆く日本人を一喝「給料13万？自分のせいやん」日本を「大当たり」とする理由は [muffin★]
- AFC U23アジアカップ カタール2024★8
- AFC U23アジアカップ カタール2024★9
- AFC U23アジアカップ カタール2024★10
- 【酒】日本vsUAE【U23アジアカップ】
- 【フジテレビ】2024 FORMULA 1【NEXT】Lap269
- とらせん祝勝会 ★2
- スピードランニングってあれ効果あるの！？
- 【鬼畜】10歳未満の女児をレイプしまくって逮捕された元保育士の小野寺朱生容疑者（23）が8回目の再逮捕
- 【実況】博衣こよりがえちえちplate up🧪★5
- 昼休みに話しかけてくる上司、先輩
- Googleって勝手にドライブ内覗くの？やばくね？
- 純金茶わん泥棒「俺イケメンだからイケメンを活かしてあれこれやりますモデルみたいなもんだねよろしく！笑」 [617981698]