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

[0001 １３２人目の素数さん 2023/03/09(木) 21:33:04.72 ID:v8QzyA/x]

いわゆる『コラッツの問題』『3n+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
※前スレ
コラッツ予想がとけたらいいな　その３
https://rio2016.5ch.net/test/read.cgi/math/1631191485/

[0304 １３２人目の素数さん 2023/08/20(日) 14:01:45.06 ID:VnAdAaOb]

>>303
> 　
> ・ 帰納法の中で一番最初に「有限長である」と証明される DivList(x) は何か？
> 普通に DivList(3) が一番最初でいいのか？
Yes です。

> ・ 帰納法の中で二番目に「有限長である」と証明される DivList(x) は何か？
> 普通に DivList(9) が二番目でいいのか？
Yes です。

> ・ DivList(27) が有限長であることの証明を、
> 論文内の手法で実際に書き下してみてください。
しばしお待ちください。

[0305 １３２人目の素数さん 2023/08/20(日) 14:14:25.45 ID:VnAdAaOb]

>>304
> ・ DivList(27) が有限長であることの証明を、
> 論文内の手法で実際に書き下してみてください。

27 は 14パターンのうちの No.6 です。

・DivList(27)が有限長であること
FirstLimited 27 を証明したいとします。
帰納法の仮定より、27 > 21 である FirstLimited 21 は言えます。
次に関数 firstToAll を使って FirstLimited 21 を AllLimited 21 に変えます。
AllLimited 21 の中に、FirstLimited 27 は含まれるので（そうなるように AllLimited 21 を作ってあります）、
それを取り出して証明完了です。

[0306 １３２人目の素数さん 2023/08/20(日) 14:24:31.70 ID:XCKG3A1v]

>>305
＞ AllLimited 21 の中に、FirstLimited 27 は含まれるので

ここが分からない。AllLimited 21 の中で具体的に何をしているのか？
DivList(21) に拡張スター変換を行うと DivList(27) が出てくるということ？
No6 の

> 108t+27　CF[4,1,-2]　y=8x/9-3　96t+21

を使って、DivList(21) から DivList(27) を出力しているということ？

[0307 １３２人目の素数さん 2023/08/20(日) 14:40:14.00 ID:VnAdAaOb]

>>306
意味分からなくても良いので見てください。プログラムの一部抜粋です。
-----
(S (S ((u + u) + (u + u)))) | Even | Even
= let x = (S (S ((u + u) + (u + u))))
in [[2, -4] `dsp` divSeq (12*x+7), [4, -4] `dsp` divSeq (3*x+2), [1, -2] `dsp` divSeq (6*x+3), [3, 0, -4] `dsp` divSeq (18*x+13), [3, -1, -2] `dsp` divSeq (9*x+6)]
-----
AllLimited は、上の数が欲しい FirstLimited を全て内蔵しています。
＞ AllLimited 21 の中に、FirstLimited 27 は含まれるので
AllLimited 21 が内蔵しているもののうち、FirstLimited 27 を取り出せる、ということです。

[0308 １３２人目の素数さん 2023/08/20(日) 14:45:15.92 ID:XCKG3A1v]

>>307
基本的なことなんだけど、質問したい。

一般に、DivList(x) の長さを｜DivList(x)｜で表記することにする。
たとえば、DivList(7) ＝ [1, 1, 2, 3, 4] は長さ5なので

｜DivList(7)｜＝5

ということになる。さて、DivList(x) に1回のスター変換を施したものを
DivList(y) とする。このとき、論文内で言及されているように、

｜DivList(y)｜＝｜DivList(x)｜＋λ　(ただしλ＝ 0 or 1 )

が成り立つ。

[0309 １３２人目の素数さん 2023/08/20(日) 14:46:18.02 ID:XCKG3A1v]

すると、DivList(27) に拡張スター変換

＞ 108t+27　CF[4,1,-2]　y=8x/9-3　96t+21

を使って DivList(21) を出力した場合だと、C,Fの2回しか変換してないので、

｜DivList(21)｜＝｜DivList(27)｜＋λ　(ただしλ＝ 0 or 1 or 2 )　…(*)

が成り立つはず。しかし、DivList(21) ＝ [6] なので ｜DivList(21)｜＝1 であり、
一方で DivList(27) は長大な列なので｜DivList(27)｜はデカイ値であり、
(*)が成り立たない。

どういうこと？

[0310 １３２人目の素数さん 2023/08/20(日) 15:01:28.01 ID:VnAdAaOb]

>>309
このときの DivList(21) は、DivList(27) に CF[4,1,-2] を施して、
　DivList(21) = [4, 1, -2長いの......](これも割数列です)
となり、
　｜DivList(21)｜＝｜DivList(27)｜＋λ　(ただしλ＝ 0 or 1 or 2 )　…(*)
は成り立たちます。

拡張star変換を導入した時点で、コラッツ値に対する割数列の一意性は崩れます。

[0311 １３２人目の素数さん 2023/08/20(日) 15:09:20.01 ID:XCKG3A1v]

>>310

＞ DivList(21) = [4, 1, -2長いの......](これも割数列です)

DivList(x)＝[a_1,a_2,…] の各 a_i は「2でa_i回割り算する」という
意味だったはず。すると、

DivList(21) = [4, 1, -2長いの......]

の場合、-2 が出てきた時点で「4を掛け算する」という意味になってしまう。
そういう解釈でいいってこと？

[0312 １３２人目の素数さん 2023/08/20(日) 15:12:14.27 ID:VnAdAaOb]

>>311
その解釈で OK です。

[0313 １３２人目の素数さん 2023/08/20(日) 15:17:47.65 ID:XCKG3A1v]

>>312
じゃあ、

DivList(21) = [4, 1, -2長いの......]

を実際に展開してみると、

21 → (21 * 3＋1) / 4 ＝ 16 → 8 → 32 → (…) → 27

になるってこと？21から出発してるのに、27 に化けるってこと？

[0314 １３２人目の素数さん 2023/08/20(日) 15:20:15.08 ID:XCKG3A1v]

いや、こうか。

21 → (21 * 3＋1) / 4 ＝ 16 → (16 * 3＋1) / 2 ＝ 49/2

→ (3 * (49/2)＋1) * 4 ＝ 298 → (…) → 27

もはや途中で分数が出現してるんだけど、それでいいの？

[0315 １３２人目の素数さん 2023/08/20(日) 15:36:23.32 ID:VnAdAaOb]

>>314
こうなります。
　 　 27[1,2,1,1,1,1,2,...]
　CF[4,1,-2]
　21[4,1,-1,2,1,1,1,1,2,...]

27 を一回コラッツ計算した値は 41。

21 を一回コラッツ計算した値は 4。
21 を二回コラッツ計算した値は 13/2。
21 を三回コラッツ計算した値は 41。一致する。

[0316 １３２人目の素数さん 2023/08/20(日) 15:46:18.65 ID:XCKG3A1v]

>>315
つまり、

27 → … → 41
21 → … → 41

となって、同じ41に合流するわけか。

