collatz: formalize universal D/F clauses and report all C2 transitions

**Motivations:**
- Convert observed witnesses into universal clause statements usable in well-founded induction
- Ensure c2_projective run report reflects every discovered transition

**Root causes:**
- H4/H5 universality bridge was implicit
- c2_projective run report only displayed legacy checks (m14→m16)

**Correctifs:**
- Add explicit universal D/F clause forms, thresholds, and induction closure schema
- Extend c2_projective metrics rendering to iterate over verification JSON transitions

**Evolutions:**
- None

**Pages affectées:**
- applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md
- applications/collatz/collatz_k_scripts/collatz_generate_run_report.py
- docs/collatz_run_report_2026-03-09_c2_projective.md

applications/collatz/collatz_k_scripts/collatz_generate_run_report.py

@@ -119,6 +119,17 @@ class LocalH6Metrics:
     certificate_paliers: list[tuple[str, int]]
 
 
+@dataclass(frozen=True)
+class C2TransitionMetric:
+    palier_parent: int
+    palier_child: int
+    both_parent_count: int
+    computed_children_count: int
+    listed_residual_count: int | None
+    children_equals_listed_residual: bool | None
+    projection_mod_4096_equals_b12: bool
+
+
 @dataclass(frozen=True)
 class C2ProjectiveMetrics:
     b12_size: int
@@ -130,6 +141,7 @@ class C2ProjectiveMetrics:
     both15_size: int
     children16_size: int
     proj_both15_equals_b12: bool
+    transitions: list[C2TransitionMetric]
 
 
 @dataclass(frozen=True)
@@ -151,8 +163,11 @@ def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics:
 
     b12 = obj.get("B12")
     checks = obj.get("checks")
+    transitions = obj.get("transitions")
     if not isinstance(b12, dict) or not isinstance(checks, dict):
         raise ValueError("Invalid C2 verification JSON: missing 'B12' or 'checks'")
+    if not isinstance(transitions, list) or not all(isinstance(x, dict) for x in transitions):
+        raise ValueError("Invalid C2 verification JSON: missing 'transitions' list")
 
     c1415 = checks.get("m14_to_m15")
     c1516 = checks.get("m15_to_m16")
@@ -171,6 +186,37 @@ def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics:
             raise ValueError(f"Invalid C2 verification JSON: {k} must be bool")
         return v
 
+    def opt_int(d: dict, k: str) -> int | None:
+        v = d.get(k)
+        if v is None:
+            return None
+        if not isinstance(v, int):
+            raise ValueError(f"Invalid C2 verification JSON: {k} must be int or null")
+        return v
+
+    def opt_bool(d: dict, k: str) -> bool | None:
+        v = d.get(k)
+        if v is None:
+            return None
+        if not isinstance(v, bool):
+            raise ValueError(f"Invalid C2 verification JSON: {k} must be bool or null")
+        return v
+
+    parsed_transitions: list[C2TransitionMetric] = []
+    for t in transitions:
+        parsed_transitions.append(
+            C2TransitionMetric(
+                palier_parent=req_int(t, "palier_parent"),
+                palier_child=req_int(t, "palier_child"),
+                both_parent_count=req_int(t, "both_parent_count"),
+                computed_children_count=req_int(t, "computed_children_count"),
+                listed_residual_count=opt_int(t, "listed_residual_count"),
+                children_equals_listed_residual=opt_bool(t, "children_equals_listed_residual"),
+                projection_mod_4096_equals_b12=req_bool(t, "projection_mod_4096_equals_b12"),
+            )
+        )
+    parsed_transitions = sorted(parsed_transitions, key=lambda x: (x.palier_parent, x.palier_child))
+
     return C2ProjectiveMetrics(
         b12_size=req_int(b12, "count"),
         both14_size=req_int(c1415, "both_parent_count"),
@@ -181,6 +227,7 @@ def parse_c2_projective_metrics(verification_json: str) -> C2ProjectiveMetrics:
         both15_size=req_int(c1516, "both_parent_count"),
         children16_size=req_int(c1516, "computed_children_count"),
         proj_both15_equals_b12=req_bool(c1516, "projection_mod_4096_equals_b12"),
+        transitions=parsed_transitions,
     )
 
 
