ncantu bd529682bf collatz: add palier2p15/p16 artefacts and Sm refinement tooling

**Motivations:**
- Publish new Collatz palier runs and associated artefacts (C3 local descent, universal clauses, iteration protocol).
- Extend the scripts toolbox to generate/verify clauses and build refinement certificates over S_m.

**Root causes:**
- Universal clause witnesses were lifted to 2^(A+1) even when the witness is already fixed modulo the domain palier, leading to unstable or unnecessarily weak/ambiguous modulus choices.
- CSV palier inference in scission could mis-detect short column names (e.g. "m") by substring matching.

**Correctifs:**
- Lift D_exact/F witnesses to m_stable := max(m, A+1) in universal clause extraction and run reports.
- Make scission palier/m column detection exact-match to avoid false positives.
- Update C3 local descent verification/reporting to use strict fusion witness selection prioritizing lower modular stability and refreshed D/F metrics.
- Add a dedicated run report profile for per-palier universal clauses.

**Evolutions:**
- Add scripts for terminal clauses and minorated descent clauses over S_m, their deterministic verification, and multi-level refinement certificate building.
- Add modular tooling for register_K and incremental comparison of D_minor families.
- Add/update feature documentation for the new pipelines and generated reports.

**Pages affectées:**
- applications/collatz/collatz_k_scripts/README.md
- applications/collatz/collatz_k_scripts/collatz_extract_universal_clauses.py
- applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
- applications/collatz/collatz_k_scripts/collatz_iterate_palier_protocol.py
- applications/collatz/collatz_k_scripts/collatz_scission.py
- applications/collatz/collatz_k_scripts/collatz_verify_c3_local_descent.py
- applications/collatz/collatz_k_scripts/collatz_verify_universal_clauses.py
- applications/collatz/collatz_k_scripts/*refinement*over_Sm*.py
- applications/collatz/collatz_k_scripts/collatz_generate_*clauses_over_Sm.py
- applications/collatz/collatz_k_scripts/collatz_verify_minorated_descent_clauses_over_Sm.py
- applications/collatz/collatz_k_scripts/collatz_build_register_K_modular.py
- applications/collatz/collatz_k_scripts/collatz_compare_dminor_families_incremental.py
- applications/collatz/*.md
- docs/features/*.md
- docs/artefacts/collatz/**
- docs/collatz_run_report_2026-03-09_*.md

2026-03-09 23:29:59 +01:00

36 KiB

Raw Permalink Blame History

Auteur : Équipe 4NK

Clauses universelles extraites — Option A (Lift(B12))

Entrée

C3 vérification JSON : docs/artefacts/collatz/c3_local_descent/verification_c3_local_descent_palier2p14.json

Domaine

palier (domaine des témoins) : 2^14
max(2^m_stable) observé : 2^102

Compteurs

total : 768
D_exact : 60
F : 648
D_brother_local : 60

Table (extrait)

kind	source_n	m_stable	residue_mod_2^m	k/t	A	N0/Nf	mate_exact
D_brother_local	191			8	14		8383
D_brother_local	303			8	15		8495
D_brother_local	623			8	15		8815
D_brother_local	1135			8	14		9327
D_brother_local	1215			8	14		9407
D_brother_local	1247			8	16		9439
D_brother_local	1327			8	16		9519
D_brother_local	1567			8	16		9759
D_brother_local	1727			8	16		9919
D_brother_local	2079			8	14		10271
D_brother_local	2271			8	15		10463
D_brother_local	2331			8	15		10523
D_brother_local	2663			8	14		10855
D_brother_local	3067			8	14		11259
D_brother_local	3135			8	17		11327
D_brother_local	3455			8	17		11647
D_brother_local	3687			8	14		11879
D_brother_local	3967			8	14		12159
D_brother_local	4079			8	15		12271
D_brother_local	4091			8	14		12283
D_brother_local	4159			8	15		12351
D_brother_local	4199			8	15		12391
D_brother_local	4955			8	14		13147
D_brother_local	5023			8	16		13215
D_brother_local	5103			8	16		13295
D_brother_local	5275			8	14		13467
D_brother_local	5615			8	14		13807
D_brother_local	5787			8	15		13979
D_brother_local	5979			8	14		14171
D_brother_local	6047			8	15		14239
D_brother_local	6559			8	14		14751
D_brother_local	6983			8	14		15175
D_brother_local	7495			8	15		15687
D_brother_local	8447			8	14		255
D_brother_local	8731			8	14		539
D_brother_local	8871			8	14		679
D_brother_local	9383			8	15		1191
D_brother_local	9755			8	14		1563
D_brother_local	10175			8	14		1983
D_brother_local	10267			8	18		2075
D_brother_local	10287			8	17		2095
D_brother_local	10799			8	14		2607
D_brother_local	11231			8	15		3039
D_brother_local	11743			8	14		3551
D_brother_local	12415			8	16		4223
D_brother_local	12647			8	14		4455
D_brother_local	13051			8	14		4859
D_brother_local	13119			8	15		4927
D_brother_local	13383			8	18		5191
D_brother_local	13563			8	17		5371
D_brother_local	13631			8	14		5439
D_brother_local	14063			8	23		5871
D_brother_local	14407			8	15		6215
D_brother_local	14939			8	14		6747
D_brother_local	15007			8	15		6815
D_brother_local	15271			8	16		7079
D_brother_local	15451			8	16		7259
D_brother_local	15591			8	16		7399
D_brother_local	16103			8	14		7911
D_brother_local	16295			8	15		8103
D_exact	255	14	255	8	13	N0=4
D_exact	539	14	539	8	13	N0=7
D_exact	679	14	679	8	13	N0=6
D_exact	1191	14	1191	8	13	N0=6
D_exact	1563	14	1563	8	13	N0=6
D_exact	1983	14	1983	8	13	N0=5
D_exact	2075	14	2075	8	13	N0=6
D_exact	2095	14	2095	8	13	N0=6
D_exact	2607	14	2607	8	13	N0=6
D_exact	3039	14	3039	8	13	N0=6
D_exact	3551	14	3551	8	13	N0=5
D_exact	4223	14	4223	8	13	N0=4
D_exact	4455	14	4455	8	13	N0=5
D_exact	4859	14	4859	8	13	N0=8
D_exact	4927	14	4927	8	13	N0=5
D_exact	5191	14	5191	8	13	N0=8
D_exact	5371	14	5371	8	13	N0=7
D_exact	5439	14	5439	8	13	N0=5
D_exact	5871	14	5871	8	13	N0=5
D_exact	6215	14	6215	8	13	N0=7
D_exact	6747	14	6747	8	13	N0=7
D_exact	6815	14	6815	8	13	N0=5
D_exact	7079	14	7079	8	13	N0=8
D_exact	7259	14	7259	8	13	N0=7
D_exact	7399	14	7399	8	13	N0=6
D_exact	7911	14	7911	8	13	N0=6
D_exact	8103	14	8103	8	13	N0=7
D_exact	8383	14	8383	8	13	N0=6
D_exact	8495	14	8495	8	13	N0=7
D_exact	8815	14	8815	8	13	N0=6
D_exact	9327	14	9327	8	13	N0=5
D_exact	9407	14	9407	8	13	N0=5
D_exact	9439	14	9439	8	13	N0=7
D_exact	9519	14	9519	8	13	N0=7
D_exact	9759	14	9759	8	13	N0=5
D_exact	9919	14	9919	8	13	N0=5
D_exact	10271	14	10271	8	13	N0=5
D_exact	10463	14	10463	8	13	N0=6
D_exact	10523	14	10523	8	13	N0=6
D_exact	10855	14	10855	8	13	N0=6
D_exact	11259	14	11259	8	13	N0=9
D_exact	11327	14	11327	8	13	N0=6
D_exact	11647	14	11647	8	13	N0=5
D_exact	11879	14	11879	8	13	N0=6
D_exact	12159	14	12159	8	13	N0=5
D_exact	12271	14	12271	8	13	N0=6
D_exact	12283	14	12283	8	13	N0=8
D_exact	12351	14	12351	8	13	N0=6
D_exact	12391	14	12391	8	13	N0=6
D_exact	13147	14	13147	8	13	N0=8
D_exact	13215	14	13215	8	13	N0=6
D_exact	13295	14	13295	8	13	N0=5
D_exact	13467	14	13467	8	13	N0=7
D_exact	13807	14	13807	8	13	N0=5
D_exact	13979	14	13979	8	13	N0=6
D_exact	14171	14	14171	8	13	N0=8
D_exact	14239	14	14239	8	13	N0=5
D_exact	14751	14	14751	8	13	N0=5
D_exact	15175	14	15175	8	13	N0=7
D_exact	15687	14	15687	8	13	N0=7
F	27	60	27	37	59	Nf=2
F	31	57	31	35	56	Nf=2
F	47	56	47	34	55	Nf=1
F	63	58	63	35	57	Nf=1
F	71	55	71	33	54	Nf=1
F	91	46	91	28	45	Nf=16
F	103	43	103	26	42	Nf=8
F	111	32	111	19	31	Nf=4
F	127	16	127	9	15	Nf=1
F	159	23	159	13	22	Nf=1
F	167	31	167	18	30	Nf=2
F	223	33	223	19	32	Nf=1
F	239	22	239	12	21	Nf=1
F	251	30	251	17	29	Nf=1
F	283	27	283	15	26	Nf=1
F	319	24	319	13	23	Nf=1
F	327	23	327	13	22	Nf=1
F	359	21	359	11	20	Nf=1
F	415	17	415	9	16	Nf=1
F	447	42	447	25	41	Nf=1
F	479	19	479	11	18	Nf=15
F	495	29	495	17	28	Nf=1
F	511	20	511	11	19	Nf=1
F	559	19	559	11	18	Nf=14
F	603	17	603	10	16	Nf=2
F	639	24	639	14	23	Nf=1
F	667	27	667	15	26	Nf=1
F	671	23	671	14	22	Nf=4
F	703	84	703	51	83	Nf=1
F	743	28	743	16	27	Nf=1
F	751	24	751	13	23	Nf=1
F	763	23	763	12	22	Nf=1
F	767	19	767	10	18	Nf=1
F	795	28	795	17	27	Nf=3
F	831	18	831	9	17	Nf=1
F	839	16	839	9	15	Nf=6
F	859	20	859	10	19	Nf=1
F	871	36	871	22	35	Nf=2
F	895	25	895	15	24	Nf=2
F	927	38	927	23	37	Nf=28
F	959	23	959	13	22	Nf=1
F	991	27	991	16	26	Nf=10
F	1007	22	1007	13	21	Nf=2
F	1023	21	1023	11	20	Nf=1
F	1051	20	1051	12	19	Nf=3
F	1055	83	1055	50	82	Nf=1
F	1095	16	1095	9	15	Nf=1
F	1115	24	1115	14	23	Nf=6
F	1127	23	1127	12	22	Nf=1
F	1151	18	1151	9	17	Nf=1
F	1179	20	1179	10	19	Nf=1
F	1183	17	1183	10	16	Nf=1
F	1255	21	1255	12	20	Nf=3
F	1263	27	1263	16	26	Nf=6
F	1275	16	1275	9	15	Nf=1
F	1279	25	1279	14	24	Nf=1
F	1307	35	1307	21	34	Nf=1
F	1343	24	1343	14	23	Nf=1
F	1351	15	1351	9	14	Nf=5
F	1383	43	1383	24	42	Nf=1
F	1407	85	1407	51	84	Nf=1
F	1439	22	1439	12	21	Nf=1
F	1471	32	1471	19	31	Nf=1
F	1503	25	1503	13	24	Nf=1
F	1519	18	1519	10	17	Nf=2
F	1535	20	1535	10	19	Nf=1
F	1583	82	1583	49	81	Nf=1
F	1639	37	1639	23	36	Nf=25
F	1663	18	1663	11	17	Nf=7
F	1691	22	1691	11	21	Nf=1
F	1695	34	1695	20	33	Nf=1
F	1767	20	1767	12	19	Nf=3
F	1775	16	1775	9	15	Nf=1
F	1791	19	1791	11	18	Nf=1
F	1819	62	1819	38	61	Nf=1
F	1883	20	1883	11	19	Nf=2
F	1895	26	1895	15	25	Nf=2
F	1919	24	1919	13	23	Nf=1
F	1951	18	1951	11	17	Nf=12
F	1959	28	1959	16	27	Nf=1
F	2043	20	2043	11	19	Nf=2
F	2047	59	2047	36	58	Nf=1
F	2111	84	2111	50	83	Nf=1
F	2119	17	2119	9	16	Nf=1
F	2139	21	2139	12	20	Nf=1
F	2151	42	2151	26	41	Nf=7
F	2159	21	2159	11	20	Nf=1
F	2175	21	2175	12	20	Nf=1
F	2207	31	2207	18	30	Nf=1
F	2215	45	2215	27	44	Nf=2
F	2287	54	2287	31	53	Nf=1
F	2299	17	2299	9	16	Nf=1
F	2303	19	2303	9	18	Nf=1
F	2367	18	2367	10	17	Nf=1
F	2375	29	2375	18	28	Nf=49
F	2407	18	2407	10	17	Nf=1
F	2463	23	2463	13	22	Nf=2
F	2495	17	2495	10	16	Nf=1
F	2527	28	2527	16	27	Nf=1
F	2543	30	2543	18	29	Nf=59
F	2559	41	2559	25	40	Nf=1
F	2651	19	2651	11	18	Nf=2
F	2671	20	2671	10	19	Nf=1
F	2687	18	2687	10	17	Nf=1
F	2715	34	2715	20	33	Nf=1
F	2719	17	2719	9	16	Nf=1
F	2727	16	2727	9	15	Nf=5
F	2751	44	2751	27	43	Nf=3
F	2791	19	2791	10	18	Nf=1
F	2799	17	2799	9	16	Nf=1
F	2811	19	2811	11	18	Nf=2
F	2815	15	2815	9	14	Nf=3
F	2843	25	2843	14	24	Nf=1
F	2879	18	2879	11	17	Nf=10
F	2887	17	2887	10	16	Nf=3
F	2919	18	2919	11	17	Nf=10
F	2943	30	2943	18	29	Nf=36
F	2983	16	2983	9	15	Nf=1
F	3007	23	3007	14	22	Nf=5
F	3055	31	3055	18	30	Nf=1
F	3071	50	3071	31	49	Nf=3
F	3099	20	3099	12	19	Nf=3
F	3103	20	3103	11	19	Nf=1
F	3163	16	3163	9	15	Nf=1
F	3175	43	3175	26	42	Nf=11
F	3183	22	3183	11	21	Nf=1
F	3199	18	3199	11	17	Nf=7
F	3227	41	3227	25	40	Nf=3
F	3231	24	3231	14	23	Nf=3
F	3239	15	3239	9	14	Nf=5
F	3263	20	3263	11	19	Nf=1
F	3303	16	3303	9	15	Nf=1
F	3311	27	3311	16	26	Nf=9
F	3323	44	3323	26	43	Nf=2
F	3327	19	3327	11	18	Nf=1
F	3355	25	3355	13	24	Nf=1
F	3375	20	3375	11	19	Nf=1
F	3391	30	3391	18	29	Nf=61
F	3399	49	3399	30	48	Nf=3
F	3431	37	3431	23	36	Nf=17
F	3487	17	3487	10	16	Nf=2
F	3519	25	3519	15	24	Nf=2
F	3567	31	3567	19	30	Nf=4
F	3583	20	3583	11	19	Nf=1
F	3611	17	3611	9	16	Nf=1
F	3615	21	3615	11	20	Nf=1
F	3631	29	3631	18	28	Nf=37
F	3711	38	3711	23	37	Nf=1
F	3739	41	3739	24	40	Nf=1
F	3743	16	3743	9	15	Nf=1
F	3775	22	3775	11	21	Nf=1
F	3815	18	3815	11	17	Nf=17
F	3823	26	3823	16	25	Nf=10
F	3839	37	3839	23	36	Nf=10
F	3867	25	3867	14	24	Nf=1
F	3931	27	3931	15	26	Nf=1
F	3943	46	3943	25	45	Nf=1
F	3999	20	3999	12	19	Nf=2
F	4007	19	4007	9	18	Nf=1
F	4031	17	4031	9	16	Nf=1
F	4095	52	4095	32	51	Nf=2
F	4123	15	4123	9	14	Nf=5
F	4127	43	4127	26	42	Nf=2
F	4143	15	4143	9	14	Nf=5
F	4167	21	4167	12	20	Nf=4
F	4187	18	4187	9	17	Nf=1
F	4207	38	4207	22	37	Nf=1
F	4255	71	4255	44	70	Nf=2
F	4263	58	4263	35	57	Nf=1
F	4287	20	4287	9	19	Nf=1
F	4319	17	4319	10	16	Nf=2
F	4335	18	4335	11	17	Nf=12
F	4347	48	4347	30	47	Nf=138
F	4351	22	4351	12	21	Nf=1
F	4379	17	4379	10	16	Nf=2
F	4399	34	4399	20	33	Nf=1
F	4415	29	4415	17	28	Nf=3
F	4423	24	4423	13	23	Nf=1
F	4511	21	4511	12	20	Nf=2
F	4543	15	4543	9	14	Nf=3
F	4575	39	4575	24	38	Nf=4
F	4591	66	4591	41	65	Nf=4
F	4607	49	4607	30	48	Nf=1
F	4635	18	4635	10	17	Nf=3
F	4655	16	4655	9	15	Nf=4
F	4699	23	4699	13	22	Nf=1
F	4719	26	4719	14	25	Nf=1
F	4735	18	4735	11	17	Nf=7
F	4763	26	4763	16	25	Nf=10
F	4767	24	4767	14	23	Nf=5
F	4775	21	4775	10	20	Nf=1
F	4799	17	4799	10	16	Nf=1
F	4839	20	4839	12	19	Nf=4
F	4847	23	4847	13	22	Nf=1
F	4863	36	4863	21	35	Nf=1
F	4891	45	4891	28	44	Nf=22
F	4935	24	4935	14	23	Nf=6
F	4967	26	4967	15	25	Nf=3
F	4991	18	4991	10	17	Nf=1
F	5055	24	5055	13	23	Nf=1
F	5087	15	5087	9	14	Nf=5
F	5119	39	5119	24	38	Nf=2
F	5147	36	5147	22	35	Nf=3
F	5151	34	5151	21	33	Nf=7
F	5211	22	5211	12	21	Nf=1
F	5223	18	5223	11	17	Nf=11
F	5231	16	5231	9	15	Nf=1
F	5247	23	5247	12	22	Nf=1
F	5279	24	5279	14	23	Nf=1
F	5287	20	5287	11	19	Nf=1
F	5311	16	5311	9	15	Nf=1
F	5343	21	5343	10	20	Nf=1
F	5351	30	5351	18	29	Nf=2
F	5359	23	5359	14	22	Nf=4
F	5375	19	5375	10	18	Nf=1
F	5403	22	5403	13	21	Nf=2
F	5423	20	5423	10	19	Nf=1
F	5447	28	5447	17	27	Nf=3
F	5479	26	5479	16	25	Nf=8
F	5503	42	5503	26	41	Nf=11
F	5535	28	5535	17	27	Nf=2
F	5567	37	5567	22	36	Nf=1
F	5599	18	5599	9	17	Nf=1
F	5631	16	5631	9	15	Nf=1
F	5659	26	5659	13	25	Nf=1
F	5663	21	5663	10	20	Nf=1
F	5679	21	5679	12	20	Nf=1
F	5735	25	5735	15	24	Nf=3
F	5759	36	5759	22	35	Nf=2
F	5791	33	5791	20	32	Nf=2
F	5823	24	5823	10	23	Nf=1
F	5863	19	5863	10	18	Nf=1
F	5887	27	5887	15	26	Nf=1
F	5915	45	5915	24	44	Nf=1
F	5991	29	5991	16	28	Nf=1
F	6015	23	6015	13	22	Nf=1
F	6055	19	6055	11	18	Nf=14
F	6079	19	6079	11	18	Nf=1
F	6139	20	6139	11	19	Nf=1
F	6143	51	6143	31	50	Nf=1
F	6171	56	6171	35	55	Nf=28
F	6175	17	6175	9	16	Nf=1
F	6191	29	6191	18	28	Nf=59
F	6207	18	6207	10	17	Nf=2
F	6235	18	6235	11	17	Nf=12
F	6247	18	6247	10	17	Nf=2
F	6255	17	6255	9	16	Nf=1
F	6271	15	6271	9	14	Nf=3
F	6303	29	6303	15	28	Nf=1
F	6311	37	6311	21	36	Nf=1
F	6367	23	6367	11	22	Nf=1
F	6383	70	6383	43	69	Nf=2
F	6395	23	6395	14	22	Nf=6
F	6399	19	6399	11	18	Nf=1
F	6427	25	6427	13	24	Nf=1
F	6463	25	6463	14	24	Nf=1
F	6471	51	6471	31	50	Nf=1
F	6503	16	6503	9	15	Nf=4
F	6591	45	6591	28	44	Nf=8
F	6623	28	6623	16	27	Nf=2
F	6639	18	6639	11	17	Nf=12
F	6655	42	6655	22	41	Nf=1
F	6703	17	6703	10	16	Nf=2
F	6759	16	6759	9	15	Nf=1
F	6767	20	6767	11	19	Nf=1
F	6783	16	6783	9	15	Nf=3
F	6811	29	6811	18	28	Nf=45
F	6823	38	6823	23	37	Nf=18
F	6847	21	6847	11	20	Nf=1
F	6887	58	6887	36	57	Nf=4
F	6895	22	6895	13	21	Nf=1
F	6907	17	6907	9	16	Nf=1
F	6911	48	6911	29	47	Nf=1
F	6939	29	6939	15	28	Nf=1
F	6975	15	6975	9	14	Nf=4
F	7015	15	7015	9	14	Nf=4
F	7039	18	7039	11	17	Nf=8
F	7103	17	7103	10	16	Nf=1
F	7135	29	7135	18	28	Nf=51
F	7151	23	7151	13	22	Nf=2
F	7163	20	7163	9	19	Nf=1
F	7167	34	7167	21	33	Nf=4
F	7195	20	7195	12	19	Nf=3
F	7199	16	7199	9	15	Nf=1
F	7231	22	7231	11	21	Nf=1
F	7271	22	7271	12	21	Nf=1
F	7279	58	7279	36	57	Nf=4
F	7295	32	7295	19	31	Nf=3
F	7323	31	7323	17	30	Nf=1
F	7327	23	7327	14	22	Nf=4
F	7335	25	7335	15	24	Nf=2
F	7359	45	7359	27	44	Nf=1
F	7407	31	7407	13	30	Nf=1
F	7419	15	7419	9	14	Nf=6
F	7423	39	7423	23	38	Nf=1
F	7451	18	7451	11	17	Nf=16
F	7471	20	7471	11	19	Nf=1
F	7487	17	7487	9	16	Nf=1
F	7527	75	7527	46	74	Nf=1
F	7551	23	7551	11	22	Nf=1
F	7583	23	7583	12	22	Nf=1
F	7615	23	7615	12	22	Nf=1
F	7647	23	7647	14	22	Nf=7
F	7663	26	7663	16	25	Nf=8
F	7679	38	7679	23	37	Nf=1
F	7707	21	7707	12	20	Nf=3
F	7711	21	7711	11	20	Nf=1
F	7727	33	7727	20	32	Nf=3
F	7783	18	7783	9	17	Nf=1
F	7807	26	7807	13	25	Nf=1
F	7835	17	7835	10	16	Nf=2
F	7839	26	7839	15	25	Nf=1
F	7871	22	7871	11	21	Nf=1
F	7919	15	7919	9	14	Nf=4
F	7935	43	7935	25	42	Nf=1
F	7963	76	7963	45	75	Nf=1
F	8027	26	8027	16	25	Nf=13
F	8039	21	8039	12	20	Nf=2
F	8063	18	8063	9	17	Nf=1
F	8095	17	8095	10	16	Nf=2
F	8127	47	8127	27	46	Nf=1
F	8175	26	8175	15	25	Nf=1
F	8187	16	8187	9	15	Nf=1
F	8191	45	8191	27	44	Nf=1
F	8219	25	8219	15	24	Nf=2
F	8223	29	8223	16	28	Nf=1
F	8239	28	8239	15	27	Nf=1
F	8255	30	8255	18	29	Nf=61
F	8263	15	8263	9	14	Nf=6
F	8283	21	8283	12	20	Nf=1
F	8295	40	8295	23	39	Nf=1
F	8303	27	8303	16	26	Nf=1
F	8319	21	8319	12	20	Nf=1
F	8351	36	8351	21	35	Nf=1
F	8359	51	8359	30	50	Nf=1
F	8415	39	8415	22	38	Nf=1
F	8431	16	8431	9	15	Nf=3
F	8443	27	8443	16	26	Nf=1
F	8475	28	8475	16	27	Nf=2
F	8511	29	8511	18	28	Nf=53
F	8519	20	8519	11	19	Nf=1
F	8551	18	8551	10	17	Nf=2
F	8607	21	8607	12	20	Nf=3
F	8639	35	8639	21	34	Nf=1
F	8671	18	8671	10	17	Nf=2
F	8687	20	8687	12	19	Nf=3
F	8703	28	8703	17	27	Nf=2
F	8751	23	8751	12	22	Nf=1
F	8795	18	8795	9	17	Nf=1
F	8831	26	8831	14	25	Nf=1
F	8859	29	8859	16	28	Nf=1
F	8863	15	8863	9	14	Nf=3
F	8895	32	8895	17	31	Nf=1
F	8935	30	8935	18	29	Nf=1
F	8943	32	8943	19	31	Nf=1
F	8955	19	8955	11	18	Nf=2
F	8959	73	8959	43	72	Nf=1
F	8987	28	8987	15	27	Nf=1
F	9023	18	9023	11	17	Nf=12
F	9031	23	9031	14	22	Nf=6
F	9051	17	9051	9	16	Nf=1
F	9063	22	9063	12	21	Nf=1
F	9087	16	9087	9	15	Nf=1
F	9119	18	9119	10	17	Nf=1
F	9151	23	9151	13	22	Nf=1
F	9183	56	9183	35	55	Nf=23
F	9199	18	9199	10	17	Nf=1
F	9215	50	9215	30	49	Nf=1
F	9243	24	9243	13	23	Nf=1
F	9247	22	9247	13	21	Nf=1
F	9287	27	9287	16	26	Nf=16
F	9307	15	9307	9	14	Nf=5
F	9319	18	9319	10	17	Nf=1
F	9343	18	9343	11	17	Nf=9
F	9371	17	9371	9	16	Nf=1
F	9375	25	9375	9	24	Nf=1
F	9447	15	9447	9	14	Nf=5
F	9455	28	9455	14	27	Nf=1
F	9467	29	9467	18	28	Nf=57
F	9471	19	9471	11	18	Nf=1
F	9499	24	9499	14	23	Nf=1
F	9535	25	9535	14	24	Nf=1
F	9543	20	9543	10	19	Nf=1
F	9575	26	9575	16	25	Nf=13
F	9599	18	9599	10	17	Nf=1
F	9631	31	9631	19	30	Nf=4
F	9663	56	9663	35	55	Nf=18
F	9695	24	9695	13	23	Nf=1
F	9711	17	9711	9	16	Nf=1
F	9727	34	9727	20	33	Nf=2
F	9775	28	9775	17	27	Nf=3
F	9831	18	9831	11	17	Nf=12
F	9855	29	9855	18	28	Nf=22
F	9883	22	9883	11	21	Nf=1
F	9887	44	9887	27	43	Nf=2
F	9959	16	9959	9	15	Nf=5
F	9967	26	9967	14	25	Nf=1
F	9983	26	9983	16	25	Nf=7
F	10011	56	10011	32	55	Nf=1
F	10075	16	10075	9	15	Nf=1
F	10087	102	10087	64	101	Nf=36
F	10111	18	10111	11	17	Nf=9
F	10143	29	10143	16	28	Nf=1
F	10151	15	10151	9	14	Nf=6
F	10235	37	10235	22	36	Nf=4
F	10239	35	10239	21	34	Nf=4
F	10303	35	10303	21	34	Nf=2
F	10311	21	10311	12	20	Nf=4
F	10331	53	10331	33	52	Nf=9
F	10343	21	10343	12	20	Nf=1
F	10351	30	10351	18	29	Nf=42
F	10367	47	10367	28	46	Nf=1
F	10399	21	10399	11	20	Nf=1
F	10407	29	10407	18	28	Nf=46
F	10479	31	10479	19	30	Nf=4
F	10491	24	10491	14	23	Nf=6
F	10495	19	10495	11	18	Nf=9
F	10559	17	10559	10	16	Nf=2
F	10567	20	10567	11	19	Nf=1
F	10599	37	10599	22	36	Nf=1
F	10655	16	10655	9	15	Nf=1
F	10687	21	10687	12	20	Nf=1
F	10719	23	10719	13	22	Nf=1
F	10735	16	10735	9	15	Nf=1
F	10751	33	10751	20	32	Nf=1
F	10843	27	10843	14	26	Nf=1
F	10863	17	10863	9	16	Nf=1
F	10879	41	10879	24	40	Nf=1
F	10907	21	10907	11	20	Nf=1
F	10911	40	10911	22	39	Nf=1
F	10919	57	10919	35	56	Nf=2
F	10943	31	10943	18	30	Nf=1
F	10983	30	10983	18	29	Nf=40
F	10991	22	10991	13	21	Nf=2
F	11003	24	11003	14	23	Nf=1
F	11007	19	11007	11	18	Nf=1
F	11035	20	11035	10	19	Nf=1
F	11071	29	11071	17	28	Nf=1
F	11079	25	11079	9	24	Nf=1
F	11111	30	11111	12	29	Nf=1
F	11135	38	11135	22	37	Nf=1
F	11175	36	11175	21	35	Nf=2
F	11199	23	11199	14	22	Nf=5
F	11247	18	11247	11	17	Nf=13
F	11263	53	11263	30	52	Nf=1
F	11291	74	11291	45	73	Nf=1
F	11295	24	11295	13	23	Nf=1
F	11355	23	11355	12	22	Nf=1
F	11367	26	11367	16	25	Nf=9
F	11375	15	11375	9	14	Nf=4
F	11391	50	11391	28	49	Nf=1
F	11419	28	11419	14	27	Nf=1
F	11423	22	11423	11	21	Nf=1
F	11431	17	11431	10	16	Nf=2
F	11455	15	11455	9	14	Nf=4
F	11495	25	11495	15	24	Nf=2
F	11503	45	11503	27	44	Nf=2
F	11515	34	11515	20	33	Nf=2
F	11519	37	11519	22	36	Nf=1
F	11547	31	11547	16	30	Nf=1
F	11567	16	11567	9	15	Nf=5
F	11583	22	11583	13	21	Nf=1
F	11591	29	11591	18	28	Nf=67
F	11623	49	11623	30	48	Nf=46
F	11679	19	11679	9	18	Nf=1
F	11711	25	11711	12	24	Nf=1
F	11759	20	11759	12	19	Nf=3
F	11775	28	11775	15	27	Nf=1
F	11803	21	11803	12	20	Nf=4
F	11807	16	11807	9	15	Nf=4
F	11823	18	11823	10	17	Nf=1
F	11903	42	11903	24	41	Nf=1
F	11931	49	11931	30	48	Nf=2
F	11935	25	11935	14	24	Nf=1
F	11967	16	11967	9	15	Nf=3
F	12007	19	12007	10	18	Nf=1
F	12015	23	12015	14	22	Nf=4
F	12031	28	12031	16	27	Nf=1
F	12059	20	12059	11	19	Nf=1
F	12123	23	12123	13	22	Nf=2
F	12135	40	12135	24	39	Nf=3
F	12191	20	12191	12	19	Nf=3
F	12199	19	12199	11	18	Nf=16
F	12223	37	12223	21	36	Nf=1
F	12287	44	12287	26	43	Nf=1
F	12315	20	12315	12	19	Nf=4
F	12319	15	12319	9	14	Nf=4
F	12335	23	12335	14	22	Nf=7
F	12359	27	12359	14	26	Nf=1
F	12379	18	12379	11	17	Nf=14
F	12399	76	12399	47	75	Nf=3
F	12447	47	12447	27	46	Nf=1
F	12455	26	12455	15	25	Nf=1
F	12479	20	12479	11	19	Nf=1
F	12511	18	12511	9	17	Nf=1
F	12527	29	12527	18	28	Nf=51
F	12539	50	12539	29	49	Nf=1
F	12543	16	12543	9	15	Nf=1
F	12571	23	12571	9	22	Nf=1
F	12591	20	12591	11	19	Nf=2
F	12607	24	12607	14	23	Nf=4
F	12615	20	12615	10	19	Nf=1
F	12703	71	12703	43	70	Nf=1
F	12735	28	12735	16	27	Nf=1
F	12767	27	12767	16	26	Nf=13
F	12783	31	12783	18	30	Nf=1
F	12799	20	12799	11	19	Nf=1
F	12827	17	12827	9	16	Nf=1
F	12847	25	12847	12	24	Nf=1
F	12891	23	12891	13	22	Nf=1
F	12911	20	12911	11	19	Nf=1
F	12927	31	12927	17	30	Nf=1
F	12955	31	12955	18	30	Nf=2
F	12959	34	12959	20	33	Nf=1
F	12967	17	12967	9	16	Nf=1
F	12991	28	12991	14	27	Nf=1
F	13031	19	13031	11	18	Nf=1
F	13039	25	13039	15	24	Nf=2
F	13055	27	13055	16	26	Nf=1
F	13083	15	13083	9	14	Nf=4
F	13127	22	13127	11	21	Nf=1
F	13159	22	13159	12	21	Nf=1
F	13183	46	13183	28	45	Nf=2
F	13247	25	13247	13	24	Nf=1
F	13279	18	13279	10	17	Nf=2
F	13311	28	13311	17	27	Nf=2
F	13339	19	13339	10	18	Nf=1
F	13343	31	13343	16	30	Nf=1
F	13403	29	13403	17	28	Nf=1
F	13415	31	13415	18	30	Nf=1
F	13423	46	13423	28	45	Nf=2
F	13439	72	13439	42	71	Nf=1
F	13471	23	13471	11	22	Nf=1
F	13479	20	13479	11	19	Nf=2
F	13503	42	13503	26	41	Nf=7
F	13535	17	13535	10	16	Nf=3
F	13543	32	13543	19	31	Nf=1
F	13551	68	13551	42	67	Nf=2
F	13567	17	13567	9	16	Nf=1
F	13595	21	13595	11	20	Nf=1
F	13615	17	13615	10	16	Nf=2
F	13639	20	13639	11	19	Nf=1
F	13671	18	13671	11	17	Nf=13
F	13695	16	13695	9	15	Nf=4
F	13727	19	13727	11	18	Nf=8
F	13759	54	13759	32	53	Nf=1
F	13791	18	13791	11	17	Nf=11
F	13823	49	13823	29	48	Nf=1
F	13851	16	13851	9	15	Nf=1
F	13855	17	13855	10	16	Nf=2
F	13871	18	13871	11	17	Nf=11
F	13927	15	13927	9	14	Nf=5
F	13951	18	13951	11	17	Nf=10
F	13983	38	13983	22	37	Nf=1
F	14015	17	14015	10	16	Nf=2
F	14055	35	14055	18	34	Nf=1
F	14079	30	14079	16	29	Nf=1
F	14107	47	14107	27	46	Nf=1
F	14183	21	14183	12	20	Nf=3
F	14207	15	14207	9	14	Nf=3
F	14247	26	14247	16	25	Nf=15
F	14271	16	14271	9	15	Nf=1
F	14331	15	14331	9	14	Nf=7
F	14335	35	14335	21	34	Nf=1
F	14363	18	14363	11	17	Nf=18
F	14367	27	14367	16	26	Nf=11
F	14383	19	14383	11	18	Nf=18
F	14399	17	14399	9	16	Nf=1
F	14427	28	14427	17	27	Nf=3
F	14439	17	14439	9	16	Nf=1
F	14447	30	14447	18	29	Nf=2
F	14463	21	14463	12	20	Nf=1
F	14495	54	14495	33	53	Nf=6
F	14503	20	14503	11	19	Nf=1
F	14559	59	14559	36	58	Nf=1
F	14575	28	14575	16	27	Nf=1
F	14587	22	14587	12	21	Nf=1
F	14591	33	14591	19	32	Nf=1
F	14619	27	14619	16	26	Nf=14
F	14655	24	14655	14	23	Nf=1
F	14663	27	14663	16	26	Nf=2
F	14695	37	14695	23	36	Nf=23
F	14783	28	14783	17	27	Nf=2
F	14815	32	14815	13	31	Nf=1
F	14831	43	14831	26	42	Nf=1
F	14847	38	14847	23	37	Nf=13
F	14895	18	14895	9	17	Nf=1
F	14951	25	14951	13	24	Nf=1
F	14959	29	14959	18	28	Nf=51
F	14975	25	14975	15	24	Nf=2
F	15003	25	15003	15	24	Nf=2
F	15015	30	15015	18	29	Nf=54
F	15039	84	15039	52	83	Nf=2
F	15079	26	15079	15	25	Nf=1
F	15087	29	15087	17	28	Nf=1
F	15099	27	15099	15	26	Nf=1
F	15103	19	15103	11	18	Nf=10
F	15131	72	15131	45	71	Nf=11
F	15167	17	15167	10	16	Nf=2
F	15207	17	15207	10	16	Nf=2
F	15231	24	15231	12	23	Nf=1
F	15295	18	15295	9	17	Nf=1
F	15327	27	15327	16	26	Nf=2
F	15343	16	15343	9	15	Nf=4
F	15355	20	15355	11	19	Nf=1
F	15359	34	15359	20	33	Nf=1
F	15387	20	15387	12	19	Nf=4
F	15391	23	15391	13	22	Nf=2
F	15423	18	15423	10	17	Nf=2
F	15463	33	15463	16	32	Nf=1
F	15471	29	15471	18	28	Nf=34
F	15487	17	15487	10	16	Nf=1
F	15515	15	15515	9	14	Nf=5
F	15519	54	15519	32	53	Nf=1
F	15527	29	15527	17	28	Nf=4
F	15551	46	15551	27	45	Nf=1
F	15599	20	15599	10	19	Nf=1
F	15611	28	15611	17	27	Nf=4
F	15615	27	15615	13	26	Nf=1
F	15643	21	15643	10	20	Nf=1
F	15663	22	15663	13	21	Nf=2
F	15679	22	15679	13	21	Nf=2
F	15719	20	15719	12	19	Nf=3
F	15743	18	15743	10	17	Nf=2
F	15775	19	15775	11	18	Nf=1
F	15807	18	15807	11	17	Nf=7
F	15839	16	15839	9	15	Nf=1
F	15855	15	15855	9	14	Nf=4
F	15871	44	15871	25	43	Nf=1
F	15899	36	15899	21	35	Nf=1
F	15903	23	15903	14	22	Nf=5
F	15919	16	15919	9	15	Nf=1
F	15975	18	15975	11	17	Nf=13
F	15999	28	15999	17	27	Nf=2
F	16027	18	16027	9	17	Nf=1
F	16031	20	16031	11	19	Nf=1
F	16063	30	16063	18	29	Nf=45
F	16111	25	16111	15	24	Nf=3
F	16127	32	16127	19	31	Nf=1
F	16155	42	16155	26	41	Nf=9
F	16219	15	16219	9	14	Nf=6
F	16231	25	16231	15	24	Nf=2
F	16255	18	16255	11	17	Nf=10
F	16287	19	16287	9	18	Nf=1
F	16319	40	16319	23	39	Nf=1
F	16367	29	16367	18	28	Nf=84
F	16379	56	16379	34	55	Nf=1
F	16383	46	16383	27	45	Nf=1

Notes

D_exact et F sont relevées au module 2^{m_{stable}} avec m_{stable}=\max(m, A+1), où m est le palier du domaine, afin de figer le mot de valuations du témoin.
D_brother_local encode une dépendance locale (palier du domaine) vers un mate_exact ; elle n’est pas utilisée ici comme clause universelle autonome.

36 KiB Raw Permalink Blame History Unescape Escape