[0317 １３２人目の素数さん 2023/08/20(日) 15:48:22.92 ID:XCKG3A1v]

となれば、

・ x から始まるコラッツ変換だと 1 に到達する。
・ y から始まるコラッツ変換は、途中で z を経由し、しかも最終的には別のループに到達する。
・ x から出発して分数を経由しながら>>315の要領で変換して z にできる。

もしこのような x, y, z が存在するなら、x からも y からも z に合流し、
そして z の先には 1 以外の別のループがあることになる。つまり、

・ もともとの DivList(x) は有限長だが、DivList(y) から
　 拡張スター変換を行って DivList(x) にした場合は、
　 その DivList(x) は無限長である

という状況になる。割数列の一意性は既に崩れているのだから、
このような状況になっても、おかしいところはない。

あなたのロジックは破綻しているのでは？

[0318 １３２人目の素数さん 2023/08/20(日) 16:12:43.61 ID:qXuvhtZR]

そもそもこんなスレに居るやつが証明できるのか？というメタな話

[0319 １３２人目の素数さん 2023/08/20(日) 16:18:41.92 ID:VnAdAaOb]

>>317
コラッツが成り立っていない世界の記述ですよね。
コラッツが成り立っていない世界については、そういう事も起こると思います。

特段、自身の証明に打撃は無いと思います。

[0320 １３２人目の素数さん 2023/08/20(日) 16:19:17.87 ID:yi5M+4Hc]

それはそうなんだけどどこまで近づけるかも大事

[0321 １３２人目の素数さん 2023/08/20(日) 16:21:49.82 ID:XCKG3A1v]

>>318
いや、論文として通ってるんだよ。

ttps://www.scirp.org/journal/paperinformation.aspx?paperid=115471

ちなみに、「リーマン予想を証明した」と
主張しているように見える論文が過去に何度も通ってたりする。

ttps://www.scirp.org/journal/articles.aspx?searchcode=proof+of+riemann&searchfield=All&page=1&skid=0

[0322 １３２人目の素数さん 2023/08/20(日) 16:24:53.38 ID:XCKG3A1v]

>>319
＞コラッツが成り立っていない世界については、そういう事も起こると思います。

つまり、こういうことね？

・ コラッツ予想が成り立ってる世界では、あなたのロジックは破綻しない。
・ コラッツ予想が成り立ってない世界では、あなたのロジックは破綻する。

だったら、あなたのロジックが破綻してないことを示すには、まず最初に

「この世界はコラッツ予想が成り立っている世界である」

ことを先回りして証明しておかなければならない。

で、その証明はどこにあるの？

[0323 １３２人目の素数さん 2023/08/20(日) 16:28:32.50 ID:VnAdAaOb]

>>322
破綻するとまでは言っていません。

>>317 を要約すると
「コラッツ予想が偽であれば、割数列の片方が有限長で、もう一方が無限長であるようなコラッツ値が存在する」
であって、この命題が自身の証明に影響を与えるとは思えません。

[0324 １３２人目の素数さん 2023/08/20(日) 16:31:20.30 ID:XCKG3A1v]

>>323
あなたのロジックのどこが破綻しているのかを、具体的に指摘してみる。

まず、割数列の一意性は既に崩れているので、DivList(x) は、
一般的には複数の表現を持ち得る。その具体例は

DivList(21) ＝ [6], [4,1,-1,2,1,1,1,1,2,...]

というもの。
つまり、DivList(21) を表現する列は [6] だけではなく、
[4,1,-1,2,1,1,1,1,2,...] という列もまた、
DivList(21) を表現する列になっている。

実際には、もっとたくさんの表現を持つだろう。
無限通りの表現を持つ可能性だってある。

[0325 １３２人目の素数さん 2023/08/20(日) 16:32:26.64 ID:XCKG3A1v]

そして、割数列の表現が一意的でない以上、

「 DlivList(x) は有限長である 」

という文章は、

「 DivList(x) を表現する "任意の列" が有限長である 」

という意味になる。しかし、あなたが定義した AllLimited x では、
そのような任意の列が有限長であることを証明しているようには見えない。
たまたま出くわした一部の表現が有限長であることを
確認しているだけではないのか？

[0326 １３２人目の素数さん 2023/08/20(日) 16:33:31.76 ID:XCKG3A1v]

たとえば DivList(9) の場合だと、帰納法の初期の段階では、
DivList(9) を表現する列はせいぜい2〜3種類が限度だろうから、
その時点での AllLimited 9 は、それら2〜3種類の表現に対して
「有限長である」を確認すれば終わってしまうことになる。

しかし、帰納法が進めば進むほど、拡張スター変換によって DivList(9) に
到達しやすくなるので、DivList(9) を表現する列のレパートリーが増えていく。

そのような無数の列が全て有限長であることを、
本来なら帰納法の初期の段階で AllLimited 9 によって
先回りして完全に証明してなければならないのだが、
そんな証明が成されているようには見えない。

[0327 １３２人目の素数さん 2023/08/20(日) 16:34:07.10 ID:XCKG3A1v]

結局、この論文の中で実際に証明されていることは、

「 DivList(x) を表現する複数の列のうち、少なくとも1つの列は有限長である」

ということにすぎないのでは？これなら、証明が通ってもおかしくない。

しかし、それが証明できたところで、コラッツ予想が証明できたことには
なってない。

[0328 １３２人目の素数さん 2023/08/20(日) 16:48:19.93 ID:VnAdAaOb]

>>327
https://github.com/righ1113/collatzProof_DivSeq/wiki/img/collatz230820.JPG

>>298 も見てほしいのですが、
AllLimited x の先頭要素(first)には、拡張star変換を使っていない一番単純な「完全割数列」というものを配置しています。
この「完全割数列」が有限長であることを FirstLimited x で表現します。
FirstLimited x が真であることは、純粋な「完全割数列」が有限長であることを示すので、コラッツ予想も真になります。

[0329 １３２人目の素数さん 2023/08/20(日) 16:56:28.07 ID:XCKG3A1v]

>>328
その>>298によれば、

＞ AllLimited x　は x の完全割数列に加えて拡張完全割数列全ても有限長であるという述語です。

と書かれているが、一方であなたは

＞ AllLimited は、上の数が欲しい FirstLimited を全て内蔵しています。

とも主張していた。結局、AllLimited には何が内蔵されているのか？

ここでは AllLimited 3 について質問したい。
この中に内蔵されている FirstLimited x 及び拡張完全割数列を、
全て列挙してみてください。

[0330 １３２人目の素数さん 2023/08/20(日) 17:02:19.76 ID:VnAdAaOb]

>>329
すみませんが宿題にさせてください。

[0331 １３２人目の素数さん 2023/08/20(日) 17:07:06.89 ID:XCKG3A1v]

>>330
はい。お待ちしてます。

[0332 １３２人目の素数さん 2023/08/20(日) 19:28:40.54 ID:XCKG3A1v]

追記。

x＝27 にスター変換Fを適用してみる。この x は 9 の倍数かつ奇数だから、
x に Fを適用することは可能である。変換後は y＝8x/3−3＝69 になる。
そして、両者の純粋な DivList は次のようになる。

