- Dstructure de groupe fini, CRT, certifiée Lean
Ce que cela montre
la géométrie de groupe qui gouverne la classification des familles.
Ce que cela ne prouve pas
une structure spectrale globale.
Statut épistémique — composite (D · O)
Dstructure de groupe finie exacte : G₃₀ ≅ C₂ × C₄, certifiée par calcul (CRT + ordres des générateurs)
Otout passage de cette structure finie vers une portée spectrale globale (ζ, ξ) reste hors de ce résultat
Ce que cela montre
la géométrie de groupe qui gouverne la classification des huit familles modulo 30.
Ce que cela ne prouve pas
aucune structure spectrale globale, aucun lien aux zéros de ζ, aucune propriété des premiers réels au-delà du découpage fini.
Risque de mauvaise lecture — prendre la richesse de la structure finie (un groupe non cyclique, à deux générateurs) pour une signature « profonde » des nombres premiers. C’est une structure modulaire, exacte et close ; elle organise, elle ne révèle pas.
Régime · démonstratif
[D] Démontré
La structure exacte du groupe
Une fois retirés les multiples de 2, 3 et 5, les restes admissibles modulo 30 sont les huit entiers premiers avec 30 :
1 · 7 · 11 · 13 · 17 · 19 · 23 · 29
Munis de la multiplication modulo 30, ces huit restes forment un groupe abélien : c’est G₃₀ = (ℤ/30ℤ)×, le groupe des unités. Son ordre est φ(30) = φ(2)·φ(3)·φ(5) = 1·2·4 = 8.
Le théorème des restes chinois (CRT) décompose ce groupe selon la factorisation 30 = 2 × 3 × 5 :
(ℤ/30ℤ)× ≅ (ℤ/2ℤ)× × (ℤ/3ℤ)× × (ℤ/5ℤ)×
≅ C₁ × C₂ × C₄
≅ C₂ × C₄
≅ C₁ × C₂ × C₄
≅ C₂ × C₄
Le facteur (ℤ/2ℤ)× est trivial (un seul élément), (ℤ/3ℤ)× est cyclique d’ordre 2, et (ℤ/5ℤ)× est cyclique d’ordre 4. Le groupe n’est donc pas cyclique : C₂ × C₄ n’est pas isomorphe à C₈ (il n’a pas d’élément d’ordre 8). C’est un point structurel important — la « forme » du socle est celle d’un produit, pas d’un cycle simple.
Concrètement, on peut prendre pour générateurs :
11 — ordre 2 (11² = 121 ≡ 1 mod 30)
17 — ordre 4 (17² = 289 ≡ 19, 17⁴ ≡ 1 mod 30)
⟹ G₃₀ = ⟨11⟩ × ⟨17⟩ ≅ C₂ × C₄
17 — ordre 4 (17² = 289 ≡ 19, 17⁴ ≡ 1 mod 30)
⟹ G₃₀ = ⟨11⟩ × ⟨17⟩ ≅ C₂ × C₄
La structure est entièrement explicite, finie, et vérifiable case par case. C’est le seuil démontré sur lequel repose toute la classification ultérieure des familles et de leurs combinaisons.
Formalisé dans G30Classification.lean · Lean 4 · Mathlib v4.29.1 · couche Frozen, sans
sorry · certification computationnelle (native_decide).Ce que ce bloc montre
- un groupe abélien fini d’ordre 8, explicite
- sa structure exacte C₂ × C₄ (non cyclique)
- des générateurs nommés (11 d’ordre 2, 17 d’ordre 4)
Ce que ce bloc ne prouve pas
- aucune propriété asymptotique des premiers
- aucune structure spectrale ou analytique
- aucun lien à ζ, ξ ou aux zéros
[O] Ouvert / retenue
Le passage vers le global n’est pas dans ce résultat
G₃₀ est un objet fini et clos. Sa structure de groupe ne dit, par elle-même, rien des nombres premiers en tant que suite infinie : elle décrit le cadre de résidus dans lequel ils se répartissent, pas leur distribution. Le fait que ce groupe soit C₂ × C₄ plutôt que C₈ est une propriété du module 30, pas un théorème sur les premiers.
Tout énoncé qui voudrait faire « monter » cette structure vers une portée globale — une signature spectrale, un lien aux zéros de la fonction zêta — exige un pont explicite, qui n’existe pas ici. Ce bloc est le seuil de retenue de la fiche : il marque où s’arrête le démontré.
Ce que ce bloc montre
- la limite exacte de portée de la structure finie
- la distinction cadre de résidus / distribution
Ce que ce bloc ne prouve pas
- aucune percée vers ζ ou RH
- aucune nécessité « profonde » de la forme C₂ × C₄
- aucun transport vers les premiers réels