**Motivations:** - Sync certs_shifted artefacts, script and README. **Root causes:** N/A **Correctifs:** N/A **Evolutions:** - collatz_build_hensel_chain_leaves_shifted.py - README.md - docs/artefacts/collatz/refinement_K/.../certs_shifted/*.json **Pages affectées:** - applications/collatz/collatz_k_scripts/README.md - applications/collatz/collatz_k_scripts/collatz_build_hensel_chain_leaves_shifted.py - docs/artefacts/collatz/refinement_K/palier2p15/hensel_chain_leaves/certs_shifted/
5.3 KiB
Auteur : Équipe 4NK
Targeted leaves (attempt) and diagnostics
Objectif
Réduire tracked.max/p99 sur une liste fixe de racines ouvertes (top‑N par lb_any) au palier 2^15,
en introduisant une grammaire de feuilles capable de payer localement une dette d’observabilité,
sans déclencher une explosion combinatoire du raffinement binaire.
Tentative implémentée
applications/collatz/collatz_k_scripts/collatz_build_targeted_refinement_leaves.pyapplications/collatz/collatz_k_scripts/collatz_verify_targeted_refinement_leaves.py
Principe : fermer chaque racine suivie r0 via un certificat de raffinement profond (cap par défaut 160)
en n’autorisant comme feuilles terminales que D_exact, F, et D_minor.
Résultat
Sur la liste fixe tracked_roots_lb_any_top200_mod2p15_to2p18.txt, aucun certificat n’a été construit (closed_roots=0).
Artefacts :
docs/artefacts/collatz/refinement_K/palier2p15/targeted_leaves/clauses_targeted_refinement_leaves_mod2p15.jsondocs/artefacts/collatz/refinement_K/palier2p15/targeted_leaves/verification_targeted_refinement_leaves_mod2p15.json
Diagnostic déterministe (root cause)
Fait structurel mesuré (au premier raffinement 2^15→2^16)
Sur les racines suivies, les deux enfants (low/high) au niveau m=16 n’ont pas de clause terminale immédiatement décidable (A+1 <= 16) dans la grammaire D_exact/F (avec k_max=t_max=256).
Ce fait est mesuré et versionné dans :
applications/collatz/collatz_k_scripts/collatz_diagnose_targeted_leaves_failure.pydocs/artefacts/collatz/refinement_K/palier2p15/targeted_leaves/diagnostic_targeted_leaves_failure_mod2p15.md
Extrait (colonnes immediate_low@16, immediate_high@16) :
root=27:no/no, etlb_root=60root=703:no/no, etlb_root=84root=2887:no/no, etlb_root=136
Interprétation mathématique
Dans la grammaire de fermeture par raffinement binaire, une racine r0 est fermée si et seulement si les deux enfants à chaque split sont fermables (directement ou récursivement).
Quand immediate_low@16=no et immediate_high@16=no, fermer r0 impose mécaniquement de raffiner plus profond au moins jusqu’à une profondeur où une clause terminale devient décidable. Le diagnostic donne des bornes inférieures lb_root typiquement dans [50, 136] sur les racines extrêmes.
Le point bloquant n’est pas “le cap 160” en tant que tel : c’est le fait que, sans règle de compression,
la fermeture par scission binaire doit couvrir un arbre de taille 2^{(lb\_root-16)} nœuds au minimum dans le cas défavorable.
Pour lb_root=136, cela correspond à une explosion combinatoire hors de portée d’un certificat fini exploitable.
Conclusion (root cause)
L’échec des certificats “targeted leaves” vient de la combinaison :
- absence de feuilles terminales décidables au premier niveau de raffinement (m=16) sur les racines extrêmes ;
- bornes inférieures
lb_roottrès élevées, qui rendent le raffinement binaire naïf exponentiel ; - grammaire de feuilles trop faible (D/F/D_minor) pour “absorber” la dette sans fermer récursivement les deux enfants.
Formalisation et plan d'implémentation
Les quatre pistes d'extension sont formalisées dans applications/collatz/conjoncture_collatz.md (section « Extensions de grammaire pour les cas no/no »). Le plan d'implémentation aligné sur these/livre_jeune_adulte.md est dans docs/features/collatz_grammar_extensions_implementation_plan.md.
Phase 1 exécutée (extension mécanique)
La Phase 1 a été exécutée : clauses terminales D/F pour m=15..21 (k_max=t_max=16), clauses D_minor pour m=20,21 (k=12,u=20 ; k=12,u=21 ; k=13,u=21), bundle étendu à max_palier=21. Rapport et métriques : docs/artefacts/collatz/refinement_K/palier2p15/phase1_grammar_extensions_report.md. Résultat : Δ(tracked.max)=0, Δ(tracked.p99)=0 ; critère de succès non atteint.
Phase 3 exécutée (chaîne Hensel décalée)
Script collatz_build_hensel_chain_leaves_shifted.py : chaîne Hensel démarrant à m=19 pour les résidus dont le frère à m=19 est fermable. 1373 résidus fermés à m=19. open_roots : 1349 → 1101 (−248). tracked.max/p99 inchangés (les racines fermées ne sont pas dans le top 200).
Option A + B exécutées
- Option A : extension à M_max=24, D_minor m=22,23,24. Aucun impact sur tracked.max/p99. Rapport :
option_a_extension_m24_report.md. - Option B : Hensel start_m=20,21. Aucun impact supplémentaire. Rapport :
option_b_hensel_m20_m21_report.md.
Le diagnostic ciblé est exécuté par le bundle avec --tracked-roots-file ; sortie : diagnostic_targeted_leaves_failure_mod2p15.md dans le répertoire du bundle.
Guidage pour une grammaire plus puissante
Une grammaire réduisant effectivement tracked.max/p99 doit introduire une règle/feuille capable de :
- fermer un sous-arbre en taille linéaire en la profondeur (compression),
- typiquement en exploitant des structures de type chaîne henselienne (un seul embranchement “dur”, le frère se ferme par une clause uniforme),
- ou une règle de “réparation/recombinaison” explicitant comment une branche survivante peut être traitée sans imposer la fermeture complète des deux enfants au même niveau de description.