DivList(x) ＝ [1,2,1,1,1,1,2,2,…]
DivList(y) ＝ [4,3,4]

一方で、変換Fにより [a_1, a_2, a_3...] → [5, a_1 - 2, a_2, a_3...]
となるらしいので、この場合の DivList(y) は

DivList(y) ＝ [5,-1,2,1,1,1,1,2,2,…]

になる。つまり、スター変換を1回しか使ってないのに、この時点で既に

DivList(y) ＝ [4,3,4], [5,-1,2,1,1,1,1,2,2,…]

という2種類の表現が得られてしまう。意味が分からない。

[0333 １３２人目の素数さん 2023/08/20(日) 19:32:59.24 ID:XCKG3A1v]

・ 変換Fは、x を y＝8x/3−3 に変換するだけであり、
　 x,y それぞれに対する割数列は、常に純粋な割数列が使われる

という立場なのであれば、そもそも [a_1, a_2, a_3...] → [5, a_1 - 2, a_2, a_3...]
という変換は成り立たない。逆に、

・ 変換Fは、純粋な DivList(x) を [a_1, a_2, a_3...] と表すときに、
　 [5, a_1 - 2, a_2, a_3...] という別の数列を割り当てる変換である

という立場なのであれば、変換後の [5, a_1 - 2, a_2, a_3...] が、
どんな初期値 z に対する純粋な割数列であるのか不明になる。
論文の中では y＝8x/3−3 と置いていて、あたかも この y に対する
純粋な割数列が [5, a_1 - 2, a_2, a_3...] であるかのように
書かれているが、>>332 に書いたように、そんなことは成り立たない。

[0334 １３２人目の素数さん 2023/08/20(日) 19:42:38.57 ID:XCKG3A1v]

つまり、x から y＝8x/3−3 への変換と、
[a_1,a_2,a_3,…] から [5, a_1 - 2, a_2, a_3...] への変換は、
x,yに対する「純粋な割数列」の観点からは全く整合性がないので、
両者を並列して表記しても、何の意味があるのか分からない。

[0335 １３２人目の素数さん 2023/08/21(月) 07:18:30.83 ID:czjDYREv]

>>331
AllLimited 3 です。
AllLimited 3 = [
　[1, 4], コラッツ値3と完全割数列
　[2, -4] `dsp` [3,2,3,4], コラッツ値45
　[3, 0, -4] `dsp` [2,3,1,1,5,4], コラッツ値81
　[4, -4] `dsp` [1,1,1,5,4], コラッツ値15
　[1, -2] `dsp` [6], コラッツ値21
　[3, -1, -2] `dsp` [1,1,2,1,4,1,3,1,2,3,4] ] コラッツ値39　からお呼ばれする
`dsp` は拡張star変換を接続する関数です。

[0336 １３２人目の素数さん 2023/08/21(月) 07:19:47.34 ID:czjDYREv]

>>332-334
star変換の時点では、割数列の要素が 0 や負になるものは禁止です。
27[1,2,1,1,1,1,2,2,…] に、F[5,-2] で変換することは禁止です。

この場合 27 を y＝8x/3－3 で 69 に変えられますが、これに意味はありません。

[0337 １３２人目の素数さん 2023/08/21(月) 15:18:38.57 ID:XO2eOtqP]

>>336
意味が分からない。変換Fが適用できる x の条件は

・ x は3の倍数かつ奇数かつ x≡0 (mod 9)

だったはず。論文の中にはそのように明記されている。
x＝27 はこの条件を満たすのだから、27 に対して
Fを適用することは可能のはず。

[0338 １３２人目の素数さん 2023/08/21(月) 15:19:39.67 ID:XO2eOtqP]

しかも、「27 は 14パターンのうちの No.6 です」と
あなたは発言している。具体的には

＞ 108t+27　CF[4,1,-2]　y=8x/9-3　96t+21

これである。t＝0 とすれば x＝27 の場合に相当し、

・ 27 に変換 F を適用したあと変換 C を適用すると 21 になる

という意味になる。実際、27にF,Cの順番で適用すれば、確かに21になる。
しかし、あなたによれば、27 に F を適用するのは禁止だと言う。

だったら、27 にCFを適用することもできない。
なんたって、まず 27 に F を適用できないのだから。

どういうこと？

[0339 １３２人目の素数さん 2023/08/21(月) 15:24:51.07 ID:XO2eOtqP]

ちょっと話が前後するが、変換Fの謎が解けた。

定義：x は整数で、[a_1,a_2,a_3,…] は整数の有限列または無限列とする。もし

・ x_0＝x, x_{i＋1}＝(3x_i＋1)/2^{a_i} で定義される x_i について、
　 ある n≧1 に対して x_n＝1 が成り立つ(途中の x_i が分数になっていても構わない)

が成り立つならば、ペア(x, [a_1,a_2,a_3,…])は
整合的であると呼ぶことにする。

[0340 １３２人目の素数さん 2023/08/21(月) 15:25:54.09 ID:XO2eOtqP]

具体例：x から決まる純粋な割数列 DivList(x) が有限長のとき、
ペア (x, DivList(x)) は自明に整合的である。

[0341 １３２人目の素数さん 2023/08/21(月) 15:27:33.83 ID:XO2eOtqP]

定理：xは奇数かつ3の倍数かつ x≡0 (mod 9) とする。
さらに、(x, [a_1,a_2,a_3,…]) は整合的とする。
このとき、(8x/3−3, [5, a_1 - 2, a_2,…]) は整合的である。

↑この定理が成り立つからこそ、変換Fでは 8x/3−3 と [5, a_1 - 2, a_2,…,a_n] を
並列して書いてたんだな。他の変換でも同じ定理が成り立つんだろう。

[0342 １３２人目の素数さん 2023/08/21(月) 15:29:19.95 ID:XO2eOtqP]

そうなると、やっぱり問題となるのはコレだな。

・ (x,[a_1,a_2,…])が整合的のとき、F変換後の
　 (8x/3−3, [5, a_1 - 2, a_2,…]) もまた整合的になるのは
　 それでいいとして、だからと言って、8x/3−3 からコラッツ変換を
　 繰り返していくと 1 に到達すると言えるのか？

つまり、純粋な割数列 DivList(8x/3−3) は有限長だと言えるのかってこと。
[5, a_1 - 2, a_2,…] と純粋な DivList(8x/3−3) は無関係なので、
(8x/3−3, [5, a_1 - 2, a_2,…]) が整合的であっても、
純粋な DivList(8x/3−3) が有限長かどうかは何も分からないはず。

[0343 １３２人目の素数さん 2023/08/21(月) 15:34:30.80 ID:czjDYREv]

>>337-338
論文には「If the original first term is negative, G[+6] is performed in advance.」
と書いてはいますが、明記はしてなかったです。すみません。

拡張star変換の時は、割数列の要素が 0 や負になるものを許可します。

[0344 １３２人目の素数さん 2023/08/21(月) 15:36:00.89 ID:XO2eOtqP]

