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

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

[前50を表示]
300:１３２人目の素数さん
15/09/14 04:20:25.24 H0h+jyLY.net
（3ｘ+1）ではg(h(a,q),1)≫i(a,q)が全単射で、g(h(a,q),1）∈J(g(h(a,q),1))⇒c≠1⇒g(h(a,q),c）●J(g(h(a,q),1))　（●は元としての存在否定の記号）
が言えるので命題1を補足すれば事足りると思われます。

301:成清　愼
15/09/14 04:25:05.64 H0h+jyLY.net
↑名前入れ忘れたので１３２人目の素数になってしまいました

302:成清　愼
15/09/14 04:46:52.71 H0h+jyLY.net
91と17が同一のループ状にあるのは、きっとこのループの中に
v∈G'(x)とv''∈G'(x)が同居しているからだと思われます（G'は（3x-1）問題における（3ｘ+1）問題でのG集合に相当する集合）
なので精査してみます。

303:righ1113 ◆OPKWA8uhcY
15/09/14 19:12:18.53 z7+1bsMM.net
なんか進んでるー
こっちはarXivに投稿できねえええ
endorserなんてシステムがあるんですね。

304:成清　愼
15/09/15 05:35:12.62 wrjEOZ4l.net
g(h(a,q),c)またはi(a,q)の qという変数は　0または1の値をとるとしているが、
これを　-1　か　1　に組み替えれば　どうも（3ｘ+1）問題と　（3ｘ-1）問題の
全体で可換群を成すような予感が・・・・

305:成清　愼
15/09/15 05:45:16.93 wrjEOZ4l.net
どうも（3ｘ-1）問題における正体は　G’の逆関数　2^n×i(a,q)+1 , 特に
i(a,q)=1がその鍵を握っているようですね。(3x+1)問題では補足に書いた
2^n×i(a,q)-1がこれに当たります。

306:成清　愼
15/09/15 05:53:22.50 wrjEOZ4l.net
【誤】（3ｘ-1）問題における正体は→【正】（3ｘ-1）問題におけるループの正体は

307:成清　愼
15/09/15 06:15:57.72 wrjEOZ4l.net
>>269
ほんとにすばらしいアドバイスを頂いて有難うございます。
(3ｘ+1）問題と　（3ｘ-1）問題の比較をやってみるとほんとに何から何まで
正反対の性質をもっていることに驚愕します。おかげで眼前がパッと開けた感じです。
中央西線が姥捨でら善光寺平の上に出てきたような。北陸自動車が関東平野を見下ろす位置に
あるいは飛騨高山→富山ルートが富山平野の上に出てきたような感じです。
城崎と宇宙に近いかも！？

308:１３２人目の素数さん
15/09/15 19:05:44.14 Y/dQxT4l.net
3ｘ-1問題は、結局の所3ｘ+1のマイナス領域ってだけだからな
3ｘ+1問題、3ｘ-1問題の両者が証明できれば、
3ｘ+1問題が正負全ての整数で証明されることになる

309:成清　愼
15/09/16 03:01:43.99 PqGg73Tt.net
{(2^n-1)*3-1} - [{(2^(n+1)-1)*3-1}/2] = -1
{(2^n+1)*3+1} - [{(2^(n+1)+1)*3+1}/2] = 1
これらの問題が増大部分で形づくる渦のような図形（これをフィボナッチ
数列による渦といって、ヒマワリの種の並びや巻貝に現れているらしい）
この渦の内側の線と一つ外側の線の間の幅が3ｘ-1と3ｘ+1では2の差がある
つまり内外の間隔が両者では前者が小さい。曲率も小さい？つまり縮小版？

310:成清　愼
15/09/16 03:24:32.97 PqGg73Tt.net
現象部分では÷（2＾2）なので両者は等しい。
奇数間の　≫+（増大）が継続する部分を1単位として考えこの間の
奇数の集合をZ(n)とすると、全奇数で、
∃Z(n)∩∃Z(n')＝{}で、ループすればループ内にこのZ(n)が何個以内
でなくてはならないのかはハジける。

311:成清　愼
15/09/16 03:25:36.68 PqGg73Tt.net
【誤】現象→【正】減少

312:成清　愼
15/09/16 03:43:47.99 PqGg73Tt.net
ルッ！ループ自体が加群を成してる！！

313:成清　愼
15/09/16 03:51:08.15 PqGg73Tt.net
=IF(MOD(○,2)=1,○*3-1,○/2)
EXCEL、 ○　は直前のセルへの参照　これは調査ツールとして便利

314:成清　愼
15/09/16 06:02:44.07 PqGg73Tt.net
297>>
∃Z(n)∩∃Z(n')＝{} (互いに素)　だけではダメで
互いに　同一のG（x）のメンバー　を含まない（（3ｘ-1）の場合　ｇ（ｘ,y）は
ｇ：　初項ｘ、漸化式a(n+1)=a(n)×4-1　の第　ｙ項　）
、　が言えれば
ループが存在しないことが言える。が実際に（3ｘ-1）の場合はこれが存在する。
多分計算で導ける。

315:成清　愼
15/09/16 06:10:34.32 PqGg73Tt.net
2＾n + 1≫2＾(n-1)/・3 + 1≫2＾(n-2)/・3＾2 + 1
・・・ 2・3＾n + 1

316:成清　愼
15/09/16 06:16:18.16 PqGg73Tt.net
ループ1からループ2が導けて加群を成すことを証明してくれ。
健闘を祈る。

317:成清　愼
15/09/16 08:49:56.49 PqGg73Tt.net
2＾n + 1が減少に転じたその先をxとする、2＾(n+1） + 1　はもう一回
≫+となる、でその先は　4X-1だから　同じG'のメンバーだ。
だんだん熱くなってきた　汗;　気温は低いのにったくご苦労さんな奴がいるよなあ！（自分）

318:成清　愼
15/09/16 08:56:49.92 PqGg73Tt.net
↑今のとこの調査では　これは減少時2＾2で割り切れて奇数となった場合
例えば2＾4で割り切れた場合はランデブーもっと先伸ばしになる。

319:成清　愼
15/09/16 09:12:51.31 PqGg73Tt.net
例えば17≫♯91の例で言えば途中に出てくる41という数が
ループの外側から91に向かう途中に出てくる一例である163という数が　
41×4-1＝163だから　やはり　41×4-1＝163で、41と163は同一G'のメンバー同志だ。
この理由も同じだろう。♪(＾^)v

320:成清　愼
15/09/16 09:36:53.40 PqGg73Tt.net
同一のG(X)が存在しないことを明示的に表するために、
J(g(h(a,q)),c)の代わりに、J(x):={G(a,q)|…}を使おう。

321:成清　愼
15/09/16 09:47:41.05 PqGg73Tt.net
【誤】2＾n + 1≫2＾(n-1)/・3 + 1≫2＾(n-2)/・3＾2 + 1
・・・ 2・3＾n + 1
↓
【正】 2＾n + 1≫2＾(n-1)・3 + 1≫2＾(n-2)・3＾2 + 1
・・・ 2・3＾n + 1

322:成清　愼
15/09/16 13:58:29.81 PqGg73Tt.net
(3ｘ+1)でも扱いが一番難しかった“≫+と≫-の境目に位置する”という
カテゴリーの奇数を表す式が(3ｘ-1)ではg(h(a,q),c)の第二項以降を表す
式と一致してる。

323:成清　愼
15/09/16 14:03:35.44 PqGg73Tt.net
命題1の同一のGのメンバー同志は同一のJの中で同居できないというのは
(3ｘ+1)では正解である可能性が出てきた。

324:成清　愼
15/09/16 14:15:57.35 PqGg73Tt.net
　k[i(a,q)]-1=G(h(a,q)) （ -1は反対写像を表す）だからです。
Cola（g（ｈ(a,0),1）)が実行された後にはじめてほかのGメンバーとJ（i(a,q)）
で同居します。(3ｘ+1)で“≫+と≫-の境目に位置する”という
カテゴリーの奇数はを　g（ｈ(2a,0),1）で、これはG数列　g（ｈ(a,q),c）（C＞1）
の範疇の数ではないからです

325:成清　愼
15/09/16 14:25:36.64 PqGg73Tt.net
(3ｘ-1)ではこの“≫+と≫-の境目に位置する”という数が(h(a,q),c)の第二項以降を表す
式と一致してる。
なので　5≫7≫5のようなことが起こり得る（ループの外からタイミングをずらして5に合流してくる7×4-1）という数がある
というわけです。(3ｘ+1)には例えば　3≫5　13≫5　の時　13≫3　は存在し得ないのです。
これがループ問題における(3ｘ-1)と(3ｘ-1)の違いです。

326:成清　愼
15/09/16 14:44:27.62 PqGg73Tt.net
渦巻きを伴ったツリーというのはグラフに書くとどうなるのかな？
2.5のフラクタル次元かな？

327:成清　愼
15/09/17 02:36:37.60 +B+tCG1t.net
合流する位置が一つ下方へずれてるせいか？あるいはまたループ自体が加群を成しているために
合流してもその先に1以外のループが存在しないからなのか？おそらくその両方が原因だろう。

328:成清　愼
15/09/17 02:57:27.38 +B+tCG1t.net
（2×3＾n±1）×4●1　（●は±の上下反転）　
(3ｘ+1)問題だけ考えていたときはループをもっとずうとお気楽に考えていた。
何度でも言うけどホントに非常に興味深い命題を与えてくれて感謝します。
奇数間増大シークェンスがピークアウトした数がnが一つ下のシークエンスに
合流する位置がその後最初に減少する時に２で何回割れるかによるため（3ｘ+1）
では比較的近くに現れるのに、（3X+1）はｎが大きくなるとだんだん≫回数が
増えていくこれは増加率の問題だろう。

329:成清　愼
15/09/17 03:15:25.37 +B+tCG1t.net
ところでフェルマーの定理を解決したワイルズは燃え尽きちゃったんだろうか？
大学は栄養士とエクササイズのインストラクターをつけて体調管理して
もう一働きしてもらえばいいのに。彼ならリーマンゼータの零点問題を
解決できると思うが。

330:１３２人目の素数さん
15/09/17 04:38:12.24 U4vMfCYB.net
ここ Twitter じゃないんだけど？

331:成清　愼
15/09/18 05:23:18.38 EYAHLKQv.net
へっ！コラッツの問題は結局は同一のGのメンバーがどこにあるのかと言う命題だったんだ

332:成清　愼
15/09/18 05:25:59.32 EYAHLKQv.net
317>>
独白につぐ独白、つぶやきにつぐつぶやきで自分の考えを纏めていく
癖をお許し下さい。

333:１３２人目の素数さん
15/09/26 06:42:33.08 CXVd2x7J.net
3x-1問題では　2^n・ｙ+1　が奇数間増大の開始点（yは3で割り切れない奇数）で
、これが n-1 回奇数間増大を繰り返し、2・3＾(2-1)+1でピークアウトする。
で、ｙが4a+1 ならばピークアウト後3倍して1を引くと2回2で割り切れる。
2割り切れた数をｚとすれば、
2^(2n）・ｙ+1におけるｚは　2^(2n+1）・ｙ+1がピークアウトした数の
G数列（漸化式　b(n+1)=b(n)・4-1　で表される数列）の一つ項番が少ない
数である。つまりこの二つの奇数間増大シークェンスはピークアウト後必ず合流する
。(3x+1)問題においては開始点が　2^n・ｙ-1、　漸化式　b(n+1)=b(n)・4+1であって
この辺の様相が全く異なる。

334:成清　愼
15/09/26 06:44:48.04 CXVd2x7J.net
↑文責は私

335:成清　愼
15/09/26 07:44:13.12 CXVd2x7J.net
拡大していくエントロピー（情報の不確実性と同義）を必死こいて低く押しとどめようとする姿は
麻雀の摸打と同じだな。

336:righ1113 ◆OPKWA8uhcY
15/09/27 12:02:07.17 4GZ0rplU.net
こちらも証明が完成したのでupしました。
URLﾘﾝｸ(drive.google.com)
良かったら見てみて下さい。

337:成清　愼
15/10/07 17:02:10.88 Zf+iS+sK.net
URLﾘﾝｸ(koubeichizoku.doujin.so)
修正しました

338:成清　愼
15/10/07 17:24:32.75 Zf+iS+sK.net
ご指摘のとおり、3ｘ-1問題との違いについて考えてみました。
3x-1では、奇数間増大がピークアウトした直後の奇数がまた別の奇数間増大の始まりとなっている
これが　5→7→5　でも　17が55でピークアウトした直後の41が　91でピークアウトする
奇数間増大の開始にあたっていて、奇数間増大、ピークアウト、一回減少、別の奇数間増大
を繰り返しこの5→7→5または　17→91→17へ入ってくるのです。これは単純計算で求まります。

339:成清　愼
15/10/07 17:35:39.40 Zf+iS+sK.net
3ｘ-1では奇数間増大は｛(4a+1)×3-1｝÷2＝6a+1　です
4（4a)+1　は更に増大します。これは　8b+1→12b+1でピークアウトする
のですが、12b+1＝4(3b)+1でまた増大の始まりとなります。

340:成清　愼
15/10/07 17:51:52.76 Zf+iS+sK.net
41→61→91（ピーク）→17（55までの増大開始）→55（ピーク）→41（増大開始）
となっています。5（増大開始）→7（ピーク）→5（増大開始）

341:成清　愼
15/10/07 20:07:44.38 Zf+iS+sK.net
この問題は心底、戦慄を覚える、ほんとうに恐ろしい問題です。
しかし拙論も途轍もなく恐ろしいものを含んでいますよ。ぜひご一読を。

342:１３２人目の素数さん
15/10/08 00:59:03.02 xCcSc+Wz.net
結果は
１、予想どおり１に収束する
２、無限大に発散する
３、ある数でループする、あるいは、ある複数の数たちでループする
ほかにはどんな場合が…？

343:成清　愼
15/10/08 14:14:14.07 DvdtsMd3.net
329>>
他にはどんな場合もありません

344:成清　愼
15/10/08 14:27:35.48 DvdtsMd3.net
3x+1も3x-1も本質的に同じだというのはご指摘の通りだと思います。
その証拠に3x+1も1→1でループするのは同じです。
ただ、奇数間増大のピークを奇数間増大のピーク以外を解決済みに
しておいてから、奇数間増大のピークを小さい方から調べていけば自分より
小さいピークは解決済みとできるのが3x+1問題なのであって、すべて1→1
のループに至るというのが結論です。3x-1問題では1から逆に辿っていくと、
5も7も17も到達できないことが解り、アレッ？と思うでしょう。（もっとも全数をチェックできるわけは
ないが）

345:成清　愼
15/10/08 14:40:11.97 DvdtsMd3.net
もっとも全数をチェックできるわけはないが→コラッツ予想とその類題は
1から逆に辿ることによって増加分は或る範囲に限定されるので積み重ねに
よって無限に至るまでチェックできます。

346:成清　愼
15/10/08 15:21:31.07 DvdtsMd3.net
323>>
拙論に出てくるg(h(a,q),c)は具体的に書くと、初項が4ａ+3または8a+1
、漸化式がX(n+1)=X(n)×4+1 の奇数列で、さらに具体的に書くと
4a+3,16a+13,64a+53,256a+

347:213.... および8a+1,32a+5,128a+21,512a+85... となるので、貴論でいうbit pattern of left edge は拙論の　2^n・aの部分がそれですね。

348:成清　愼
15/10/08 16:01:14.13 DvdtsMd3.net
3x+1問題では　2a+1→.....2c+1　が存在すれば　2^n・b+2a+1 →.....2・3^m・b+2c+1
が必ず存在します（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で表せる範囲とは一体何なんだ。ここを追及していくと拙論のような
ものになるのです。畏れ多くもフェルマー大先生の無限降下法の逆で無限上昇方とでもいうべき
考え方を含んでいます。

349:成清　愼
15/10/08 16:20:06.79 DvdtsMd3.net
b＝0でしか表せない範囲というのはコラッツ予想の題意のとおりの演算
によってどんどん狭まっていきます。コラッツ予想の題意の反対の演算
によってどんどん拡大していきます。この範囲というのが単純な大小関係では
表せないだけで抽象的な大小関係を想定すればいくら拡大しても無限上昇法
でループが存在しないことが言える。2^n・b+2a+1>2a+1が単純な大小関係では
なくこの抽象的な大小関係も表すようにこの抽象的大小関係というものを規定して
やることが必要です。

350:成清　愼
15/10/12 16:24:12.10 888izrM7.net
英文も作成しました
URLﾘﾝｸ(koubeichizoku.doujin.so)

351:成清　愼
15/10/13 13:13:54.28 Me85tfua.net
V2,V3,……Vn-1,Vｎを奇数とした時
V1→V2→V3……→Vn-1 とループせずに来れば、Vn-1の次に来るVnが
V2,V3,……Vn-1の何れでもあり得ないことは簡単に言えます。
（これらはいずれもVn-1の次ではないから）
ただ問題はVｎ＝V1　ではないかという疑いだけです。拙論では
V1＝∞という状況を作り出した上でそれでもVnは今まで出てきた奇数では
あり得ないということを論旨の中心に据えました

352:１３２人目の素数さん
15/10/13 14:32:04.56 b/GXrfdW.net
誰か簡単に説明してくれ。
どんなよそうなの?

353:成清　愼
15/10/13 14:43:40.58 Me85tfua.net
全ての正整数は2で割り切れたら2で割る、割り切れなかったら3倍して1を足す
を繰り返すと1になる。という予想です。
URLﾘﾝｸ(ja.wikipedia.org)

354:１３２人目の素数さん
15/10/13 16:43:34.40 b/GXrfdW.net
>>338
ありがとうございます。

355:成清　愼
15/10/16 02:44:52.33 0s37cJmA.net
空舟さんへのお返事です。
> DD++さんへのお返事です。
>
以下省略
URLﾘﾝｸ(koubeichizoku.doujin.so)
大幅改定いたしました。
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')は互いに素である。以上が成立することに変りはありません。
URLﾘﾝｸ(koubeichizoku.doujin.so)

356:成清　愼
15/10/16 05:44:46.29 0s37cJmA.net
g(h(a,0),1)=4a+3, g(h(a,0),2)=16a+13, g(h(a,0),3)=64a+53 g(h(a,0),4)=256a+213 ....
g(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個の数のように扱ってしまえばこれら剰余類の間のせめぎ合いも
かなり

357:抽象化されて量子化のカオスのような状態から抜け出せるような気がしてなりません。個々の特性は一切無視して、とにかく任意のG(h(a,q))は全正奇数の真部分集合であり、 i(a,q)を媒介として直和された相異なるG(h(a,q))の直和集合もまた全正奇数の真部分集合で、互いに素であると言うところだを強烈にガン見するわけです。

358:righ1113 ◆OPKWA8uhcY
15/11/21 16:27:32.22 7bk9f0su.net
今日こたつを出しました。
って去年も書いた気がするな。

359:１３２人目の素数さん
15/11/23 18:07:22.24 /Bgrn41sa
（１からｎまでの自然数の交代和⇒1-2+3-...）=f(n) =1/4(1-(2n+1))(-1)^n
とする。

n+f(n)+f(n+f(n))+f{n+f(n)+f(n+f(n))}+...(1)

コラッツ予想の操作は上記のf(n)に関する入れ子構造についての無限和を取る事
と同値である。
ここまでは完璧に分かったから、
(1)式の一般項
全てのｎについての極限値
これらを求めてくれ

360:１３２人目の素数さん
15/12/24 09:39:21.19 RbV5bbUg.net
反証を見つけた方が早そうだ。
反証が見つかると思うんだけどなぁ。無限に大きくなるようなものは見つからないだろうけど
ループする奴はどこかにあるような？

361:１３２人目の素数さん
15/12/24 18:35:08.93 OsvuPr+X.net
>>344
どうぞどうぞ

362:１３２人目の素数さん
15/12/24 20:34:54.35 OsvuPr+X.net
例えば１，２，４のループ以外でループがあるとして、
そのループはこれこれの条件を満たさなければいけない
みたいな結果はどれくらいあるの？

363:１３２人目の素数さん
15/12/25 13:40:55.32 oZAW5C+C.net
１，２，４のループ以外では、ループする場合の最小の奇数は、
4m+3型の奇数であることは言える。

364:１３２人目の素数さん
15/12/31 07:23:24.61 o5hkKHBb.net
>>346
URLﾘﾝｸ(deweger.xs4all.nl)
結果だけ言うと
整数で、3倍して1足したすぐ後に2回以上2で割れる操作が68回以下のものはない
って論文で、
2回以上2で割れると元の数よりは小さくなので、割って減少する回数は少なくとも69回以上あるってことだ
しかも、この論文古いからもっと回数は増えてるかもな

365:righ1113 ◆OPKWA8uhcY
16/05/04 12:36:28.41 Mm3dg5Gj.net
今日こたつをしまいました。

366:１３２人目の素数さん
16/05/06 21:07:36.87 K2vLIneF.net
いまさらこたつとかおそいよもっと早くしまえ。
それからコラッツのほうは進展あったのか？

367:１３２人目の素数さん
16/05/06 23:54:12.83 3f8xb+Kl.net
いつ示されてるのか知らんがこんな話がある
URLﾘﾝｸ(integers.hatenablog.com)

368:tai
16/05/10 07:11:52.36 2mzzv61v.net
URLﾘﾝｸ(taibuturi.fuma-kotaro.com)
の一番した
test12.pdf
がコラッツ予想の
の半分の証明です
上のほうは
リーマン予想の証明だったりする
自分では考えまくった
と思います
間違っている可能性もあります

369:righ1113 ◆OPKWA8uhcY
16/05/14 14:13:06.71 IrWcxE2T.net
>>350
僕のほうは>>322でコラッツ予想の証明を完成しています。
他に、別の方が、>>352で、コラッツ予想がLoopしない証明を載せています。

370:１３２人目の素数さん
16/05/14 17:25:00.57 kAt1eCb5.net
>>353
英語8ページか…意外と短い
余力があれば日本語版もオナシャス

371:１３２人目の素数さん
16/05/14 18:02:52.16 kAt1eCb5.net
例えば、>>322の証明をCoqで検証するとかいうのはやってみる気ない？
素人の俺には証明に穴がないか検証するのは難しいが、
Coqで証明が検証されたとなれば信頼度がだいぶ変わってくる。
Coq
URLﾘﾝｸ(ja.wikipedia.org)

372:righ1113 ◆OPKWA8uhcY
16/05/15 14:07:43.39 HMT90KXl.net
すごいことになってる。
しばらく考えさせて下さい。

373:１３２人目の素数さん
16/05/15 18:22:03.00 xV6S1y8i.net
すごいことって何かあったのか？

374:righ1113 ◆OPKWA8uhcY
16/05/16 18:06:23.91 +2bpW1Z1.net
いえ、Coqで検証なんて、
思い付きもしなかったもんで。

375:１３２人目の素数さん
16/05/16 18:52:31.06 dTU5tRHR.net
Coqはめちゃくちゃ難しいぞ
まあ数板にスレがあるから行ってみれ
寂れてるけど

376:tai
16/05/21 17:56:40.84 BTQQe4FH.net
スレ違いですが
奇数の完全数がないことまで
同様の手法で示せました
URLﾘﾝｸ(taibuturi.fuma-kotaro.com)

377:￥ ◆2VB8wsVUoo
16/05/21 19:05:38.20 mdtcfbbU.net
￥

378:￥ ◆2VB8wsVUoo
16/05/21 19:05:57.78 mdtcfbbU.net
￥

379:￥ ◆2VB8wsVUoo
16/05/21 19:06:18.11 mdtcfbbU.net
￥

380:￥ ◆2VB8wsVUoo
16/05/21 19:06:37.18 mdtcfbbU.net
￥

381:￥ ◆2VB8wsVUoo
16/05/21 19:06:54.61 mdtcfbbU.net
￥

382:￥ ◆2VB8wsVUoo
16/05/21 19:07:15.12 mdtcfbbU.net
￥

383:￥ ◆2VB8wsVUoo
16/05/21 19:07:33.61 mdtcfbbU.net
￥

384:￥ ◆2VB8wsVUoo
16/05/21 19:07:52.69 mdtcfbbU.net
￥

385:￥ ◆2VB8wsVUoo
16/05/21 19:08:11.74 mdtcfbbU.net
￥

386:￥ ◆2VB8wsVUoo
16/05/21 19:08:28.08 mdtcfbbU.net
￥

387:￥ ◆2VB8wsVUoo
16/05/22 01:04:30.30 Q+2nNM8l.net
￥

388:righ1113 ◆OPKWA8uhcY
16/05/22 16:09:42.64 As5SZbzk.net
Coq、気長にやってみます。

389:righ1113 ◆OPKWA8uhcY
16/05/22 16:19:17.83 As5SZbzk.net
手始めにコラッツ数列を計算する関数。
Require 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

390:righ1113 ◆OPKWA8uhcY
16/05/22 16:22:31.37 As5SZbzk.net
クエリで
Eval 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

391:１３２人目の素数さん
16/05/22 16:49:26.93 mkl5wCNj.net
頑張れ～
もしCoqで証明が成功したらマジですごい。
Coqスレの1である片山博文MZも仲間に引き入れられれば
色々教えてもらえるかもね。

392:１３２人目の素数さん
16/05/24 02:04:08.25 xIwNaKmu.net
>>360
ところどころ何が言いたいかよくわからんが、とりあえず明確な間違いが一つ。
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 の場合とか。

393:１３２人目の素数さん
16/05/24 10:35:07.76 WulNrhxx.net
流れぶったぎってすまんが
・ある自然数が100以下の素因数を持っていれば全て削る
・持ってなければ3n+1の操作を施す
みたいな問題から考えてくアプローチを思いついたんだけどこれって既出？

394:￥ ◆2VB8wsVUoo
16/05/24 10:50:07.49 98ujCcPg.net
￥
>性犯罪者の増田哲也（50歳・東京都足立区千住寿町）が
>8月4日にＪＲ牟岐線の列車内で、午後4時20分ごろから約50分にわたり、
>徳島県内の女性（21歳・専門学校生）の胸や太ももなどを触った

395:疑いで、 >8月5日未明、県迷惑行為防止条例違反（痴漢行為）容疑で徳島県警阿南署に >逮捕されました。 > >性犯罪者　増田哲也の供述 >「夏休み期間に、講演活動を兼ねて旅行していた。好みの女性だったのでムラムラした」 >

396:１３２人目の素数さん
16/05/24 19:49:39.12 ISALUQi7.net
>>377
多分初めてだとおもうが、なにか成果が出そうなのか？

397:tai
16/05/24 21:39:24.40 374dBI4a.net
>>376
ありがとう
気づかなかった
間違いですね

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

399:１３２人目の素数さん
16/05/24 22:58:34.15 +Z6NkEEQ.net
>>379
や、まだ全然。多分簡単な問題から始めたら解決の糸口見つかるかなーと思ったけど
コラッツ問題の闇の深さを垣間見ることになっただけだった…
もし興味ある人いたら考えてみてくれ

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.

次ページ