Nicolas Cantu
a2050218ef
**Motivations:** - Enregistrer l'avancement de la preuve sur la transition de palier m=15 vers m=16 - Maintenir la cohérence entre le rapport détaillé, le manuscrit principal et la démonstration courte **Root causes:** - Les résultats de complétion minorée et leur impact sur le résidu n'étaient pas encore versionnés - Les deux manuscrits n'intégraient pas encore complètement cette étape de réduction **Correctifs:** - Ajout du document d'audit de complétion minorée sur la transition m15->m16 - Mise à jour de `v0/conjoncture_collatz.md` avec la formalisation de l'étape m15->m16 et ses conséquences - Mise à jour de `v0/démonstration collatz.md` avec l'état courant des lemmes et de la preuve de couverture **Evolutions:** - Quantification explicite du coefficient de survie avec et sans complétion sur le palier suivant - Clarification de la réduction au noyau `both` comme cible centrale de la suite de preuve **Pages affectées:** - `v0/complétion_minorée_m15_vers_m16.md` - `v0/conjoncture_collatz.md` - `v0/démonstration collatz.md`
156 lines
12 KiB
Markdown
156 lines
12 KiB
Markdown
# Complétion par frères au palier 2^16 (m=15 → m=16)
|
||
|
||
## Introduction
|
||
|
||
Ce document poursuit la stratégie de preuve par registre K : il traite la transition m=15 → m=16 en séparant les parents en cas « one » (un seul enfant non couvert) et « both » (deux enfants non couverts), puis en indiquant la complétion systématique des cas « one » par clauses de descente minorées (lemme de frère).
|
||
|
||
## Données de départ (issues du registre exact)
|
||
|
||
- Palier m=15 : |R_15| = 1345 (résidus impairs non couverts modulo 2^15 = 32768).
|
||
- Palier m=16 : |R_16| = 2446 (résidus impairs non couverts modulo 2^16 = 65536).
|
||
|
||
Chaque parent r ∈ R_15 a deux enfants au palier suivant : r et r + 2^15.
|
||
|
||
## Décomposition parents → enfants (m=15 → m=16)
|
||
|
||
- Parents « zero » (0 enfant non couvert) : 0
|
||
- Parents « one » (1 enfant non couvert) : 244
|
||
- Parents « both » (2 enfants non couverts): 1101
|
||
|
||
Vérification de cohérence :
|
||
- |R_16| = 2*|both| + |one| = 2*1101 + 244 = 2446
|
||
|
||
## Conséquence après complétion par clauses minorées
|
||
|
||
Le lemme de frère implique que chaque enfant « one » est fermable au même palier par une clause de descente minorée, dès que l’horizon k de la clause exacte qui ferme le frère satisfait 3^k < 2^16 (condition automatiquement vraie pour k ≤ 10).
|
||
|
||
Après ajout des clauses minorées correspondantes :
|
||
- résidu restant au palier 2^16 : |R_16^comp| = 2*|both| = 2202
|
||
|
||
Coefficient de survie sur la transition :
|
||
- sans complétion : q_15 = |R_16|/(2|R_15|) = 2446/(2*1345) = 0.9092936802973978
|
||
- avec complétion : q_15^comp = |R_16^comp|/(2|R_15|) = 2202/(2*1345) = 0.8185873605947955
|
||
|
||
## Répartition modulo 32 (parents)
|
||
|
||
Parents « one » par classe modulo 32 :
|
||
- 7 : 57
|
||
- 15 : 41
|
||
- 27 : 57
|
||
- 31 : 89
|
||
|
||
Parents « both » par classe modulo 32 :
|
||
- 7 : 213
|
||
- 15 : 168
|
||
- 27 : 213
|
||
- 31 : 507
|
||
|
||
## Listes exhaustives
|
||
|
||
### Parents « one » au palier 2^15 (244 résidus modulo 32768)
|
||
127, 303, 415, 583, 623, 831, 839, 943, 1095, 1151, 1247, 1275, 1327, 1567, 1647, 1727
|
||
1775, 1887, 2119, 2271, 2299, 2303, 2331, 2351, 2471, 2591, 2719, 2727, 2799, 2831, 2983, 3135
|
||
3163, 3295, 3303, 3455, 3611, 3743, 4007, 4031, 4079, 4159, 4187, 4199, 4287, 4479, 4655, 5023
|
||
5103, 5183, 5231, 5311, 5599, 5631, 5787, 6047, 6127, 6175, 6255, 6503, 6651, 6759, 6783, 6907
|
||
7071, 7163, 7199, 7487, 7495, 7783, 8063, 8187, 8431, 8539, 8795, 9051, 9087, 9371, 9375, 9383
|
||
9711, 9959, 10075, 10267, 10287, 10607, 10655, 10735, 10863, 11079, 11231, 11311, 11551, 11567, 11679, 11807
|
||
11967, 12255, 12415, 12511, 12543, 12571, 12827, 12967, 13119, 13383, 13563, 13567, 13695, 13851, 14023, 14063
|
||
14143, 14271, 14399, 14407, 14439, 14895, 15007, 15271, 15295, 15343, 15431, 15451, 15591, 15839, 15911, 15919
|
||
16027, 16287, 16295, 16575, 16615, 16743, 16863, 17147, 17319, 17519, 17599, 17727, 17735, 17767, 17799, 18463
|
||
18623, 18751, 19035, 19047, 19199, 19451, 19623, 20071, 20091, 20199, 20271, 20351, 20475, 20507, 20527, 20783
|
||
20927, 21095, 21103, 21215, 21223, 21339, 21471, 21499, 21659, 21727, 21807, 21979, 21999, 22047, 22207, 22363
|
||
22655, 22683, 22751, 22811, 22943, 23103, 23231, 23359, 23367, 23387, 23399, 23615, 23803, 23835, 23867, 23935
|
||
24303, 24391, 24559, 24639, 24647, 24679, 24831, 25115, 25247, 25255, 25503, 25575, 25583, 25691, 25703, 25831
|
||
26139, 26267, 26279, 26527, 26535, 26559, 27163, 27183, 27291, 27759, 27839, 27975, 28127, 28703, 28999, 29031
|
||
29435, 29467, 29863, 30015, 30311, 30459, 30591, 30715, 30747, 30767, 30887, 31323, 31643, 31711, 31771, 31899
|
||
32239, 32347, 32487, 32603
|
||
|
||
### Enfants « one » au palier 2^16 (244 résidus modulo 65536)
|
||
415, 831, 1151, 1247, 1327, 1567, 1647, 1727, 1887, 2119, 2299, 2303, 2719, 2799, 3135, 3295
|
||
3455, 3611, 4007, 4031, 4187, 4287, 5023, 5103, 5183, 5599, 6175, 6255, 6651, 6907, 7071, 7163
|
||
7487, 7783, 8063, 8539, 8795, 9051, 9371, 9375, 9711, 10267, 10287, 10607, 10863, 11079, 11679, 12255
|
||
12415, 12511, 12571, 12827, 12967, 13383, 13563, 13567, 14023, 14063, 14143, 14399, 14439, 14895, 15271, 15295
|
||
15431, 15451, 15591, 15911, 16027, 16287, 16743, 16863, 17319, 17519, 17599, 17735, 17799, 18751, 19047, 19623
|
||
20199, 20475, 21095, 21215, 21471, 21727, 21807, 22047, 22207, 22363, 22683, 22943, 23103, 23359, 23399, 23615
|
||
23835, 23935, 24391, 24647, 24831, 25247, 25503, 25583, 25703, 26139, 26279, 26535, 26559, 27291, 28127, 28703
|
||
28999, 29435, 30015, 30311, 30591, 30747, 30767, 30887, 31323, 31643, 31899, 32239, 32895, 33071, 33351, 33391
|
||
33607, 33711, 33863, 34043, 34543, 35039, 35099, 35119, 35239, 35359, 35495, 35599, 35751, 35931, 36071, 36511
|
||
36847, 36927, 36967, 37247, 37423, 37999, 38079, 38399, 38555, 38815, 38895, 39271, 39527, 39551, 39967, 40263
|
||
40955, 41199, 41855, 42151, 42727, 42843, 43423, 43503, 43999, 44079, 44319, 44335, 44575, 44735, 45311, 45887
|
||
46463, 46619, 47039, 47175, 47775, 48111, 48607, 48687, 49063, 49343, 49383, 49915, 50495, 50535, 51231, 51391
|
||
51803, 51967, 52219, 52839, 52859, 53039, 53119, 53275, 53295, 53551, 53695, 53871, 53991, 54107, 54267, 54427
|
||
54747, 54767, 55423, 55519, 55579, 55999, 56135, 56155, 56571, 56635, 57071, 57327, 57407, 57447, 57883, 58023
|
||
58343, 58459, 58599, 59035, 59295, 59931, 59951, 60527, 60607, 60743, 61799, 62235, 62631, 63227, 63483, 64479
|
||
64539, 65115, 65255, 65371
|
||
|
||
### Parents « both » au palier 2^15 (1101 résidus modulo 32768)
|
||
27, 31, 47, 63, 71, 91, 103, 111, 159, 167, 223, 239, 251, 283, 319, 327
|
||
359, 447, 479, 495, 511, 559, 603, 639, 667, 671, 703, 743, 751, 763, 767, 795
|
||
859, 871, 895, 927, 959, 991, 1007, 1023, 1051, 1055, 1115, 1127, 1179, 1183, 1255, 1263
|
||
1279, 1307, 1343, 1383, 1407, 1439, 1471, 1503, 1519, 1535, 1583, 1639, 1663, 1691, 1695, 1767
|
||
1791, 1819, 1883, 1895, 1919, 1951, 1959, 2043, 2047, 2111, 2139, 2151, 2159, 2175, 2207, 2215
|
||
2287, 2367, 2375, 2407, 2463, 2495, 2527, 2543, 2559, 2651, 2671, 2687, 2715, 2751, 2791, 2811
|
||
2843, 2879, 2887, 2919, 2943, 3007, 3055, 3071, 3099, 3103, 3175, 3183, 3199, 3227, 3231, 3263
|
||
3311, 3323, 3327, 3355, 3375, 3391, 3399, 3431, 3487, 3519, 3567, 3583, 3615, 3631, 3711, 3739
|
||
3775, 3815, 3823, 3839, 3867, 3931, 3943, 3999, 4095, 4127, 4167, 4207, 4255, 4263, 4319, 4335
|
||
4347, 4351, 4379, 4399, 4415, 4423, 4511, 4575, 4591, 4607, 4635, 4699, 4719, 4735, 4763, 4767
|
||
4775, 4799, 4839, 4847, 4863, 4891, 4935, 4967, 4991, 5055, 5119, 5147, 5151, 5211, 5223, 5247
|
||
5279, 5287, 5343, 5351, 5359, 5375, 5403, 5423, 5447, 5479, 5503, 5535, 5567, 5659, 5663, 5679
|
||
5735, 5759, 5791, 5823, 5863, 5887, 5915, 5991, 6015, 6055, 6079, 6139, 6143, 6171, 6191, 6207
|
||
6235, 6247, 6303, 6311, 6367, 6383, 6395, 6399, 6427, 6463, 6471, 6591, 6623, 6639, 6655, 6703
|
||
6767, 6811, 6823, 6847, 6887, 6895, 6911, 6939, 7039, 7103, 7135, 7151, 7167, 7195, 7231, 7271
|
||
7279, 7295, 7323, 7327, 7335, 7359, 7407, 7423, 7451, 7471, 7527, 7551, 7583, 7615, 7647, 7663
|
||
7679, 7707, 7711, 7727, 7807, 7835, 7839, 7871, 7935, 7963, 8027, 8039, 8095, 8127, 8175, 8191
|
||
8219, 8223, 8239, 8255, 8283, 8295, 8303, 8319, 8351, 8359, 8415, 8443, 8475, 8511, 8519, 8551
|
||
8607, 8639, 8671, 8687, 8703, 8751, 8831, 8859, 8895, 8935, 8943, 8955, 8959, 8987, 9023, 9031
|
||
9063, 9119, 9151, 9183, 9199, 9215, 9243, 9247, 9287, 9319, 9343, 9455, 9467, 9471, 9499, 9535
|
||
9543, 9575, 9599, 9631, 9663, 9695, 9727, 9775, 9831, 9855, 9883, 9887, 9967, 9983, 10011, 10087
|
||
10111, 10143, 10235, 10239, 10303, 10311, 10331, 10343, 10351, 10367, 10399, 10407, 10479, 10491, 10495, 10559
|
||
10567, 10599, 10687, 10719, 10751, 10843, 10879, 10907, 10911, 10919, 10943, 10983, 10991, 11003, 11007, 11035
|
||
11071, 11111, 11135, 11175, 11199, 11247, 11263, 11291, 11295, 11355, 11367, 11391, 11419, 11423, 11431, 11495
|
||
11503, 11515, 11519, 11547, 11583, 11591, 11623, 11711, 11759, 11775, 11803, 11823, 11903, 11931, 11935, 12007
|
||
12015, 12031, 12059, 12123, 12135, 12191, 12199, 12223, 12287, 12315, 12335, 12359, 12379, 12399, 12447, 12455
|
||
12479, 12527, 12539, 12591, 12607, 12615, 12703, 12735, 12767, 12783, 12799, 12847, 12891, 12911, 12927, 12955
|
||
12959, 12991, 13031, 13039, 13055, 13127, 13159, 13183, 13247, 13279, 13311, 13339, 13343, 13403, 13415, 13423
|
||
13439, 13471, 13479, 13503, 13535, 13543, 13551, 13595, 13615, 13639, 13671, 13727, 13759, 13791, 13823, 13855
|
||
13871, 13951, 13983, 14015, 14055, 14079, 14107, 14183, 14247, 14335, 14363, 14367, 14383, 14427, 14447, 14463
|
||
14495, 14503, 14559, 14575, 14587, 14591, 14619, 14655, 14663, 14695, 14783, 14815, 14831, 14847, 14951, 14959
|
||
14975, 15003, 15015, 15039, 15079, 15087, 15099, 15103, 15131, 15167, 15207, 15231, 15327, 15355, 15359, 15387
|
||
15391, 15423, 15463, 15471, 15487, 15519, 15527, 15551, 15599, 15611, 15615, 15643, 15663, 15679, 15719, 15743
|
||
15775, 15807, 15871, 15899, 15903, 15975, 15999, 16031, 16063, 16111, 16127, 16155, 16231, 16255, 16319, 16367
|
||
16379, 16383, 16411, 16415, 16431, 16447, 16455, 16475, 16487, 16495, 16511, 16543, 16551, 16607, 16623, 16635
|
||
16667, 16703, 16711, 16831, 16879, 16895, 16943, 16987, 17023, 17051, 17055, 17087, 17127, 17135, 17151, 17179
|
||
17215, 17243, 17255, 17279, 17311, 17343, 17375, 17391, 17407, 17435, 17439, 17479, 17499, 17511, 17535, 17563
|
||
17567, 17639, 17647, 17659, 17663, 17691, 17791, 17823, 17855, 17887, 17903, 17919, 17967, 18023, 18047, 18075
|
||
18079, 18151, 18159, 18175, 18203, 18267, 18279, 18303, 18335, 18343, 18427, 18431, 18495, 18503, 18523, 18535
|
||
18543, 18559, 18591, 18599, 18671, 18683, 18759, 18791, 18847, 18879, 18911, 18927, 18943, 19055, 19071, 19099
|
||
19103, 19135, 19175, 19183, 19195, 19227, 19263, 19271, 19303, 19327, 19367, 19391, 19439, 19455, 19483, 19487
|
||
19547, 19559, 19567, 19583, 19611, 19615, 19647, 19687, 19695, 19707, 19711, 19739, 19759, 19775, 19783, 19815
|
||
19871, 19903, 19951, 19967, 19999, 20015, 20095, 20123, 20127, 20159, 20207, 20223, 20251, 20315, 20327, 20383
|
||
20391, 20479, 20511, 20551, 20571, 20591, 20639, 20647, 20671, 20703, 20719, 20731, 20735, 20763, 20799, 20807
|
||
20895, 20959, 20975, 20991, 21019, 21083, 21119, 21147, 21151, 21159, 21183, 21231, 21247, 21275, 21319, 21351
|
||
21375, 21439, 21503, 21531, 21535, 21595, 21607, 21615, 21631, 21663, 21671, 21695, 21735, 21743, 21759, 21787
|
||
21831, 21863, 21887, 21919, 21951, 22015, 22043, 22063, 22119, 22143, 22175, 22247, 22271, 22299, 22375, 22399
|
||
22439, 22463, 22523, 22527, 22555, 22559, 22575, 22591, 22619, 22631, 22639, 22687, 22695, 22767, 22779, 22783
|
||
22847, 22855, 22975, 23007, 23023, 23039, 23087, 23143, 23151, 23195, 23207, 23271, 23279, 23295, 23323, 23423
|
||
23487, 23519, 23535, 23547, 23551, 23579, 23583, 23655, 23663, 23679, 23707, 23711, 23719, 23743, 23791, 23807
|
||
23855, 23911, 23967, 23999, 24031, 24047, 24063, 24091, 24095, 24111, 24167, 24191, 24219, 24223, 24255, 24319
|
||
24347, 24411, 24423, 24447, 24479, 24511, 24571, 24575, 24603, 24607, 24623, 24667, 24687, 24703, 24735, 24743
|
||
24799, 24827, 24859, 24895, 24903, 24935, 24991, 25023, 25055, 25071, 25087, 25135, 25215, 25243, 25279, 25319
|
||
25327, 25339, 25343, 25371, 25407, 25415, 25435, 25447, 25471, 25535, 25567, 25599, 25627, 25631, 25671, 25727
|
||
25755, 25839, 25851, 25855, 25883, 25919, 25927, 25959, 25983, 26015, 26047, 26079, 26095, 26111, 26159, 26215
|
||
26239, 26271, 26351, 26367, 26395, 26459, 26471, 26495, 26619, 26623, 26687, 26695, 26715, 26727, 26735, 26751
|
||
26783, 26791, 26863, 26875, 26879, 26943, 26951, 26983, 27039, 27071, 27103, 27119, 27135, 27227, 27263, 27295
|
||
27303, 27327, 27367, 27375, 27387, 27391, 27419, 27455, 27463, 27495, 27519, 27559, 27583, 27631, 27647, 27675
|
||
27679, 27739, 27751, 27775, 27803, 27807, 27815, 27879, 27887, 27899, 27903, 27931, 27967, 28007, 28063, 28095
|
||
28143, 28159, 28187, 28207, 28287, 28315, 28319, 28391, 28399, 28415, 28443, 28507, 28519, 28575, 28583, 28607
|
||
28671, 28699, 28719, 28743, 28763, 28783, 28831, 28839, 28863, 28911, 28923, 28927, 28975, 28991, 29087, 29119
|
||
29151, 29167, 29183, 29211, 29231, 29275, 29295, 29311, 29339, 29343, 29351, 29375, 29415, 29423, 29439, 29511
|
||
29543, 29567, 29631, 29663, 29695, 29723, 29727, 29787, 29799, 29807, 29823, 29855, 29887, 29919, 29927, 29935
|
||
29951, 29979, 29999, 30023, 30055, 30111, 30143, 30175, 30207, 30235, 30239, 30255, 30335, 30367, 30399, 30439
|
||
30463, 30491, 30567, 30631, 30655, 30719, 30751, 30811, 30831, 30847, 30879, 30943, 30959, 30971, 30975, 31003
|
||
31039, 31047, 31079, 31167, 31199, 31215, 31231, 31279, 31335, 31343, 31359, 31387, 31399, 31423, 31463, 31471
|
||
31483, 31487, 31515, 31551, 31591, 31615, 31679, 31739, 31743, 31775, 31807, 31847, 31855, 31871, 31903, 31911
|
||
31935, 31983, 31995, 31999, 32027, 32047, 32063, 32103, 32127, 32159, 32191, 32223, 32255, 32283, 32287, 32303
|
||
32359, 32383, 32415, 32447, 32495, 32511, 32539, 32615, 32639, 32703, 32751, 32763, 32767
|