で、話を戻す。

>>335
dsp の意味が不明瞭。たとえば、

＞ [2,-4] dsp [3,2,3,4], コラッツ値45

は

・ 純粋な割数列 DivList(45)＝[3,2,3,4] に E[2,-4] を適用した後の
　 値 y と数列 [b_1,b_2,…] については、有限長の列になっている

という意味でいいのか？この場合、>>335には全部で5個の
拡張割数列しか書かれていない。なぜ？

[0345 １３２人目の素数さん 2023/08/21(月) 15:36:34.85 ID:XO2eOtqP]

AllLimited x は、

「 x に対して拡張スター変換を行ったときの全ての拡張完全割数列も有限長」

という意味を内包していたはず。
なぜ AllLimited 3 には5個しか書かれてないのか？

拡張スター変換はA,B,C,D,E,F,Gを何度も適用できる(特にGは無制限)のだから、
x から出発して無限通りの拡張スター変換を試すことで、
奇数かつ3の倍数になる y をいくらでも生成できるはず。
すると、対応する拡張完全割数列も無限に出てくるはず。

なぜ AllLimited 3 では5個しか書かれてないのか？

[0346 １３２人目の素数さん 2023/08/21(月) 15:38:42.72 ID:XO2eOtqP]

あと、AllLimited x には

＞ AllLimited は、上の数が欲しい FirstLimited を全て内蔵しています。

という意味も含まれているとあなたは発言している。
しかし、AllLimited 3 には、FirstLimited については

・ FirstLimited 3

しか内蔵されてないように見える。これはどういうこと？

・AllLimited 3 に内蔵される FirstLimited は、FirstLimited 3 のみである

という認識で合ってる？

[0347 １３２人目の素数さん 2023/08/21(月) 16:16:53.39 ID:czjDYREv]

>>344
　[2, -4] `dsp` [3,2,3,4]
は
　[2,-1,2,3,4]
という拡張完全割数列になるという意味です。

>>345
証明では一回の拡張star変換を使うだけで、すべての 3の倍数の奇数 をまかなえます。（>>273 の chapter06 の表参照）なので
AllLimited 3 は、
　FirstLimited 45
　FirstLimited 81
　FirstLimited 15
　FirstLimited 21
　FirstLimited 39
を証明する時しか使わないので、AllLimited 3 では 5個 内蔵しています。

>>346
まず「FirstLimited 3」は内蔵しています。
そして、「FirstLimited」という形ではないですけど、AllLimited 3 では 5個 内蔵しています。
「[2, -4] `dsp` [3,2,3,4]」が有限長と分かっているから、「FirstLimited 45」も成り立つ、としています。

[0348 １３２人目の素数さん 2023/08/21(月) 17:34:29.10 ID:XO2eOtqP]

>>347
＞「[2, -4] `dsp` [3,2,3,4]」が有限長と分かっているから、
＞「FirstLimited 45」も成り立つ、としています。

意味が分からない。45 に対する純粋な割数列がそもそも [3,2,3,4] であり、
この時点で既に有限長であるから、[2,-4]とのdspを考えるまでもなく、
FirstLimited 45 が導出できている。つまり、

・ [3,2,3,4], コラッツ値45

と書いた時点で既に FirstLimited 45 が導出できているのであって、
[2, -4]とのdspは FirstLimited 45 を導出するのに何の役にも立ってない。

[0349 １３２人目の素数さん 2023/08/21(月) 17:35:35.94 ID:czjDYREv]

>>348
すみませんが宿題にさせてください。

[0350 １３２人目の素数さん 2023/08/21(月) 17:37:58.00 ID:XO2eOtqP]

別の言い方をすると、AllLimited 3 の中で一体どうやって

[3,2,3,4]

という数列を算出したのかということ。
まさか、初期値 45 から出発してコラッツ操作を直接計算することで

[3,2,3,4]

を出力したのか？もしそうなら、

「45からコラッツ操作で1に到達できることを先に確認して、
そのあとで [2,-4] との dsp を考えている(当然ながら、その結果は有限長)」

という順番になるので、推論の向きが逆。つまり、あなたは

「dspを施した後の列が有限長だから、45 の純粋な割数列も有限長」

を示したのでなくて、

「そもそも45の純粋な割数列が有限長だから、dspを施した後も有限長」

としか言ってないことになる。

[0351 １３２人目の素数さん 2023/08/21(月) 17:39:39.76 ID:XO2eOtqP]

なので、俺からの質問としては、次のようになる。

・ コラッツ値45に対して出力されている [3,2,3,4] は、
　AllLimited 3 の中で一体どのようなアルゴリズムによって
　出力されているのか？まさか、コラッツ操作を直接計算してるわけじゃないよね？

[0352 BLACKX ◆SvoRwjQrNc 2023/08/21(月) 21:03:49.94 ID:4xvTJKKA]

私への回答で手動だと回答あるよ
>>272

[0353 BLACKX ◆SvoRwjQrNc 2023/08/22(火) 02:44:44.05 ID:ygQrW8qm]

私がディオファントス的立場から考えるに
x.y.z.4の4が出てる時点で手動でしかないと思う
自己共役から洗い出すと最後が4になるのが奇数であることを示していて、あとは素数判別式で無理やり示すことは可能かと考えられるが、14パターンの変換式では直観的に網羅されてないはず(グラフ理論の観点から)
ちなみにグラフ理論では4パターン
整数→素因数分解にて半手動でair値取得

[0354 １３２人目の素数さん 2023/08/22(火) 07:53:11.48 ID:/h4GgIkE]

>>351
・べた書き
AllLimited 3 は、分かりやすさのため、[3,2,3,4]等ソースコードにべた書きしています。

・一般はこうやってます
一般化されたコードである
>>307 を見ると、（[2, -4] `dsp` divSeq (12*x+7),）等書いているのですが、
「divSeq (12*x+7)」が有限長かは分からないので、以下の方法を使っています。
（divseq は完全割数列を出力する関数ですが、定理証明においてこれが実際に動いている訳ではないです。）

・firstToAll
証明方針を再掲します。
> FirstLimited x を証明したいとします。
> 帰納法の仮定より、x>q である FirstLimited q は言えます。
> 次に＜関数 firstToAll＞ を使って FirstLimited q を AllLimited q に変えます。
> AllLimited q の中に、FirstLimited x(の素) は含まれるので（そうなるように AllLimited q を作ってあります）、
> それを取り出して証明完了です。

＜関数 firstToAll＞がここでのポイントです。
有限長であるFirstLimited q を入力とし、firstToAll をくぐり抜けて得られた AllLimited q は、
中身の全ての割数列の有限性を保証されています。（そういう firstToAll の作用です）
「dspを施した後の列が(firstToAllの作用により)有限長だから、45 の純粋な割数列も有限長」となっています。

このような計算方法になっています。
尚、firstToAll の存在は自明ではないので、firstToAll の正当性を定理証明したのが、>>263 の ”divseq2” となっております。

[0355 １３２人目の素数さん 2023/08/22(火) 08:09:22.05 ID:/h4GgIkE]