@@ -264,11 +311,22 @@ def write_c2_projective_run_report(
     lines.append("## Compteurs et métriques")
     lines.append("")
     lines.append(f"- |B12| = {metrics.b12_size}")
-    lines.append(f"- m=14: |both|={metrics.both14_size}, |children(m=15)|={metrics.children15_size}, |listed residual(m=15)|={metrics.residual15_size}")
+    for t in metrics.transitions:
-    lines.append(f"- m=14: children(m=15) == residual(m=15) : {metrics.children15_equals_residual15}")
+        if t.listed_residual_count is None:
-    lines.append(f"- m=14: both mod 4096 == B12 : {metrics.proj_both14_equals_b12}")
+            lines.append(
-    lines.append(f"- m=15: |both|={metrics.both15_size}, |children(m=16)|={metrics.children16_size}")
+                f"- m={t.palier_parent}: |both|={t.both_parent_count}, |children(m={t.palier_child})|={t.computed_children_count}"
-    lines.append(f"- m=15: both mod 4096 == B12 : {metrics.proj_both15_equals_b12}")
+            )
+        else:
+            lines.append(
+                f"- m={t.palier_parent}: |both|={t.both_parent_count}, "
+                f"|children(m={t.palier_child})|={t.computed_children_count}, "
+                f"|listed residual(m={t.palier_child})|={t.listed_residual_count}"
+            )
+        if t.children_equals_listed_residual is not None:
+            lines.append(
+                f"- m={t.palier_parent}: children(m={t.palier_child}) == residual(m={t.palier_child}) : {t.children_equals_listed_residual}"
+            )
+        lines.append(f"- m={t.palier_parent}: both mod 4096 == B12 : {t.projection_mod_4096_equals_b12}")
     lines.append("")
     lines.append("## Chemins d’artefacts (versionnés)")
     lines.append("")

applications/collatz/collatz_k_scripts/plan_lemmes_manquants_et_programme_de_preuve.md

@@ -296,6 +296,55 @@ Passer de l’instance locale au cas général exige de relier les témoins obse
 - D exact : contrôler l’extension “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N_0\)” via les formules affines (seuil \(N_0\)) ;
 - fusion : contrôler l’extension “pour tout \(n\) dans une classe modulo \(2^m\), pour tout \(n\ge N_F\)” et la propriété de réduction \(m<n\) sans la prouver seulement sur un représentant.
 
