nicolas.cantu/algo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity
algo/docs/artefacts/collatz/universal_clauses/clauses_universelles.md
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

415 lines
18 KiB
Markdown
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

**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.json`
## Domaine
- palier (domaine des témoins) : 2^13
- max(2^m_stable) observé : 2^85
## Compteurs
- total : 384
- D_exact : 27
- F : 330
- D_brother_local : 27
## Table (extrait)
| kind | source_n | m_stable | residue_mod_2^m | k/t | A | N0/Nf | mate_exact |
| --- | --- | --- | --- | --- | --- | --- | --- |
| D_brother_local | 127 | | | 8 | 12 | | 4223 |
| D_brother_local | 359 | | | 8 | 12 | | 4455 |
| D_brother_local | 763 | | | 8 | 12 | | 4859 |
| D_brother_local | 831 | | | 8 | 12 | | 4927 |
| D_brother_local | 1095 | | | 8 | 12 | | 5191 |
| D_brother_local | 1275 | | | 8 | 12 | | 5371 |
| D_brother_local | 1343 | | | 8 | 12 | | 5439 |
| D_brother_local | 1775 | | | 8 | 12 | | 5871 |
| D_brother_local | 2119 | | | 8 | 12 | | 6215 |
| D_brother_local | 2651 | | | 8 | 12 | | 6747 |
| D_brother_local | 2719 | | | 8 | 12 | | 6815 |
| D_brother_local | 2983 | | | 8 | 12 | | 7079 |
| D_brother_local | 3163 | | | 8 | 12 | | 7259 |
| D_brother_local | 3303 | | | 8 | 12 | | 7399 |
| D_brother_local | 3815 | | | 8 | 12 | | 7911 |
| D_brother_local | 4007 | | | 8 | 12 | | 8103 |
| D_brother_local | 4351 | | | 8 | 12 | | 255 |
| D_brother_local | 4635 | | | 8 | 12 | | 539 |
| D_brother_local | 4775 | | | 8 | 12 | | 679 |
| D_brother_local | 5287 | | | 8 | 12 | | 1191 |
| D_brother_local | 5659 | | | 8 | 12 | | 1563 |
| D_brother_local | 6079 | | | 8 | 12 | | 1983 |
| D_brother_local | 6171 | | | 8 | 12 | | 2075 |
| D_brother_local | 6191 | | | 8 | 12 | | 2095 |
| D_brother_local | 6703 | | | 8 | 12 | | 2607 |
| D_brother_local | 7135 | | | 8 | 12 | | 3039 |
| D_brother_local | 7647 | | | 8 | 12 | | 3551 |
| 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 | |
| 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 | 159 | 23 | 159 | 13 | 22 | Nf=1 | |
| F | 167 | 31 | 167 | 18 | 30 | Nf=2 | |
| F | 191 | 18 | 191 | 9 | 17 | Nf=1 | |
| 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 | 303 | 19 | 303 | 9 | 18 | Nf=1 | |
| F | 319 | 24 | 319 | 13 | 23 | Nf=1 | |
| F | 327 | 23 | 327 | 13 | 22 | 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 | 623 | 19 | 623 | 9 | 18 | Nf=1 | |
| 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 | 767 | 19 | 767 | 10 | 18 | Nf=1 | |
| F | 795 | 28 | 795 | 17 | 27 | Nf=3 | |
| 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 | 1115 | 24 | 1115 | 14 | 23 | Nf=6 | |
| F | 1127 | 23 | 1127 | 12 | 22 | Nf=1 | |
| F | 1135 | 16 | 1135 | 9 | 15 | 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 | 1215 | 16 | 1215 | 9 | 15 | Nf=1 | |
| F | 1247 | 20 | 1247 | 9 | 19 | Nf=1 | |
| F | 1255 | 21 | 1255 | 12 | 20 | Nf=3 | |
| F | 1263 | 27 | 1263 | 16 | 26 | Nf=6 | |
| F | 1279 | 25 | 1279 | 14 | 24 | Nf=1 | |
| F | 1307 | 35 | 1307 | 21 | 34 | Nf=1 | |
| F | 1327 | 21 | 1327 | 9 | 20 | 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 | 1567 | 20 | 1567 | 9 | 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 | 1727 | 20 | 1727 | 9 | 19 | Nf=1 | |
| F | 1767 | 20 | 1767 | 12 | 19 | Nf=3 | |
| 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 | 2079 | 17 | 2079 | 9 | 16 | Nf=1 | |
| F | 2111 | 84 | 2111 | 50 | 83 | 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 | 2271 | 17 | 2271 | 9 | 16 | Nf=1 | |
| 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 | 2331 | 17 | 2331 | 9 | 16 | 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 | 2663 | 16 | 2663 | 9 | 15 | Nf=1 | |
| 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 | 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 | 3007 | 23 | 3007 | 14 | 22 | Nf=5 | |
| F | 3055 | 31 | 3055 | 18 | 30 | Nf=1 | |
| F | 3067 | 18 | 3067 | 9 | 17 | 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 | 3135 | 21 | 3135 | 9 | 20 | 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 | 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 | 3455 | 21 | 3455 | 9 | 20 | Nf=1 | |
| 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 | 3687 | 19 | 3687 | 9 | 18 | Nf=1 | |
| 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 | 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 | 3967 | 20 | 3967 | 9 | 19 | Nf=1 | |
| F | 3999 | 20 | 3999 | 12 | 19 | Nf=2 | |
| F | 4031 | 17 | 4031 | 9 | 16 | Nf=1 | |
| F | 4079 | 18 | 4079 | 9 | 17 | Nf=1 | |
| F | 4091 | 16 | 4091 | 9 | 15 | Nf=2 | |
| 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 | 4159 | 18 | 4159 | 9 | 17 | Nf=1 | |
| F | 4167 | 21 | 4167 | 12 | 20 | Nf=4 | |
| F | 4187 | 18 | 4187 | 9 | 17 | Nf=1 | |
| F | 4199 | 18 | 4199 | 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 | 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 | 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 | 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 | 4955 | 17 | 4955 | 9 | 16 | Nf=2 | |
| F | 4967 | 26 | 4967 | 15 | 25 | Nf=3 | |
| F | 4991 | 18 | 4991 | 10 | 17 | Nf=1 | |
| F | 5023 | 18 | 5023 | 9 | 17 | Nf=1 | |
| F | 5055 | 24 | 5055 | 13 | 23 | Nf=1 | |
| F | 5087 | 15 | 5087 | 9 | 14 | Nf=5 | |
| F | 5103 | 18 | 5103 | 9 | 17 | Nf=1 | |
| 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 | 5275 | 17 | 5275 | 9 | 16 | Nf=2 | |
| F | 5279 | 24 | 5279 | 14 | 23 | 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 | 5615 | 17 | 5615 | 9 | 16 | Nf=1 | |
| F | 5631 | 16 | 5631 | 9 | 15 | 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 | 5787 | 17 | 5787 | 9 | 16 | Nf=1 | |
| 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 | 5979 | 16 | 5979 | 9 | 15 | Nf=2 | |
| F | 5991 | 29 | 5991 | 16 | 28 | Nf=1 | |
| F | 6015 | 23 | 6015 | 13 | 22 | Nf=1 | |
| F | 6047 | 17 | 6047 | 9 | 16 | Nf=1 | |
| F | 6055 | 19 | 6055 | 11 | 18 | Nf=14 | |
| F | 6139 | 20 | 6139 | 11 | 19 | Nf=1 | |
| F | 6143 | 51 | 6143 | 31 | 50 | Nf=1 | |
| F | 6175 | 17 | 6175 | 9 | 16 | Nf=1 | |
| 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 | 6559 | 16 | 6559 | 9 | 15 | Nf=1 | |
| 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 | 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 | 6983 | 18 | 6983 | 9 | 17 | Nf=1 | |
| 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 | 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 | 7495 | 19 | 7495 | 9 | 18 | 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 | 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 | |
## 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.
Reference in New Issue View Git Blame Copy Permalink