話題がプログラムの中身に移ってきたので、こちらのソースコードもご参照ください。
・旧版 Idris
https://github.com/righ1113/collatzProof_DivSeq/tree/master/program3
・新版 Lean 4
https://github.com/righ1113/divseq2

[0356 １３２人目の素数さん 2023/08/22(火) 08:20:56.56 ID:/h4GgIkE]

すいません、再投稿します。
話題がプログラムの中身に移ってきたので、こちらのソースコードもご参照ください。
・旧版 Idris（firstToAllに不備があります）
https://github.com/righ1113/collatzProof_DivSeq/tree/master/program3
・新版 Lean 4（スレの説明と一部関数名が変わっております）
https://github.com/righ1113/divseq2

[0357 １３２人目の素数さん 2023/08/22(火) 14:13:16.23 ID:oEBbQ4Sw]

>>354
いま問題にしているのは、

・ いかにして FirstLimited 45 が証明されていのか？

ということ。あなたは今回、

・ FirstLimited 3 から firstToAll を適用したタイミングで
　 FirstLimited 45 が証明されている

としか答えていない。firstToAll の中で具体的に何を行うことで
FirstLimited 45 に到達しているのか、その部分だけを抽出して、
紙の上で手書きで再現する形で提示してください。
プログラム丸投げじゃなくてね。

[0358 １３２人目の素数さん 2023/08/22(火) 14:21:09.01 ID:oEBbQ4Sw]

BaseCase である FirstLimited 3 については、
直接計算によって有限性が証明できる。
実際、3 に対する純粋な割数列は

DivList(3)＝[1,4]

と直接計算できて、これは有限長である。これに対して
firstToAll を適用すると、あなたの主張によれば

・ FirstLimited 45,81,15,21,39 が導出される

ということになる。

[0359 １３２人目の素数さん 2023/08/22(火) 14:21:10.14 ID:/h4GgIkE]

>>357
時間をください。

[0360 １３２人目の素数さん 2023/08/22(火) 14:23:02.40 ID:oEBbQ4Sw]

では、firstToAll の中で、具体的には何をしているのか？
せっかく拡張スター変換を導入したのだから、
例えば「39」の場合だと、「3」が「39」に変換されるような
拡張スター変換を使っているのではないか？つまり、

DivList(3)＝[1,4]

に対して拡張スター変換を適用して、

DivList(39)＝[b_1,b_2,…,b_k] (何らかの有限長の割数列)

という割数列に変換するのではないか？
そして、これが有限長であることを理由に、

・ 純粋な DivList(39) もまた有限長である

と推論しているのではないか？

[0361 １３２人目の素数さん 2023/08/22(火) 14:26:55.65 ID:oEBbQ4Sw]

もしそうなら、この推論が正しいとは思えない。
なぜなら、拡張スター変換後の

・ DivList(39)＝[b_1,b_2,…,b_k] (何らかの有限長の割数列)

は割数列の一意性が崩れているので、ここでの [b_1,b_2,…,b_k] は、
39 に対する純粋な割数列とは全くの別物だからだ。
これが有限長だからと言って、39 に対する純粋な割数列までもが
有限長であるとは推論できないはず。

[0362 １３２人目の素数さん 2023/08/22(火) 14:33:46.15 ID:oEBbQ4Sw]

上記の [b_1,b_2,…,b_k] が、39 の純粋な割数列と
「無関係」であることは、次のような事実からも容易に推察できる。
まず、39 の純粋な割数列は

DivList(39)＝[1,1,2,1,4,1,3,1,2,3,4] (長さ11)

である。長さが11もあるのだ。
一方で、BaseCase である DivList(3)＝[4,1] は、長さが2しかない。
これに拡張スター変換を1,2回適用したくらいでは、
長さがせいぜい＋4程度にしかならない。つまり、拡張スター変換後の

・ DivList(39)＝[b_1,b_2,…,b_k]

は、長さがせいぜい6程度にしかならない。
長さが11の本物の割数列とは全くの別者である。
両者の間に関係があるとは思えない。

[0363 １３２人目の素数さん 2023/08/23(水) 07:48:16.08 ID:jvofjEJg]

>>357
FirstLimited と AllLimited の定義（Lean 4 版）を一部示します。
inductive AllLimited : Nat → Prop where
| is : (l : Nat)
→ (AllLimited l)
→ (AllLimited succ (succ (succ (succ ((succ (l * 2 * 2)) * 3))))) -- 02★２
→ (AllLimited succ (succ (l*3))) -- 09
→ (AllLimited succ (succ (succ (l * 2 * 3)))) -- 11
→ (AllLimited 18*l+13) -- 03'★４
→ (AllLimited 9*l+6) -- 12'
　　　　......

inductive FirstLimited : Nat → Prop where
| is02 : (l : Nat) → (AllLimited l)★１ → (FirstLimited succ (succ (succ (succ ((succ (l * 2 * 2)) * 3)))))
| is03 : (m : Nat) → (AllLimited 2*m)★３ → (FirstLimited (m * 36 + 13))
......

[0364 １３２人目の素数さん 2023/08/23(水) 07:49:10.92 ID:jvofjEJg]

>>363
・おわび
(AllLimited z) というだけで、内蔵する割数列の有限性は保証されます。
なので、firstToAll が (AllLimited z)型を返すというだけで、内蔵する割数列の有限性は保証されます。

・firstToAll：前文
firstToAll の型(説明のようなもの)は以下のようになっています。
　firstToAll : (z : Nat) -> FirstLimited z -> AllLimited z
これは、「全ての z に対して、FirstLimited z なら、AllLimited z である」ということを表す関数です。
「z と FirstLimited z を引数に取って、AllLimited z を返す関数」とも言えます。

・「02」の場合
p=(FirstLimited z) として、場合分けをおこないます。
　match p with
　　| FirstLimited.is02 _ p2 => match p2 with
　　　| AllLimited.is _ _ p3 _ _ _ _ _ _ _ _ _ _ _ => p3
「02」というのが例の 14パターン の場合分けです。
02 の場合分けに入った時点で、求める答えは、(AllLimited z) ではなく (AllLimited succ (succ (succ (succ ((succ (l * 2 * 2)) * 3))))) に変化します。
「p2」には★１が入ります。その p2 でさらに場合分けをおこないます。
「p3」には★２が来て、計算をおこなうのですが、★１の「l」が★２の「l」に代入されて、そのまま
　(AllLimited succ (succ (succ (succ ((succ (l * 2 * 2)) * 3)))))
が出力されます。これが求めている答えになります。

[0365 １３２人目の素数さん 2023/08/23(水) 07:49:59.76 ID:jvofjEJg]

>>364
・「03」の場合
　match p with
　　| FirstLimited.is03 m p2 => match p2 with
　　　| AllLimited.is _ _ _ _ _ p3 _ _ _ _ _ _ _ _ => have p4 := Eq.subst (h₀₃ m) p3; p4
03 の場合分けに入った時点で、求める答えは、(AllLimited z) ではなく (AllLimited (m * 36 + 13)) に変化します。
「p2」には★３が入ります。その p2 でさらに場合分けをおこないます。
「p3」には★４が来て、計算をおこなうのですが、★３の「2*m」が★４の「l」に代入されて
　(AllLimited (m * 36 + 13))
が出力されます。これが求めている答えになります。have 以降は気にしないでください。

