Navigation
Atlas des théorèmes
41 théorèmes du crible au Modèle Standard, chacun cliquable vers sa fiche.
Réplique interactive de la figure pleine-page de la monographie : axiomes U1–U4 → T1 → T3 → s = ½ → T2 → L0 → T6 → GFT → G1/G3 → T4 → Mertens → T5 (μ* = 15) → T0 → W7-1 → BA5 → Lemmes E/F/G → α_EM, sin²θ_W, α_s, G, m_e → 43 observables. Chaque boîte est colorée par classe épistémique (THM bleu, ID vert, DER orange, BRIDGE violet, VAL gris, COND hachuré, CONJ crosshatché) et porte sa marque de formalisation Lean.
Couverture : 39/41 cartes pointent vers une fiche dédiée du site ; les autres renvoient à la monographie via le lien de bas de page.
Passez la souris sur une carte pour voir ses voisins immédiats : ce dont elle dépend directement (juste avant) et ce qu'elle permet directement (juste après). Sur mobile : tapez une carte pour basculer la mise en évidence.
Colonne 1
I. Cœur arithmétique
primitives génératives {1, +, ×, ≠ 0}
Transitions interdites : $T_3$ a $T_{11}=T_{22}=0$
$T_3$ antidiagonal, forme stochastique unique
mesure stationnaire de $T_3$ (le théorème)
Conservation $s^2 = 1/4$
Verrou max-entropie sur les classes résiduelles
Unicité d’Ératosthène (corps + axiomes + Čencov)
$\log_2 m = D_{KL} + H$
$D_{KL}$ divergence unique (Shore–Johnson)
métrique de Fisher unique (Čencov 1982, étendu)
$\sin^2\theta_p = \delta_p(2-\delta_p)$
Colonne 2
II. Convergence et point fixe
Convergence spectrale : $\alpha_k \to 1/2$
Compacité : $\|M(x) - \log\log x\| < \infty$
critère $\gamma_p > s \Leftrightarrow p \in \{3,5,7\}$
Point fixe maître : $\mu^* = \sum_{\text{actifs}} p = 15$
$N_c = N_{\text{gen}} = N_{\text{spatial}} = 3$
Suite des espacements unique (lifting U1–U4)
Identité de spirale : $\sigma^2 = \pi(k+1)$
chaîne $s \to \alpha_{\text{bare}}$
borne sous-dominante (sous axiome T5Like)
théorème premier (spectre actif ⇒ $N_{\text{gen}}$)
Colonne 3
III. Pont
Produit de Pontryagin : $\widehat{\mathbb{Z}/P} = \prod \widehat{\mathbb{Z}/p}$
identification physique : $\alpha_{\text{crible}} = \alpha_{\text{EM}}$
Reconstruction OS (positivité)
Reconstruction métrique (Fisher → Riemann)
limite inductive (Wightman W1–W4)
théorème (4 unicités T6 + G1 + G3 + T5)
$\mathbb{Z}/P \cong \bigoplus \mathbb{Z}/p$ — invariance de jauge causale
$C^*$-dynamique : $Z(\beta) \to \zeta(\beta)$, $\beta_c = 1$
borne d’erreur (Lee–Yang tail)
DAG de dépendances
Colonne 4
IV. Reconstruction et sortie
axiomes vN1–vN6 ; règle de Born depuis $|w_p|^2$
Bianchi I + signature lorentzienne ; Friedmann depuis Fisher
GFT = premier principe ; $Z_F = Z_R = Z_P$
$\alpha_{\text{bare}} = \prod \sin^2\theta_p$ + habillage → 0,004 ppb
$\sin^2\theta_W = \gamma_7^2 / \sum \gamma_p^2$, 0,01–0,05 %
$G/\alpha = 2\pi$ (Friedmann) ; $m_e = s$ (calibration SCU)
moyenne 0,30 % (0 paramètre ajusté)
prédictions P1–P28 (falsifiables)
géométrique ($F_{\text{inactive}}$) ; programme DM/DE
via spirale W7 — non réduite
Légende
Classes épistémiques
- [THM] prouvé inconditionnel
- [ID] identité algébrique
- [DER] dérivation
- [BRIDGE] identification physique
- [VAL] validation empirique
- [COND] conditionnel (hachuré)
- [CONJ] conjectural (crosshatché)
- axiome primitives U1–U4
Statut Lean
- ✓L kernel-vérifié, 0 sorry
- ∼L partiel (sorrys documentés)
- ⋆L externe (Mathlib)
- ◦L non formalisé
Aller plus loin
Cette carte est la traduction web d’une figure pleine page de la monographie. Pour voir les flèches de dépendance complètes (intra-colonne, inter-colonnes, court-circuits du résultat phare α_EM) ainsi que le contexte de chaque résultat, consultez la monographie. Pour le détail des modules formalisés, voir la page Formalisation Lean ; pour le statut épistémique fin, voir Statuts des résultats et Audit.