Recherches · Pièce-mère
La classification spectrale finie
le 3/5, entièrement classifié — et en cours de formalisation
Le « 3/5 » du triplet de Couret n’est ni un mystère ni un transport vers les premiers : c’est une identité finie, démontrable, et désormais classifiée de bout en bout. Tout triplet de G₃₀ relève exactement de l’un de deux spectres. Voici le résultat, ses preuves élémentaires, et l’état de sa certification machine.
Le cadre
Un laboratoire fini, entièrement observable
Le groupe des unités modulo 30 est fini, abélien, d’ordre 8, et se décompose canoniquement. Son dual compte huit caractères : le trivial, trois quadratiques (ordre 2, valeurs ±1) et quatre complexes d’ordre 4, en deux paires conjuguées. Cette répartition 3+4 gouverne toute la suite.
caractères : 1 trivial · 3 quadratiques (χ₃, χ₅, χ₁₅) · 4 complexes (2 paires conjuguées)
À un triplet T (trois classes) on associe le noyau centré kT = 1T − 3/8. Le centrage annule le caractère trivial ; sur tout caractère non trivial ψ, l’énergie est |Σx∈T ψ(x)|². La somme de ces énergies est constante, indépendante du triplet — une identité de Parseval.
15 unités d’énergie à répartir entre les 7 directions non triviales — une constante topologique.
Le moteur
Le lemme du défaut ponctuel
Soit G abélien fini d’ordre pair n, χ un caractère d’ordre 2, A = ker χ (de taille n/2), a₀ ∈ A, et T = A privé de a₀. Alors le noyau centré porte une énergie dominante sur χ, et exactement 1 sur chacune des autres directions.
n = 8 (G₃₀) → 6/10 = 3/5 · n = 16 → 7/9 · n = 480 → ≈ 0,992
Démonstration. Comme χ vaut +1 exactement sur A, on a l’identité ponctuelle 1A = (χ₀ + χ)/2. Pour ψ non trivial, ψ ≠ χ : Σx∈A ψ(x) = ½(ΣG ψ + ΣG χψ) = 0, les deux sommes s’annulant par orthogonalité (χψ est un caractère non trivial car χ⁻¹ = χ). Donc ΣT ψ = −ψ(a₀), d’énergie 1 (module 1) ; et ΣT χ = |A| − 1 = n/2 − 1. ∎
Le théorème
La dichotomie spectrale complète
Le lemme donne le sens direct ; la réciproque, spécifique à G₃₀, ferme la classification. Tout triplet est de l’un de deux types — et il n’y en a que deux.
Type Q — aligné
contenu dans une fibre quadratique privée d’un point · spectre (9,1,1,1,1,1,1) · ratio 3/5 · 24 triplets
Type C — presque aligné
aucune fibre quadratique · spectre (5,5,1,1,1,1,1) · ratio 1/3 au plus · 32 triplets
Réciproque (l’argument clé). Si une énergie vaut 9, alors |ΣT ψ| = 3 est la somme de trois nombres de module 1 : l’égalité dans l’inégalité triangulaire force les trois valeurs à la même phase, donc T est dans une fibre de ψ. Or un caractère d’ordre 4 a des fibres de taille 2 — il ne peut contenir trois éléments de même valeur ; ψ est donc quadratique. Dénombrement : 3 × 2 × C(4,3) = 24, distincts (deux fibres quadratiques se coupent en taille 2 < 3). Hors fibre, les 12 unités restantes se répartissent forcément en (5,5,1,1) sur les quatre caractères complexes.
La rigidité
Orbites & les deux triplets fixes
Sous les 8 automorphismes de G₃₀, les orbites d’éléments sont {1}, {19}, {11,29}, {7,13,17,23} — 19 étant l’unique carré non trivial, donc caractéristique. Les 24 triplets de Type Q se stratifient en 9 orbites ; un triplet fixe par tout automorphisme est une réunion d’orbites de taille 3, et il n’y en a qu’exactement deux :
tous deux des défauts ponctuels du demi-espace quadratique ker(χ₅) = {1,11,19,29}
Le triplet de Couret TC = {1,11,29} n’est donc ni unique par énergie (il est l’un des 24), ni l’unique triplet fixe (il y en a deux). Sa spécificité est documentaire — c’est celui qu’a transmis le corpus Couret — non une unicité mathématique.
Le versant premiers
Mesuré — et toujours en quarantaine
La dominance 3/5 est une concentration d’énergie dans les caractères ; la densité de comptage des premiers dans trois classes tend banalement vers 3/8 (Dirichlet). Deux objets distincts. La mesure correcte — la somme du caractère χ₅ sur les premiers — donne une équirépartition.
le petit reste relève du biais de Chebyshev classique
Bilan
Quatre statuts, une quarantaine
D·c
D·c
M
M
Q
La formalisation
Du témoin fini au moteur abstrait
La promotion vers D est organisée en quatre étages, sur deux axes (certification × portée). Aucun D n’est déclaré avant lake build -wfail, suppression des sorry, log d’audit et empreinte SHA-256.
G30Classification.lean
Témoin fini, 0 sorry, decide / native_decide. Chaque théorème re-dérivé en externe sous la convention du dépôt → vrai. Oracle de régression.
CharacterSubgroupSums.lean
Projecteur quadratique Pχ = ½(1+χ) = 1ker χ ; somme nulle sur le noyau. Cœur prouvé sans sorry ; restent l’orthogonalité globale et des pas mécaniques.
PointDefectLemma.lean
Le lemme général (sens direct) : Eχ = (n/2−1)², Eψ = 1. Structure complète, sorrys mécaniques.
…FromPointDefect.lean
La réciproque spécifique à G₃₀ (taille 3, fibres d’ordre 4 de taille 2).
Trois prises pour le premier build
- linarith sur ℂ ne compile pas (ℂ n’est pas ordonné) → linear_combination.
- orthogonalité globale : MulChar.IsNontrivial.sum_eq_zero vise les caractères d’anneau, pas G →* ℂˣ ; la preuve par translation (~4 lignes) est plus rapide.
- étiquette honnête : native_decide porte Lean.ofReduceBool → c’est [D-computational], pas un [D] nu.
La méthode à l’épreuve d’elle-même
Étude de cas InterIA
Cet épisode illustre comment la contrainte transforme le statut de la sortie d’une IA — non comme une preuve que la contrainte rendrait l’IA « cherchante ».
- 1 · PropositionUne IA propose une série de corollaires d’un même noyau. Chacun correct.
- 2 · ContradictionVérification indépendante, puis refus d’inscrire deux d’entre eux (de simples reformulations) — consolidation en une pièce-mère unique. La sobriété l’emporte sur la pente productiviste.
- 3 · VérificationLa couche Lean réelle change de convention de caractères ; la divergence est attrapée et réconciliée par re-calcul exhaustif. Rien n’est cru sur parole, y compris le travail antérieur de l’IA.
- 4 · FormalisationDeux axes de statut, sorrys explicites, fragilités de syntaxe signalées.
Garanties
Ce que cela ne prouve pas
GoldbachProofClaimed = false
HilbertPolyaClaimed = false
ScopeExpansionClaimed = false