残りのパターンも同様におこないます。あくまで例の 14パターン が主軸です。

これが定理証明における firstToAll の説明です。
これで作られた firstToAll に (FirstLimited 3) を渡すと、(AllLimited 3) が返ってきます。
> AllLimited 3 = [
> 　[1, 4],　　　　　　　　　　　　　　　　　　　　コラッツ値3と完全割数列
> 　[2, -4] `dsp` [3,2,3,4],　　　　　　　　　　　　　コラッツ値45
> 　.....]
の中身が有限長だと分かったので、コラッツ値45 も有限長、FirstLimited 45 が得られます。

[0366 １３２人目の素数さん 2023/08/23(水) 13:49:54.26 ID:SzHPMf8P]

>>364
＞(AllLimited z) というだけで、内蔵する割数列の有限性は保証されます。

意味が分からない。額面通り

「 AllLimited z と書くだけで内蔵されている割数列の有限性が保証される」

のであれば、何の推論も適用せず、いきなり AllLimited 3 とか
AllLimited 9 とかを書くだけで終わってしまう。
極端なことを言えば、何の工夫もせずに

AllLimited 3, AllLimited 9, AllLimited 15, AllLimited 21, AllLimited 27, …

と順番に書いていくだけでいい。

[0367 １３２人目の素数さん 2023/08/23(水) 13:51:19.66 ID:SzHPMf8P]

この方針のもとでは、

∀n∈N s.t. AllLimited 3(2n＋1)

という命題を簡単に証明できる。実際、命題 P(n) を

P(n): AllLimited 3(2n＋1)

と書いた上で、

・ BaseCase の P(1)では、何も考えずに いきなり AllLimited 3 を書けばいい
・ P(n) が真という仮定のもとでは、何も考えずに いきなり AllLimited 3(2(n＋1)＋1) を書けばいい

という論証を行えば、それだけで ∀n∈N s.t. AllLimited 3(2n＋1)
という命題が証明できてしまう。

[0368 １３２人目の素数さん 2023/08/23(水) 13:52:09.13 ID:SzHPMf8P]

そのような行為をせずに、FirstLimited 3 から出発して
場合分けだの何だの推論を繰り返しているということは、
無条件で AllLimited z と書いただけでは
有限性が保証されないということだろう？

つまり、AllLimited z を呼び出すには、
その前にクリアしなければならない
何らかの「前提Ｘ」があるんだろう？

今回の目標は AllLimited 3 を呼び出すことなのだから、
これを呼び出すための前提Ｘを、先にクリアしておかなければ
ならないんだろう？

そのＸとは具体的には何？

[0369 １３２人目の素数さん 2023/08/23(水) 13:59:38.21 ID:SzHPMf8P]

＞「02」というのが例の 14パターン の場合分けです。
＞02 の場合分けに入った時点で、求める答えは、(AllLimited z) ではなく
＞(AllLimited succ (succ (succ (succ ((succ (l * 2 * 2)) * 3))))) に変化します。
＞「p2」には★１が入ります。その p2 でさらに場合分けをおこないます。

これも意味不明。例の14パターンの場合分けとは、

DivList(x) ＝ (何らかの有限長の割数列)

という表現に対して何らかの拡張スター変換を施して

DivList(y) ＝ (別の有限長の割数列)

を導出する操作のことを指している。14パターンのうち
どの操作が適用できるかは、x の値に応じて異なる。

[0370 １３２人目の素数さん 2023/08/23(水) 14:02:20.25 ID:SzHPMf8P]

今回の場合は BaseCase についての話であり、明示的に得られている
「 DivList(x) ＝ (何らかの有限長の割数列) 」は

DivList(3)＝[1,4]

のみである。従って、14パターンのうち、せいぜい2〜3通りの
パターンしか該当するパターンは存在しないはずである。
そのような2〜3通りのパターンに対して変換を施して

DivList(y) ＝ (別の有限長の割数列)

を導出できたとして、あなたはこれが有限長であることを根拠にして、
AllLimited y や FirstLimited y が真になることが理論的に
保証されると勘違いしているように見受けられる。
もしそうなら、それは間違っている。実際、拡張スター変換を
施した時点で割数列の一意性が崩れているので、

DivList(y) ＝ (別の有限長の割数列)

という表現が有限長であったとしても、y に対する
純粋な割数列までもが有限長であるとは言えないからだ。

[0371 １３２人目の素数さん 2023/08/23(水) 14:17:49.82 ID:SzHPMf8P]

＞03 の場合分けに入った時点で、求める答えは、(AllLimited z) ではなく (AllLimited (m * 36 + 13)) に変化します。
＞「p2」には★３が入ります。その p2 でさらに場合分けをおこないます。
＞「p3」には★４が来て、計算をおこなうのですが、★３の「2*m」が★４の「l」に代入されて
＞　(AllLimited (m * 36 + 13))
＞が出力されます。これが求めている答えになります。have 以降は気にしないでください。

これもまた意味不明。あなたの説明を額面通りに受け取ると、

・ AllLimited 3 を呼び出すのが目標なのだが、場合分けをしてみると、
　 実際には AllLimited (別の値) を呼び出すことに帰着される

ということになる。つまり、問題を先送りというか、
別の AllLimited z に責任転嫁しているだけである。
それならそれで別に構わないのだが、だったら結局のところ、
責任転嫁した先にある AllLimited (別の値) を「呼び出していい」
という根拠は一体どこにあるの？どうも君は、

「有限長の割数列に対して拡張スター変換を施したら、
　その先にある割数列は全て有限長。ゆえに、AllLimited (別の値) は
　この時点で既に呼び出していい」

と勘違いしているように見えるのだが。

[0372 １３２人目の素数さん 2023/08/23(水) 14:20:15.48 ID:SzHPMf8P]

何度も言うが、今は BaseCase から出発しているのである。
純粋な割数列が有限長だと判明しているのは x＝3 だけであり、

DivList(3)＝[1,4]

という表現のみが得られている。ここから出発して、
例の14パターンの場合分けを通過しても、

DivList(y) ＝ (別の有限長の割数列)

という表現がいくつか得られるだけである。
これらの表現は確かに有限長である。しかし、割数列の一意性が崩れている。
従って、y に対する純粋な割数列までもが有限長であるとは結論できない。

つまり、DivList(3)＝[1,4] から出発して例の14パターンを通過しても、
FirstLimited 45 とか FirstLimited 39 とかは原理的に証明できっこない。

やはり、あなたのロジックは破綻しているのでは？

[0373 １３２人目の素数さん 2023/08/23(水) 14:34:58.80 ID:jvofjEJg]

