0001１３２人目の素数さん
2012/10/14(日) 10:32:39.71http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。
探検
コラッツ予想がとけたらいいな
■ このスレッドは過去ログ倉庫に格納されています
http://d.hatena.ne.jp/righ1113/
コラッツ予想について、証明を考えてみました。
ご指摘ご意見ご感想など、ぜひよろしくお願いします。
0324成清 愼
2015/10/07(水) 17:02:10.88ID:Zf+iS+sK修正しました
0325成清 愼
2015/10/07(水) 17:24:32.75ID:Zf+iS+sK3x-1では、奇数間増大がピークアウトした直後の奇数がまた別の奇数間増大の始まりとなっている
これが 5→7→5 でも 17が55でピークアウトした直後の41が 91でピークアウトする
奇数間増大の開始にあたっていて、奇数間増大、ピークアウト、一回減少、別の奇数間増大
を繰り返しこの5→7→5または 17→91→17へ入ってくるのです。これは単純計算で求まります。
0326成清 愼
2015/10/07(水) 17:35:39.40ID:Zf+iS+sK4（4a)+1 は更に増大します。これは 8b+1→12b+1でピークアウトする
のですが、12b+1＝4(3b)+1でまた増大の始まりとなります。
0327成清 愼
2015/10/07(水) 17:51:52.76ID:Zf+iS+sKとなっています。5（増大開始）→7（ピーク）→5（増大開始）
0328成清 愼
2015/10/07(水) 20:07:44.38ID:Zf+iS+sKしかし拙論も途轍もなく恐ろしいものを含んでいますよ。ぜひご一読を。
0329１３２人目の素数さん
2015/10/08(木) 00:59:03.02ID:xCcSc+Wz１、予想どおり１に収束する
２、無限大に発散する
３、ある数でループする、あるいは、ある複数の数たちでループする
ほかにはどんな場合が…？
0330成清 愼
2015/10/08(木) 14:14:14.07ID:DvdtsMd3他にはどんな場合もありません
0331成清 愼
2015/10/08(木) 14:27:35.48ID:DvdtsMd3その証拠に3x+1も1→1でループするのは同じです。
ただ、奇数間増大のピークを奇数間増大のピーク以外を解決済みに
しておいてから、奇数間増大のピークを小さい方から調べていけば自分より
小さいピークは解決済みとできるのが3x+1問題なのであって、すべて1→1
のループに至るというのが結論です。3x-1問題では1から逆に辿っていくと、
5も7も17も到達できないことが解り、アレッ？と思うでしょう。（もっとも全数をチェックできるわけは
ないが）
0332成清 愼
2015/10/08(木) 14:40:11.97ID:DvdtsMd31から逆に辿ることによって増加分は或る範囲に限定されるので積み重ねに
よって無限に至るまでチェックできます。
0333成清 愼
2015/10/08(木) 15:21:31.07ID:DvdtsMd3拙論に出てくるg(h(a,q),c)は具体的に書くと、初項が4ａ+3または8a+1
、漸化式がX(n+1)=X(n)×4+1 の奇数列で、さらに具体的に書くと
4a+3,16a+13,64a+53,256a+213.... および8a+1,32a+5,128a+21,512a+85...
となるので、貴論でいうbit pattern of left edge は拙論の 2^n・aの部分が
それですね。
0334成清 愼
2015/10/08(木) 16:01:14.13ID:DvdtsMd3が必ず存在します（nは 2a+1→.....2b+1 の間で２で割り切れた回数の通算、mは3倍して1を足した回数）
（逆も真）。しかしながら 2^n・b+2a+1＝2・3＾m・b+2c+1としても2^2n・b+2a+1≠2・3＾2m・b+2c+1だからループできないので
b=0しかループできない。しかも2a+1≠2c+1でもあるからこれもループできない。
それでは一体b=0で表せる範囲とは一体何なんだ。ここを追及していくと拙論のような
ものになるのです。畏れ多くもフェルマー大先生の無限降下法の逆で無限上昇方とでもいうべき
考え方を含んでいます。
0335成清 愼
2015/10/08(木) 16:20:06.79ID:DvdtsMd3によってどんどん狭まっていきます。コラッツ予想の題意の反対の演算
によってどんどん拡大していきます。この範囲というのが単純な大小関係では
表せないだけで抽象的な大小関係を想定すればいくら拡大しても無限上昇法
でループが存在しないことが言える。2^n・b+2a+1>2a+1が単純な大小関係では
なくこの抽象的な大小関係も表すようにこの抽象的大小関係というものを規定して
やることが必要です。
0336成清 愼
2015/10/12(月) 16:24:12.10ID:888izrM7http://koubeichizoku.doujin.so/collatz/collatze2.htm
0337成清 愼
2015/10/13(火) 13:13:54.28ID:Me85tfuaV1→V2→V3……→Vn-1 とループせずに来れば、Vn-1の次に来るVnが
V2,V3,……Vn-1の何れでもあり得ないことは簡単に言えます。
（これらはいずれもVn-1の次ではないから）
ただ問題はVｎ＝V1 ではないかという疑いだけです。拙論では
V1＝∞という状況を作り出した上でそれでもVnは今まで出てきた奇数では
あり得ないということを論旨の中心に据えました
0338１３２人目の素数さん
2015/10/13(火) 14:32:04.56ID:b/GXrfdWどんなよそうなの?
0339成清 愼
2015/10/13(火) 14:43:40.58ID:Me85tfuaを繰り返すと1になる。という予想です。
https://ja.wikipedia.org/wiki/%E3%82%B3%E3%83%A9%E3%83%83%E3%83%84%E3%81%AE%E5%95%8F%E9%A1%8C
0340１３２人目の素数さん
2015/10/13(火) 16:43:34.40ID:b/GXrfdWありがとうございます。
0341成清 愼
2015/10/16(金) 02:44:52.33ID:0s37cJmA> DD++さんへのお返事です。
>
以下省略
http://koubeichizoku.doujin.so/collatz/collatz3.htm
大幅改定いたしました。
i(a,q)がどのL(a',q')に含まれるかという事を考えるのはやめました。かわりに
相異なるCola(a,q)を実行することは、相異なるG(h(a,q))をi(a,q)を含むL(a',q')に、下から
積み重ねていく、まるで南部俵積唄みたいな作業なんだと考えることとしました。
これでも任意のL(a,q)は相異なるG(h(a',q'))の直和集合であり、全正奇数の真部分集合である。
任意のL(a,q)は重複元を持たない。
また任意のL(a,q)とL(a',q')は互いに素である。以上が成立することに変りはありません。
http://koubeichizoku.doujin.so/collatz/collatz3.htm
0342成清 愼
2015/10/16(金) 05:44:46.29ID:0s37cJmAg(h(a,1),1)=8a+1, g(h(a,1),2)=32a+5, g(h(a,1),3)=128a+21 g(h(a,1),4)=512a+85 ....
で、 g(x,n+1)=4・g(x,n)+1
i(a,1)=6a+1 i(a,0)=6a+5
j(g(h(a,q),c)→i(a,q) は全射であるが、単射ではない、
G(h(a,q)):={g(h(a,q),c|c=1,2,3,...∞}
j(v∈G(h(a,q)))=i(a,q) j-1[i(a,q)]=G(h(a,q)) i(a,q)→G(h(a,q))全単射
添字集合G(h(a,q))を1個の数のように扱ってしまえばこれら剰余類の間のせめぎ合いも
かなり抽象化されて量子化のカオスのような状態から抜け出せるような気がしてなりません。
個々の特性は一切無視して、とにかく任意のG(h(a,q))は全正奇数の真部分集合であり、
i(a,q)を媒介として直和された相異なるG(h(a,q))の直和集合もまた全正奇数の真部分集合で、
互いに素であると言うところだを強烈にガン見するわけです。
0343righ1113 ◆OPKWA8uhcY
2015/11/21(土) 16:27:32.22ID:7bk9f0suって去年も書いた気がするな。
0344１３２人目の素数さん
2015/12/24(木) 09:39:21.19ID:RbV5bbUg反証が見つかると思うんだけどなぁ。無限に大きくなるようなものは見つからないだろうけど
ループする奴はどこかにあるような？
0345１３２人目の素数さん
2015/12/24(木) 18:35:08.93ID:OsvuPr+Xどうぞどうぞ
0346１３２人目の素数さん
2015/12/24(木) 20:34:54.35ID:OsvuPr+Xそのループはこれこれの条件を満たさなければいけない
みたいな結果はどれくらいあるの？
0347１３２人目の素数さん
2015/12/25(金) 13:40:55.32ID:oZAW5C+C4m+3型の奇数であることは言える。
0348１３２人目の素数さん
2015/12/31(木) 07:23:24.61ID:o5hkKHBbhttp://deweger.xs4all.nl/papers/%5B35%5DSidW-3n+1-ActaArith%5B2005%5D.pdf
結果だけ言うと
整数で、3倍して1足したすぐ後に2回以上2で割れる操作が68回以下のものはない
って論文で、
2回以上2で割れると元の数よりは小さくなので、割って減少する回数は少なくとも69回以上あるってことだ
しかも、この論文古いからもっと回数は増えてるかもな
0349righ1113 ◆OPKWA8uhcY
2016/05/04(水) 12:36:28.41ID:Mm3dg5Gj0350１３２人目の素数さん
2016/05/06(金) 21:07:36.87ID:K2vLIneFそれからコラッツのほうは進展あったのか？
0351１３２人目の素数さん
2016/05/06(金) 23:54:12.83ID:3f8xb+Klhttp://integers.hatenablog.com/entry/2016/04/19/234355
0352tai
2016/05/10(火) 07:11:52.36ID:2mzzv61vの一番した
test12.pdf
がコラッツ予想の
の半分の証明です
上のほうは
リーマン予想の証明だったりする
自分では考えまくった
と思います
間違っている可能性もあります
0353righ1113 ◆OPKWA8uhcY
2016/05/14(土) 14:13:06.71ID:IrWcxE2T僕のほうは>>323でコラッツ予想の証明を完成しています。
他に、別の方が、>>352で、コラッツ予想がLoopしない証明を載せています。
0354１３２人目の素数さん
2016/05/14(土) 17:25:00.57ID:kAt1eCb5英語8ページか…意外と短い
余力があれば日本語版もオナシャス
0355１３２人目の素数さん
2016/05/14(土) 18:02:52.16ID:kAt1eCb5素人の俺には証明に穴がないか検証するのは難しいが、
Coqで証明が検証されたとなれば信頼度がだいぶ変わってくる。
Coq
https://ja.wikipedia.org/wiki/Coq
0356righ1113 ◆OPKWA8uhcY
2016/05/15(日) 14:07:43.39ID:HMT90KXlしばらく考えさせて下さい。
0357１３２人目の素数さん
2016/05/15(日) 18:22:03.00ID:xV6S1y8i0358righ1113 ◆OPKWA8uhcY
2016/05/16(月) 18:06:23.91ID:+2bpW1Z1思い付きもしなかったもんで。
0359１３２人目の素数さん
2016/05/16(月) 18:52:31.06ID:dTU5tRHRまあ数板にスレがあるから行ってみれ
寂れてるけど
0360tai
2016/05/21(土) 17:56:40.84ID:BTQQe4FH奇数の完全数がないことまで
同様の手法で示せました
http://taibuturi.fuma-kotaro.com/
0361￥ ◆2VB8wsVUoo
2016/05/21(土) 19:05:38.20ID:mdtcfbbU0362￥ ◆2VB8wsVUoo
2016/05/21(土) 19:05:57.78ID:mdtcfbbU0363￥ ◆2VB8wsVUoo
2016/05/21(土) 19:06:18.11ID:mdtcfbbU0364￥ ◆2VB8wsVUoo
2016/05/21(土) 19:06:37.18ID:mdtcfbbU0365￥ ◆2VB8wsVUoo
2016/05/21(土) 19:06:54.61ID:mdtcfbbU0366￥ ◆2VB8wsVUoo
2016/05/21(土) 19:07:15.12ID:mdtcfbbU0367￥ ◆2VB8wsVUoo
2016/05/21(土) 19:07:33.61ID:mdtcfbbU0368￥ ◆2VB8wsVUoo
2016/05/21(土) 19:07:52.69ID:mdtcfbbU0369￥ ◆2VB8wsVUoo
2016/05/21(土) 19:08:11.74ID:mdtcfbbU0370￥ ◆2VB8wsVUoo
2016/05/21(土) 19:08:28.08ID:mdtcfbbU0371￥ ◆2VB8wsVUoo
2016/05/22(日) 01:04:30.30ID:Q+2nNM8l0372righ1113 ◆OPKWA8uhcY
2016/05/22(日) 16:09:42.64ID:As5SZbzk0373righ1113 ◆OPKWA8uhcY
2016/05/22(日) 16:19:17.83ID:As5SZbzkRequire Import Coq.Program.Wf.
Require Import Omega.
Program Fixpoint collatz03 (x y : nat) {measure y} : list nat :=
match y with
| 0 => 0::nil
| _ => match x with
| 0 => 0::nil
| 1 => 1::nil
| _ => if Nat.odd x then (3*x+1) :: collatz03 (3*x+1) (y-1)
else (x/2) :: collatz03 (x/2) (y-1)
end
end.
Next Obligation.
omega.
Qed.
Next Obligation.
omega.
Qed.
ここまでで3日かかりました。www
0374righ1113 ◆OPKWA8uhcY
2016/05/22(日) 16:22:31.37ID:As5SZbzkEval compute in collatz03 9 20
→
Result for command Eval compute in collatz03 9 20 . :
= (28
:: 14
:: 7
:: 22
:: 11
:: 34
:: 17
:: 52
:: 26
:: 13
:: 40
::
20
::
10
::
5
::
16
::
8
::
4
::
2 :: 1 :: 1 :: nil)%list
: list nat
0375１３２人目の素数さん
2016/05/22(日) 16:49:26.93ID:mkl5wCNjもしCoqで証明が成功したらマジですごい。
Coqスレの1である片山博文MZも仲間に引き入れられれば
色々教えてもらえるかもね。
0376１３２人目の素数さん
2016/05/24(火) 02:04:08.25ID:xIwNaKmuところどころ何が言いたいかよくわからんが、とりあえず明確な間違いが一つ。
mod p^2 で
1 + p = n(l + kp)
より
nl = 1(mod p), nk = 1(mod p)
というところ。
nl = 1(mod p) は言えるが nk = 1(mod p) とは限らない。
例えば nl = p+1 の場合とか。
0377１３２人目の素数さん
2016/05/24(火) 10:35:07.76ID:WulNrhxx・ある自然数が100以下の素因数を持っていれば全て削る
・持ってなければ3n+1の操作を施す
みたいな問題から考えてくアプローチを思いついたんだけどこれって既出？
0378￥ ◆2VB8wsVUoo
2016/05/24(火) 10:50:07.49ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0379１３２人目の素数さん
2016/05/24(火) 19:49:39.12ID:ISALUQi7多分初めてだとおもうが、なにか成果が出そうなのか？
0380tai
2016/05/24(火) 21:39:24.40ID:374dBI4aありがとう
気づかなかった
間違いですね
0381￥ ◆2VB8wsVUoo
2016/05/24(火) 22:31:29.99ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0382１３２人目の素数さん
2016/05/24(火) 22:58:34.15ID:+Z6NkEEQや、まだ全然。多分簡単な問題から始めたら解決の糸口見つかるかなーと思ったけど
コラッツ問題の闇の深さを垣間見ることになっただけだった…
もし興味ある人いたら考えてみてくれ
0383￥ ◆2VB8wsVUoo
2016/05/24(火) 22:59:49.43ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0384￥ ◆2VB8wsVUoo
2016/05/24(火) 23:00:06.58ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0385￥ ◆2VB8wsVUoo
2016/05/24(火) 23:00:23.53ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0386￥ ◆2VB8wsVUoo
2016/05/24(火) 23:00:41.20ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0387￥ ◆2VB8wsVUoo
2016/05/24(火) 23:00:58.88ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0388￥ ◆2VB8wsVUoo
2016/05/24(火) 23:01:17.09ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0389￥ ◆2VB8wsVUoo
2016/05/24(火) 23:02:01.29ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0390￥ ◆2VB8wsVUoo
2016/05/24(火) 23:02:18.83ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0391￥ ◆2VB8wsVUoo
2016/05/24(火) 23:17:55.21ID:98ujCcPg0392￥ ◆2VB8wsVUoo
2016/05/24(火) 23:18:14.02ID:98ujCcPg0393tai
2016/05/24(火) 23:38:41.03ID:374dBI4aまだ途中ですので
まちがっているかもしれません
0394￥ ◆2VB8wsVUoo
2016/05/24(火) 23:54:36.02ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0395￥ ◆2VB8wsVUoo
2016/05/24(火) 23:54:53.79ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0396￥ ◆2VB8wsVUoo
2016/05/24(火) 23:55:08.89ID:98ujCcPg>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った疑いで、
>8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に
>逮捕されました。
>
>性犯罪者 増田哲也の供述
>「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」
>
0397righ1113 ◆OPKWA8uhcY
2016/05/25(水) 20:06:38.89ID:EB6pp118Theorem 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.
0398righ1113 ◆OPKWA8uhcY
2016/05/31(火) 13:18:55.66ID:MldWQZrVLemma 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.
0399righ1113 ◆OPKWA8uhcY
2016/05/31(火) 13:46:31.08ID:MldWQZrVLemma 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.
0400１３２人目の素数さん
2016/05/31(火) 16:43:04.58ID:Q9drQ/Ad正直すぐ投げ出すんじゃないかと侮っていたよ。
0401righ1113 ◆OPKWA8uhcY
2016/05/31(火) 23:37:09.87ID:5ZwDxW8hCoqで証明できると楽しいです。
0402righ1113 ◆OPKWA8uhcY
2016/06/04(土) 21:52:45.29ID:1pZXMfoL>>323の僕の証明の流れは、次のようになっています。
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からやっていこうと思います。
0403righ1113 ◆OPKWA8uhcY
2016/06/04(土) 22:01:11.07ID:1pZXMfoL前提として、コラッツパターンXsよりシミュレーションAが大きい、というのがあります。
理由は、コラッツパターンの下位からの繰り上がりがあったりなかったりするのに対して、
シミュレーションAは、常に下位からの繰り上がりがあるからです。
なので、pxs=log Xs - bit + aが成り立つのですが、前述の理由によりa>=0です。
（これは>>323には書いてないです。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)]が示せました。
0404righ1113 ◆OPKWA8uhcY
2016/06/04(土) 22:03:58.52ID:1pZXMfoL前提として、シミュレーションBより左端を伸ばすパターンが大きい、というのがあります。
理由は、左端を伸ばすパターンの下位からの繰り上がりがあったりなかったりするのに対して、
シミュレーションBは、常に下位からの繰り上がりがないからです。
なので、pys=log Ys - bit - aが成り立つのですが、前述の理由によりa>=0です。
（これは>>323には書いてないです。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は以上になります。
0405righ1113 ◆OPKWA8uhcY
2016/06/05(日) 18:56:49.96ID:yXCfmuqWビット数はbit=10です。
xsAの0ステップ目を1111111111、ysBの0ステップ目を0000000001として
（ずれが0で一番差が開いている数）ステップを重ねると、
xsAは115ステップ目が3ステップ目と一致して以後繰り返しになります。
xsBは93ステップ目が3ステップ目と一致して以後繰り返しになります。
その区間の最上位繰り上がりの可否を、大きい繰り返しになるまで調べます。
Haskellでやった時は、ずれの最大値は2でした。
Coqはこれからやります。
0406righ1113 ◆OPKWA8uhcY
2016/06/07(火) 16:41:02.76ID:MtRwR70UxsAの0ステップ目を1111111111、ysBの0ステップ目を0000000001として
（ずれが0で一番差が開いている数）ステップを重ねると、
xsAは113ステップ目が2ステップ目と一致して以後繰り返しになります。
xsBは91ステップ目が2ステップ目と一致して以後繰り返しになります。
colPattAの第二要素でHaskellとCoqでdiffを取ったので大丈夫だと思います。
0407righ1113 ◆OPKWA8uhcY
2016/06/07(火) 16:45:19.93ID:MtRwR70UTheorem 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.
これで小さい繰り返しはクリアできました。
0408righ1113 ◆OPKWA8uhcY
2016/06/07(火) 20:12:15.58ID:MtRwR70Uずれが際限なく増えていきます。
0409１３２人目の素数さん
2016/06/07(火) 20:14:39.10ID:KJBV85MD0410righ1113 ◆OPKWA8uhcY
2016/06/07(火) 21:33:31.73ID:MtRwR70Uありがとうございます。がんばります。
0411righ1113 ◆OPKWA8uhcY
2016/06/07(火) 22:06:33.54ID:MtRwR70UcolPattAは繰り返しの項数が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)))))).
0412righ1113 ◆OPKWA8uhcY
2016/06/07(火) 22:32:18.95ID:MtRwR70U0413１３２人目の素数さん
2016/06/07(火) 23:18:10.94ID:KJBV85MDそれならそれで面白いが。
0414righ1113 ◆OPKWA8uhcY
2016/06/08(水) 00:37:23.48ID:JADn1FP5それをCoqに落とし込むのに手間取っています。
0415righ1113 ◆OPKWA8uhcY
2016/06/08(水) 02:03:36.44ID:JADn1FP5>>237-238を見て、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.もできました。
0416righ1113 ◆OPKWA8uhcY
2016/06/08(水) 09:39:08.70ID:JADn1FP5>>237-238の手計算も間違っていました。
ビット数を増やすという切り札があるので、それをやってみます。
Coqはウソつかないんですねー
0417413
2016/06/08(水) 21:39:10.48ID:lYAR2M8u0418１３２人目の素数さん
2016/06/08(水) 22:23:08.13ID:WkHIclqp0419righ1113 ◆OPKWA8uhcY
2016/06/08(水) 23:36:44.69ID:aPj7A/ik0420１３２人目の素数さん
2016/06/09(木) 02:17:55.30ID:Z2BPqjfW何をいまさら。こんなやり方でコラッツの予想が解けるわけがない。
0421１３２人目の素数さん
2016/06/09(木) 19:53:16.16ID:OutW5kLLCoqがあれば間違った証明は通らないだろうしいくらでも頑張れる環境がある。
コラッツの予想が解けるのは時間の問題だな。
0422righ1113 ◆OPKWA8uhcY
2016/06/10(金) 05:50:42.64ID:oOXw5TlH5bitで考えて、さらに命題を一つ考えます。
（★）「下位からの繰り上がりは、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なのはご容赦を。
0423１３２人目の素数さん
2016/06/11(土) 01:05:42.63ID:p56I7Ltoどっちも難しそうだが。
■ このスレッドは過去ログ倉庫に格納されています
ニュース
- 【テレビ】時速30キロ厳守の出川が走ると大渋滞発生…テレ東「充電させてもらえませんか？」は以前から問題視されていた！ [ネギうどん★]
- 【MLB】カブス・今永昇太が7回3安打無失点の好投で開幕5連勝 デビュー6先発の防御率0.78は歴代4位 [フォーエバー★]
- 30分並んで確保した新幹線の自由席、子連れに「席譲ってください」と言われたけど譲るべき…？ ★5 [おっさん友の会★]
- 【MLB】大谷翔平 33試合目で今季初となる休養日、前日は今季初の3三振 直近5試合では打率.227 [阿弥陀ヶ峰★]
- 「ハリポタ」主演ラドクリフさん、原作者のトランス嫌悪「本当に悲しい」 [少考さん★]
- 「頂き女子りりちゃん」名古屋高裁に控訴…懲役９年・罰金800万円の判決に不服 ★2 [少考さん★]
- 速報:アメリカ、日本を中露と共に排外主義国に認定。バイデン大統領が表明 [246620176]
- 【画像】愛知県に人が住んでる離島があることが発覚。何があんのここ [389296376]
- 自民議員「快適ドライブイェイ！」スピードメーター「91km/h」が写ってしまう(制限速度60km/h) [256556981]
- 「大谷のスタメン落ちはただの休養です！安心してください！」という速報記事が出る [973994793]
- 遺体をバレずに処理する方法 何を思いついた？ [205023192]
- しょぼいうんこばかり出る(⁠´⁠；⁠ω⁠；⁠｀⁠)