+Formalisation minimale attendue (clauses universelles).
+
+On se place dans le cadre du registre \(\mathcal{K}\), où chaque clause est indexée par :
+- un module \(2^m\) (palier) ;
+- une classe impaire \(r\in(\mathbb{Z}/2^m\mathbb{Z})^\times\) ;
+- des paramètres affines issus d’un préfixe exact (mot de valuations, somme \(A\), constante \(C\)) et/ou d’un choix de préimage.
+
+Clause D universelle (forme).
+Une clause D\((k)\) exacte sur la classe \(r\pmod{2^m}\) consiste à fixer un mot \((a_0,\dots,a_{k-1})\), sa somme \(A=\sum_{i<k}a_i\) et la constante \(C_k\) telles que, pour tout impair \(n\equiv r\pmod{2^m}\), le préfixe de valuations est identique (stabilité) et
+\[
+U^{(k)}(n)=\frac{3^k n + C_k}{2^A}.
+\]
+Sous la condition structurelle \(\Delta_D=2^A-3^k>0\), on définit le seuil
+\[
+N_0=\left\lfloor\frac{C_k}{\Delta_D}\right\rfloor+1,
+\]
+et l’énoncé universel attendu est :
+\[
+\forall n\equiv r\!\!\!\pmod{2^m},\quad n\ge N_0 \Longrightarrow U^{(k)}(n)<n.
+\]
+Cette implication est l’interface mathématique de (H4) : elle transforme une entrée `covered` d’un certificat D en une réduction stricte dans l’ordre usuel sur \(\mathbb{N}\).
+
+Clause F universelle (forme).
+Une clause F\((t)\) sur la classe \(r\pmod{2^m}\) fixe un préfixe exact de longueur \(t\) (donc \(A_t\) et \(C_t\)) et un choix \(a\in\{1,2\}\) tel que, pour tout \(n\equiv r\pmod{2^m}\),
+\[
+y(n)=U^{(t)}(n)=\frac{3^t n + C_t}{2^{A_t}}
+\]
+est impair et satisfait \(y(n)\not\equiv 0\pmod 3\) (le cas \(\equiv 0\pmod 3\) n’admet pas de préimage impaire).
+Comme \(3^t n\equiv 0\pmod 3\), la classe de \(y(n)\) modulo 3 est indépendante de \(n\) sur la classe, et le choix \(a=\mathrm{fusion\_choice\_a}(y(n))\) est constant.
+On définit alors une préimage impaire
+\[
+m(n)=\frac{2^a y(n)-1}{3},
+\]
+et, sous la condition structurelle \(\Delta_F = 3\cdot 2^{A_t}-2^a\cdot 3^t>0\), le seuil
+\[
+N_F = \mathrm{Nf\_F}(C_t,A_t,t,a),
+\]
+tel que l’énoncé universel attendu soit :
+\[
+\forall n\equiv r\!\!\!\pmod{2^m},\quad n\ge N_F \Longrightarrow \bigl(U(m(n))=y(n)\ \wedge\ m(n)<n\bigr).
+\]
+Cette implication est l’interface mathématique de (H5) : elle transforme une entrée `covered` d’un certificat F en une réduction stricte (par fusion) dans l’ordre usuel sur \(\mathbb{N}\).
+
+Compatibilité avec l’induction bien fondée (schéma H4/H5).
+Soit \(P(n)\) la propriété “l’orbite accélérée de \(n\) atteint 1”. On fixe une borne \(N^\star\) telle que, pour toute clause D/F utilisée, les implications universelles ci-dessus valent pour tous \(n\ge N^\star\) dans les classes considérées. On vérifie \(P(n)\) pour tout impair \(n<N^\star\) (validation de base finie), puis on conclut \(P(n)\) pour tout impair \(n\ge N^\star\) par induction forte sur \(n\) :
+- si une clause D s’applique à \(n\), on obtient \(U^{(k)}(n)<n\), donc \(P(U^{(k)}(n))\Rightarrow P(n)\) ;
+- si une clause F s’applique à \(n\), on obtient \(m(n)<n\) et \(U(m(n))=U^{(t)}(n)\), donc \(P(m(n))\Rightarrow P(n)\).
+L’ordre usuel sur \(\mathbb{N}\) fournit le bon ordre nécessaire à la clôture.
+
 En l’absence de ce passage, l’instance locale reste un artefact d’audit (citable), et le verrou global est formulé comme “uniformiser / itérer” (C1+C2→C3) sur des paliers arbitraires.
 
 ## Conclusion

docs/collatz_run_report_2026-03-09_c2_projective.md

@@ -9,7 +9,7 @@
 
 ## Code et reproductibilité
 
-- **Commit Git** : `ace28bbecf9c9c768ed124ffe1dcd36aada5425a`
+- **Commit Git** : `4a2f06c4be18ce8285049560ee375e425c1451b5`
 - **Commande** :
 
 ```bash
@@ -39,8 +39,10 @@ python3 applications/collatz/collatz_k_scripts/collatz_generate_run_report.py --
 - m=14: |both|=593, |children(m=15)|=1186, |listed residual(m=15)|=1186
 - m=14: children(m=15) == residual(m=15) : True
 - m=14: both mod 4096 == B12 : True
-- m=15: |both|=1101, |children(m=16)|=2202
+- m=15: |both|=1101, |children(m=16)|=2202, |listed residual(m=16)|=2202
 - m=15: both mod 4096 == B12 : True
+- m=16: |both|=2202, |children(m=17)|=4404, |listed residual(m=17)|=4404
+- m=16: both mod 4096 == B12 : True
 
 ## Chemins d’artefacts (versionnés)