>>368
特に前提X はありませんが、(AllLimited 3)等と直接書くことはできないです。プログラムの制約で。
その上で、証明手順といえば以前に書いたものと変わらず
-----
> 6t+3 を 14パターン に分けます。
> FirstLimited (パターンx) を証明したいとします。
> 帰納法の仮定より、x>q である FirstLimited q は言えます。
> 次に＜関数 firstToAll＞ を使って FirstLimited q を AllLimited q に変えます。
> AllLimited q の中に、FirstLimited x(の素) は含まれるので（そうなるように AllLimited q を作ってあります）、
> それを取り出して証明完了です。
-----
としか言えないです。ちなみに、定理証明プログラムのチェックはパスしています。

[0374 １３２人目の素数さん 2023/08/23(水) 14:35:32.02 ID:jvofjEJg]

>>369-372
すみません、＜関数 firstToAll＞の中身については、噛み合ってなくて議論ができないです。
自分にプログラムを説明する能力がなくてすみません。

[0375 １３２人目の素数さん 2023/08/23(水) 14:36:47.13 ID:SzHPMf8P]

>>374
質問の仕方を変えます。いま目標にしているのは、

・ FirstLimited 3 から出発して AllLimited 3 に到達すること

である。そして、あなたの解説によれば、

・ AllLimited 3 のかわりに、別の AllLimited z に到達することに帰着される

ということになる。では、具体的にどのような AllLimited z に帰着されるのか、
そのような z を全て列挙して下さい。

[0376 １３２人目の素数さん 2023/08/23(水) 14:46:12.51 ID:SzHPMf8P]

ちなみに、>>356のソースコードを見ても

firstToAll

という関数名が見当たらないんだが、どこにあります？

[0377 １３２人目の素数さん 2023/08/23(水) 14:49:07.30 ID:jvofjEJg]

>>376
divseq2 のコードでは、Main.lean の 「singleToExts」という名前になっています。

[0378 １３２人目の素数さん 2023/08/23(水) 14:53:09.47 ID:SzHPMf8P]

一応、これにも返答しておく。

>>373
＞ちなみに、定理証明プログラムのチェックはパスしています。

拡張スター変換に対する理論的な性質を前提とした上での話でしょ？
つまり、一番肝心なところはプログラム内でも「公理」としてスルーしてるんでしょ？
そこの理論が間違ってたら、プログラムのチェックが通ってても意味がない。

本当に定理証明プログラムを名乗るなら、
コラッツ予想そのものを意味するプログラムを
厳密に書かなければ意味がない。

[0379 １３２人目の素数さん 2023/08/23(水) 15:00:01.62 ID:jvofjEJg]

>>375
> ・ AllLimited 3 のかわりに、別の AllLimited z に到達することに帰着される
その解釈がもう噛み合ってないのですみません。
力不足で申し訳ありません。

[0380 １３２人目の素数さん 2023/08/23(水) 15:03:32.35 ID:SzHPMf8P]

>>379
解釈が合ってないも何も、あなた自身が

＞02 の場合分けに入った時点で、求める答えは、(AllLimited z) ではなく
＞(AllLimited succ (succ (succ (succ ((succ (l * 2 * 2)) * 3))))) に変化します。

と説明したのだが？

[0381 １３２人目の素数さん 2023/08/23(水) 15:03:46.54 ID:jvofjEJg]

>>378
ごもっともです......

[0382 １３２人目の素数さん 2023/08/23(水) 15:09:22.44 ID:SzHPMf8P]

>>381
ごもっともですって・・・なんだそりゃ。
なぜコラッツ予想そのものを意味するプログラムを厳密に書かないんだ？

[0383 １３２人目の素数さん 2023/08/23(水) 15:10:42.01 ID:jvofjEJg]

>>382
自分は割数列を使ったコラッツ予想の証明しか思いつかないからです。

[0384 １３２人目の素数さん 2023/08/23(水) 15:13:39.81 ID:SzHPMf8P]

>>383
だから、そこまで含めて全ての言明をプログラムで書かない理由は？

「どうやってプログラムに翻訳したらいいか分からない箇所があるので、
　そこは公理にしてお茶を濁している」ということ？

[0385 １３２人目の素数さん 2023/08/23(水) 15:17:59.06 ID:jvofjEJg]

>>384
いや、95%は定理証明に成功していて、残りは公理としています。

[0386 １３２人目の素数さん 2023/08/23(水) 15:19:30.22 ID:jvofjEJg]

>>385
答えになってないですね。
残り 5% の公理も、人間が見ればほぼ自明と分かるようなものです。

[0387 １３２人目の素数さん 2023/08/23(水) 15:22:42.26 ID:SzHPMf8P]

>>386
人間が見て自明と分かるから、

「わざわざプログラムに翻訳せずに、言わば "手抜き" をして公理で済ませている」

ということ？やろうと思えば、その部分もプログラムに翻訳できるってこと？

[0388 １３２人目の素数さん 2023/08/23(水) 15:24:49.65 ID:jvofjEJg]

>>387
いや、技術的な理由で、絶対に定理証明できない部分です。

[0389 １３２人目の素数さん 2023/08/23(水) 15:26:07.36 ID:SzHPMf8P]

>>388
具体的にどのような公理を設定しているのか、ここに書けますか？

[0390 １３２人目の素数さん 2023/08/23(水) 15:38:19.79 ID:jvofjEJg]

>>389
・旧型のほうは、公理はありません。しかし証明の一部を devseq2 に依存しています。
・devseq2
　Divseq2.lean
　　FirstLimited 3, 9（これを公理にしないといけない技術的理由がある）
　Main.lean
　　axiom h₀₅ (m : Nat) : (9 * (8 * m + 7) + 11) / 2 = succ (succ (succ (succ ((succ ((succ ((succ (succ (m * 3))) * 2)) * 2)) * 3))))
　　axiom h₀₆ (l : Nat) : (16 * l + 3) + (16 * l + 3 - 3) / 8 + 1 = succ (succ (succ (succ (l * 3 * 2 * 3))))
　　axiom h₀₇ (l : Nat) : 8 * l + 4 + (8 * l + 4 - 4) / 4 * 5 + 6 = succ (succ (succ (succ (((succ (l * 3)) * 2) * 3))))
　　axiom h₀₈ (l : Nat) : 4 * (4 * l + 3) + (4 * l + 3 - 3) / 2 + 4 = succ (succ (succ (succ (((succ (succ (l * 3))) * 2) * 3))))
　　axiom h₁₃ (l : Nat) : (9 * (4 * l + 1) + 15) / 2 = succ (succ (succ ((succ ((succ (l * 3)) * 2)) * 3)))
　　axiom h₁₄ (l : Nat) : (9 * (8 * l + 7) + 9) / 4 = succ (succ (succ ((succ ((succ (succ (l * 3))) * 2)) * 3)))
　　　どれも簡単な計算で、真と分かる。succ は +1 する関数

[0391 １３２人目の素数さん 2023/08/23(水) 15:43:22.64 ID:SzHPMf8P]

>>390
左辺の四則演算を suc と * の組み合わせで言い換えただけだよね。
で、技術的な理由により、その言い換えは「公理」として設定しなければならないと。

だったら、その公理のもとで、
コラッツ予想そのものをプログラムで翻訳することは可能なのでは？つまり、

「任意の正整数nに対して、nに有限回のコラッツ操作を施すと1になる」

を直接的に意味するようなプログラムを書くことは普通に可能なのでは？

[0392 １３２人目の素数さん 2023/08/23(水) 15:46:58.98 ID:jvofjEJg]

>>391
いや〜難しいですねー
残りの定理証明の部分もどっぷり割数列につかっていますし。

[0393 １３２人目の素数さん 2023/08/23(水) 15:47:52.73 ID:SzHPMf8P]

>>392
「やろうと思えば原理的にはできる」なのか、
それとも「原理的に不可能」なのか、どっちですか？

[0394 １３２人目の素数さん 2023/08/23(水) 15:51:19.66 ID:jvofjEJg]

>>393
原理的に不可能だと思います。
やるなら一からコラッツ予想そのものを定理証明したほうが良いです。

[0395 １３２人目の素数さん 2023/08/23(水) 15:56:16.47 ID:SzHPMf8P]

>>394
原理的に不可能なら、余計に説得力がないことになっちゃうが。
せっかく定理証明支援系使ってるのに、
肝心なところは翻訳不可能って、なんだそりゃ。

[0396 １３２人目の素数さん 2023/08/23(水) 15:57:28.51 ID:SzHPMf8P]

とりあえず、divseq2 の singleToExts (つまりfirstToAll)について質問したい。

・ まずは singleToExts 3 を実行する。

・ すると、内部で p = SingleLimited 3 と置かれて、
　 p に対するパターンマッチングが順次行われる。

・ マッチング先として用意されているパターンは
　 SingleLimited.is02 〜 SingleLimited.is14 の13通りである
　 (それぞれの内部でさらに小さな場合分けは存在するが)。

そこで質問。p = SingleLimited 3 とのマッチングに成功する

・ SingleLimited.is**

は、is02〜is14 のうちどれですか？

[0397 １３２人目の素数さん 2023/08/23(水) 16:32:17.21 ID:SzHPMf8P]

よく見たら、まず SingleLimited の時点で
定義がゴリゴリしてるな。SingleLimited の定義は

inductive SingleLimited : Nat → Prop where
| is02 : (l : Nat) → (ExtsLimited <| l) → (SingleLimited <| succ (succ (succ (succ ((succ (l * 2 * 2)) * 3)))))

と続いていきますが、このように定義された SingleLimited について、

・ SingleLimited 3

と書いたとき、これは内部的には何を表現しているのですか？
Nat → Prop と書いてあるので、「SingleLimited 3」それ自体は
何らかの Prop を表現しているのですか？
だとすると、それは具体的にはどのような Prop ですか？

[0398 １３２人目の素数さん 2023/08/23(水) 16:35:06.38 ID:jvofjEJg]

>>396
・プログラムのコラッツ値は 6t+3 の t を渡す仕様になっています。
3 のときは 0 を渡すことになります。

divseq2 の Divseq2.lean です。SingleLimited→FirstLimited、ExtsLimited→AllLimited です。
-----
inductive SingleLimited : Nat → Prop where
| is02 : (l : Nat) → (ExtsLimited <| l) → (SingleLimited <| succ (succ (succ (succ ((succ (l * 2 * 2)) * 3)))))
| is03 : (m : Nat) → (ExtsLimited <| 2*m) → (SingleLimited <| succ (succ (succ (succ ((succ ((succ (m * 3 * 2)) * 2)) * 3)))))
| is04 : (m : Nat) → (ExtsLimited <| 4*m+1) → (SingleLimited <| succ (succ (succ (succ (succ (succ (succ (m * 3) * 2) * 2) * 3)))))
| is05 : (m : Nat) → (ExtsLimited <| 8*m+7) → (SingleLimited <| succ (succ (succ (succ (succ (succ (succ (succ (m * 3)) * 2) * 2) * 3)))))
| is06 : (l : Nat) → (ExtsLimited <| 16*l+3) → (SingleLimited <| succ (succ (succ (succ (l * 3 * 2 * 3)))))
| is07 : (l : Nat) → (ExtsLimited <| 8*l+4) → (SingleLimited <| succ (succ (succ (succ (((succ (l * 3)) * 2) * 3)))))
| is08 : (l : Nat) → (ExtsLimited <| 4*l+3) → (SingleLimited <| succ (succ (succ (succ (((succ (succ (l * 3))) * 2) * 3)))))
| is09 : (j : Nat) → (ExtsLimited <| j) → (SingleLimited <| succ (succ (j*3)))
| is11 : (k : Nat) → (ExtsLimited <| k) → (SingleLimited <| succ (succ (succ (k * 2 * 3))))
| is12 : (l : Nat) → (ExtsLimited <| 2*l) → (SingleLimited <| succ (succ (succ ((succ (l * 3 * 2)) * 3))))
......
-----
SingleLimited の定義のこの中に SingleLimited 3(0) は無いので、
is02～is14 どれにもマッチしません。

しかし
singleToExts に SingleLimited 3(0) を渡したら ExtsLimited 3(0) が返ります（プログラムで確認済）

[0399 １３２人目の素数さん 2023/08/23(水) 16:38:25.62 ID:jvofjEJg]

>>397
「3グループの先頭要素の割数列が有限長」という意味ですが、これ自体はコード化していません。

[0400 １３２人目の素数さん 2023/08/23(水) 16:57:16.91 ID:SzHPMf8P]

>>398
＞・プログラムのコラッツ値は 6t+3 の t を渡す仕様になっています。
＞ 3 のときは 0 を渡すことになります。

つまり、FirstLimited 3 に対応する
プログラム内の記述は SingleLimited 0 ということですか？
また、「 FirstLimited 3 に firstToAll を適用する」ことは

・ singleToExts 0 を実行する

ことと同じですか？

[0401 １３２人目の素数さん 2023/08/23(水) 16:59:47.48 ID:jvofjEJg]

>>400
はい、そうです。
・ singleToExts 0 (SingleLimited 0) を実行する
です。

[0402 １３２人目の素数さん 2023/08/23(水) 17:01:29.32 ID:jvofjEJg]

ちょっと違いました。
・singleToExts (zero) is10　を実行する
でした。is10 は定義されています。

[0403 １３２人目の素数さん 2023/08/23(水) 17:05:26.22 ID:SzHPMf8P]

>>401
ちょっと話が横道に逸れるけど、質問したい。

＞ singleToExts 0 (SingleLimited 0) を実行する

singleToExts は2変数関数ということですか？
今回の場合だと、「0」「SingleLimited 0」という
2つの値を渡して実行するということですか？

singleToExts の目的を考えると、そこに渡す変数は常に

「 x 」「 SingleLimited x 」

でしかないように見えるので、第一変数 x を指定した時点で、
第二変数は必要なくて、singleToExts の内部で
勝手に SingleLimited x を1つ生成すれば、
singleToExts それ自体は1変数関数で済むのでは？

そういう実装は不可能だった？