Public : Licence — accrétion de la troisième étape de la série Geometry, le programme gradué de la preuve automatique en géométrie. C’est l’accrétion de recherche de Geometry-03 — La méthode de Wu : le chemin principal reste lisible sans ouvrir cette lettre.
Ce que ce notebook suppose. Geometry-03 — La méthode de Wu : pseudo-division prem, ensemble caractéristique (basic-set de Chou), test de Wu, conditions de non-dégénérescence lues sur les initiales. Et Geometry-01 pour la vérification numérique sur figures aléatoires ; la série SMT/Z3 pour le contexte solveur.
Le problème posé. Sur le théorème du papillon (T2), le test de Wu du 03 rend un reste non nul : il ne prouve rien. Le 03 explique alors, en prose, que la variété est réductible et que la décomposition de Ritt est « la brique manquante ». Ce notebook prend cette explication au sérieux et la met à l’épreuve — y compris là où elle se révèle incomplète.
Ce que vous emportez. Trois résultats, tous mesurés ici :
| § | Contenu | Livrable |
|---|---|---|
| 1 | Le papillon : Wu dit « non », la figure dit « oui » | encodage H2, g2, sanity numérique |
| 2 | La chasse aux dénominateurs | identité g2 = x_X·(b2−c2) + y_Y·(d2−a2) vérifiée |
| 3 | La décomposition de Ritt : mécanisme, puis mesure | ritt_split_one ; factorisation des initiales de la chaîne du papillon |
| 4 | Les composantes, une fois scindées | témoin rationnel : X à l’infini, g2 = 24/5 |
| 5 | Ce qui survit | contrôle numérique sur 400 figures |
| 6 | Témoin négatif | un énoncé faux rejeté |
| 7 | Exercices | 3 énoncés à compléter |
Les briques algorithmiques — prem, la chaîne, le test de Wu — sont reprises du 03 à l’identique (même code, mêmes résultats) ; ritt_split_one est la seule brique nouvelle.
# Socle : polynomes, pseudo-division, chaine caracteristique (repris du 03, a l'identique).
import sys
import time
import sympy
from sympy import (symbols, Poly, prem, factor_list, expand, simplify, together,
solve, Rational, Symbol)
t_start = time.time()
print("sympy", sympy.__version__, "| Python", sys.version.split()[0])sympy 1.14.0 | Python 3.13.15T2 (papillon). \(M\), \(P\), \(Q\) sont alignés (\(P \neq Q\)), et \(M\) est le milieu de \([PQ]\). Deux droites passant par \(M\) coupent le cercle de diamètre \([PQ]\) en \(A, B\) pour l’une et \(C, D\) pour l’autre. Les droites \((AD)\) et \((CB)\) coupent la droite \((PQ)\) en \(X\) et \(Y\). Alors \(M\) est le milieu de \([XY]\).
Encodage (repris du 03, §10, à l’identique). Repère : \(M = (0,0)\), \(P = (-1,0)\), \(Q = (1,0)\) — la droite \((PQ)\) est donc l’axe des abscisses, et \(M\) en est l’origine. Le cercle passe par \(P\) et \(Q\) : centre \((0, c)\), rayon\(^2 = 1 + c^2\) (le cas du diamètre \([PQ]\) est la valeur particulière \(c = 0\)). Les inconnues sont les coordonnées de \(A, B, C, D\) ; \(c\) est un paramètre.
| Hypothèse | Polynôme |
|---|---|
| \(A\) sur le cercle | \(h_a : a_1^2 + a_2^2 - 2ca_2 - 1\) |
| \(B\) sur le cercle | \(h_b\) (idem en \(b\)) |
| \(A, M, B\) alignés | \(h_{ab} : a_1 b_2 - a_2 b_1\) |
| \(C\), \(D\) sur le cercle | \(h_c\), \(h_d\) |
| \(C, M, D\) alignés | \(h_{cd} : c_1 d_2 - c_2 d_1\) |
Les alignements s’écrivent comme des déterminants nuls parce que \(M\) est à l’origine : c’est le seul intérêt du choix de repère, et il évite deux constantes dans chaque hypothèse.
# Fil rouge de l'accretion : le papillon (T2), exactement l'encodage du 03 §10.
a1, a2, b1, b2, c1, c2, d1, d2, cc = symbols("a1 a2 b1 b2 c1 c2 d1 d2 c")
V2 = [cc, a1, a2, b1, b2, c1, c2, d1, d2]
ha = a1**2 + a2**2 - 2*cc*a2 - 1 # A sur le cercle (centre (0,c), rayon^2 = 1+c^2)
hb = b1**2 + b2**2 - 2*cc*b2 - 1 # B sur le cercle
hab = a1*b2 - a2*b1 # A, M=(0,0), B alignes
hc = c1**2 + c2**2 - 2*cc*c2 - 1 # C sur le cercle
hd = d1**2 + d2**2 - 2*cc*d2 - 1 # D sur le cercle
hcd = c1*d2 - c2*d1 # C, M, D alignes
H2 = [ha, hb, hab, hc, hd, hcd]
# Conclusion telle que le 03 l'encode : M milieu de [XY] <=> x_X + y_Y = 0,
# ou x_X et y_Y sont les ABSCISSES des intersections de (AD) et (CB) avec l'axe (PQ).
g2 = (a1*d2 - a2*d1)*(b2 - c2) + (c1*b2 - c2*b1)*(d2 - a2)
print(f"T2 : {len(H2)} hypotheses, {len(V2)} variables")
print("g2 (degre total) :", Poly(g2, *V2).total_degree())T2 : 6 hypotheses, 9 variables
g2 (degre total) : 3# Sanity numerique AVANT tout symbolique : c = 2, corde AB de pente 1, corde CD de pente 2.
# (Regle d'hygiene du 03 : la verification numerique attrape les erreurs d'encodage
# qu'aucun moteur symbolique ne signalera -- c'est elle qui a attrape le rapport dirige de Ceva.)
_p = Symbol("p")
rAB = solve(2*_p**2 - 4*_p - 1, _p) # y = x : (1+m^2)x^2 - 2cm x - 1 = 0, c = 2, m = 1
rCD = solve(5*_p**2 - 8*_p - 1, _p) # y = 2x : idem avec m = 2
A = (rAB[0], rAB[0]); B = (rAB[1], rAB[1])
Cc = (rCD[0], 2*rCD[0]); D = (rCD[1], 2*rCD[1])
def abscisse_sur_axe(P1, P2):
'''Abscisse de l'intersection de (P1 P2) avec l'axe (PQ) : y = 0.'''
(x1, y1), (x2, y2) = P1, P2
return simplify(x1 - y1*(x2 - x1)/(y2 - y1))
xX = abscisse_sur_axe(A, D); yY = abscisse_sur_axe(Cc, B)
print(f"x_X = {float(xX):+.6f} y_Y = {float(yY):+.6f} x_X + y_Y = {float(xX + yY):+.2e}")
print("SANITY :", "OK — M=(0,0) est bien le milieu de [XY]" if simplify(xX + yY) == 0 else "ECHEC")x_X = -0.105468 y_Y = +0.105468 x_X + y_Y = +1.48e-126
SANITY : OK — M=(0,0) est bien le milieu de [XY]La figure est bonne : sur cet exemple, le milieu de \([XY]\) est \(M\). Le théorème est un vrai théorème, et l’échec du test de Wu ne dit donc pas qu’il est faux.
def main_var(f, varlist):
'''Variable principale : la plus grande variable (ordre d'elimination) qui apparait.'''
for v in reversed(varlist):
if Poly(f, v).degree() > 0:
return v
return None
def rank_p(p_, varlist):
'''(indice de la variable principale, degre en celle-ci) -- ordre lexicographique.'''
mv = main_var(p_, varlist)
return (varlist.index(mv), Poly(p_, mv).degree()) if mv else (-1, 0)
def prem_s(f, gg, v):
'''Pseudo-reste : prem(Poly(f, v), Poly(gg, v)) -- sans fractions.'''
return prem(Poly(f, v), Poly(gg, v))
def basic_set(H, varlist):
'''Selection gloutonne (Chou) : un polynome par variable principale, par rang croissant.'''
B, used = [], set()
for p_ in sorted(H, key=lambda q: rank_p(q, varlist)):
mv = main_var(p_, varlist)
if mv is None:
return [p_]
if mv not in used:
B.append(p_)
used.add(mv)
return Bdef char_set_basic(H, varlist, max_iter=80):
'''Iteration de Chou : basic-set + pseudo-reduction des non-retenus jusqu'a stabilite.'''
H = [expand(h) for h in H]
for it in range(max_iter):
B = basic_set(H, varlist)
R = []
for h in H:
if h in B:
continue
r = h
for p_ in reversed(B):
mv = main_var(p_, varlist)
r = prem_s(r, p_, mv) if mv else r
if r != 0:
R.append(r)
if not R:
return B, it
H = sorted(set(H).union(R), key=lambda q: (rank_p(q, varlist), str(q)))
raise RuntimeError("pas de convergence de l'ensemble caracteristique")
def wu_prem(g, B, varlist):
'''Pseudo-reste successif de g a travers la chaine B, du sommet vers la base.'''
R = expand(g)
for p_ in reversed(B):
mv = main_var(p_, varlist)
R = prem_s(R, p_, mv) if mv else R
return R
t0 = time.time()
B2, it2 = char_set_basic(H2, V2)
t_cs = time.time() - t0
t0 = time.time()
R2 = wu_prem(g2, B2, V2)
t_test = time.time() - t0
def _ex(f):
'''Maillon de chaine lisible : prem renvoie un Poly, on l'affiche en expression.'''
return expand(f.as_expr()) if isinstance(f, Poly) else expand(f)
print(f"CS(T2) : {len(B2)} polynomes, converge en {it2} iteration(s) [{t_cs:.2f}s]")
for b in B2:
print(f" mv={str(main_var(b, V2)):3s} {str(_ex(b))[:70]}")
print()
print(f"prem(g2, CS) = {R2 if R2 == 0 else 'polynome NON NUL'} [{t_test:.2f}s]")
print("VERDICT :", "PROUVE" if R2 == 0 else "NON CONCLUANT — ce critere-ci n'a rien prouve")CS(T2) : 6 polynomes, converge en 1 iteration(s) [0.09s]
mv=a2 a1**2 + a2**2 - 2*a2*c - 1
mv=b1 -a1**2 - 2*a1*a2*b1*c + 2*a2*b1**2*c + b1**2
mv=b2 a1*b2 - a2*b1
mv=c2 -2*c*c2 + c1**2 + c2**2 - 1
mv=d1 -2*c*c1*c2*d1 + 2*c*c2*d1**2 - c1**2 + d1**2
mv=d2 c1*d2 - c2*d1
prem(g2, CS) = polynome NON NUL [0.03s]
VERDICT : NON CONCLUANT — ce critere-ci n'a rien prouve\(g_2\) n’est pas l’énoncé géométrique. C’est l’énoncé après multiplication par \((d_2-a_2)(b_2-c_2)\), et cette multiplication n’est une équivalence que là où ce produit ne s’annule pas. Regardons d’où il vient.
Un point de \((AD)\) s’écrit \(A + t\,(D - A)\) ; son intersection avec l’axe \((PQ)\) (\(y = 0\)) impose \(a_2 + t\,(d_2-a_2) = 0\), soit \(t = -a_2/(d_2-a_2)\), et l’abscisse vaut
\[x_X \;=\; a_1 - a_2\,\frac{d_1-a_1}{d_2-a_2} \;=\; \frac{a_1 d_2 - a_2 d_1}{d_2 - a_2}\]
De même \(y_Y = \dfrac{c_1 b_2 - c_2 b_1}{b_2 - c_2}\). La conclusion « \(M = (0,0)\) est le milieu de \([XY]\) » s’écrit donc \(x_X + y_Y = 0\) — une équation rationnelle, pas polynomiale. Multiplier les deux membres par le produit des deux dénominateurs donne \(g_2\).
Vérifions l’identité plutôt que de la croire :
# Les abscisses de X et Y, puis l'identite qui les relie a g2 (le 03 l'affirme ; on la mesure).
xX = (a1*d2 - a2*d1)/(d2 - a2) # X = (AD) inter (PQ) [PQ : axe y = 0]
yY = (c1*b2 - c2*b1)/(b2 - c2) # Y = (CB) inter (PQ)
den = (d2 - a2)*(b2 - c2)
reste = expand(together(xX + yY)*den - g2)
print("denominateur commun :", den)
print("facteurs :", [str(f) for f, m in factor_list(den)[1]])
print("(x_X + y_Y)*den - g2 =", reste)
assert reste == 0, "l'identite g2 <-> enonce geometrique est FAUSSE"
print("VERIFIE : g2 est exactement (x_X + y_Y) mis au meme denominateur.")denominateur commun : (-a2 + d2)*(b2 - c2)
facteurs : ['b2 - c2', 'a2 - d2']
(x_X + y_Y)*den - g2 = 0
VERIFIE : g2 est exactement (x_X + y_Y) mis au meme denominateur.L’identité est exacte. Elle livre la carte du problème :
| Facteur nul | Ce qu’il signifie | Conséquence |
|---|---|---|
| \(d_2 - a_2 = 0\) | \(a_2 = d_2\) : \((AD)\) est horizontale, donc parallèle à \((PQ)\) | le point \(X\) est à l’infini |
| \(b_2 - c_2 = 0\) | \(b_2 = c_2\) : \((CB)\) est horizontale, donc parallèle à \((PQ)\) | le point \(Y\) est à l’infini |
C’est le point que le 03 laisse en prose et que ce notebook mesure : sur ces bords, l’énoncé « \(M\) est le milieu de \([XY]\) » ne parle plus de rien — l’un de ses objets n’existe pas. Un test qui travaille sur \(g_2\) sans tenir compte de ce fait lit une valeur non nulle là où il n’y a plus d’énoncé du tout.
Le test de Wu divise par les initiales de la chaîne — les coefficients dominants, en la variable principale, de chaque polynôme. Une telle division n’est licite que là où l’initiale ne s’annule pas. Quand une initiale se factorise, \(I = I' \cdot I''\), le lieu où elle s’annule se coupe en deux morceaux, et le raisonnement peut repartir séparément sur chacun.
La décomposition de Ritt (Ritt 1950 ; forme algorithmique Ritt–Wu) exploite cela : elle coupe récursivement sur chaque facteur d’initiale, en adjoignant le facteur au système pour la branche correspondante, jusqu’à ce que toutes les initiales soient irréductibles. La variété \(V(H)\) sort alors comme une union finie de composantes, chacune avec sa propre chaîne — et le test de Wu se fait composante par composante au lieu d’un verdict global.
Un système conçu pour déclencher la scission. Avec \(H_s = [\,(x^2-1)\,y - 2,\;\; xz - y\,]\), la variable principale du premier polynôme est \(y\) et son initiale est \(x^2 - 1 = (x-1)(x+1)\) : deux facteurs, donc deux branches, plus le complément.
x, y, z = symbols("x y z")
Hs, Vs = [(x**2 - 1)*y - 2, x*z - y], [x, y, z] # initiale (x-1)(x+1) en y
def ritt_split_one(H, varlist):
'''Premiere scission de Ritt : sur la PREMIERE initiale qui se factorise en
facteurs non triviaux. Renvoie (polynome, initiale, facteurs, branches).
Borne assumee : une seule scission. L'algorithme complet (Ritt-Ritt) recurse sur
CHAQUE branche -- y compris la branche complementaire -- jusqu'a irreductibilite.
Une etape suffit a montrer la mecanique ; terminaison et complexite ne sont pas
demontrees ici.
'''
B, _ = char_set_basic(H, varlist)
for f in B:
v = main_var(f, varlist)
if v is None:
continue
I = Poly(f, v).LC()
facs = [fac for fac, mult in factor_list(I)[1]
if Poly(fac, *varlist).total_degree() > 0]
if len(facs) > 1:
branches = []
for fac in facs: # branches "ce facteur s'annule"
Bi, _ = char_set_basic(list(H) + [fac], varlist)
branches.append((f"{fac} = 0", Bi, ()))
branches.append(("aucun facteur nul", B, tuple(facs)))
return f, I, facs, branches
return None
f_split, I_split, facs_split, branches = ritt_split_one(Hs, Vs)
print(f"chaine de Hs : {[str(b) for b in char_set_basic(Hs, Vs)[0]]}")
print(f"premiere initiale factorisable : {I_split} (porte par {f_split})")
print(f"facteurs non triviaux : {facs_split} -> {len(branches)} branches\n")
for k, (lab, Bk, nz) in enumerate(branches, 1):
print(f"branche {k} — {lab}")
print(f" chaine ({len(Bk)} poly) : {[str(b)[:48] for b in Bk]}")
if nz:
print(f" non-annulations portees : {[str(t) for t in nz]}")
else:
# Cette branche est-elle habitee ? Annuler un facteur de l'initiale rend la
# division illicite ; il faut verifier que le point existe vraiment.
fac = facs_split[k-1]; vf = main_var(fac, Vs)
for rt in solve(fac, vf):
val = simplify(f_split.subs(vf, rt))
print(f" au point {vf} = {rt} : le polynome scinde vaut {val}"
f" -> branche {'VIDE (incompatible)' if val != 0 else 'non vide'}")chaine de Hs : ['x**2*y - y - 2', 'x*z - y']
premiere initiale factorisable : x**2 - 1 (porte par x**2*y - y - 2)
facteurs non triviaux : [x - 1, x + 1] -> 3 branches
branche 1 — x - 1 = 0
chaine (3 poly) : ['x - 1', 'x**2*y - y - 2', 'x*z - y']
au point x = 1 : le polynome scinde vaut -2 -> branche VIDE (incompatible)
branche 2 — x + 1 = 0
chaine (3 poly) : ['x + 1', 'x**2*y - y - 2', 'x*z - y']
au point x = -1 : le polynome scinde vaut -2 -> branche VIDE (incompatible)
branche 3 — aucun facteur nul
chaine (2 poly) : ['x**2*y - y - 2', 'x*z - y']
non-annulations portees : ['x - 1', 'x + 1']Trois branches là où le test global n’en voyait qu’une. La troisième — « aucun facteur nul » — est le lieu non dégénéré de cette scission. Et les deux premières sont vides : en \(x = 1\) comme en \(x = -1\), le polynôme scindé vaut \(-2\), jamais \(0\). La cellule le mesure au lieu de le supposer.
Ce n’est pas un détail : c’est la raison pour laquelle une décomposition ne se contente pas de compter les branches. Une composante vide ne porte aucun point, donc rien à prouver — mais un test qui l’ignorerait raisonnerait sur du vide. C’est exactement le partage des rôles de Chou (1988) : l’algorithme sépare, l’analyse classe.
Le 03 conclut son §11 en annonçant que la chaîne du papillon est réductible et que la décomposition est « la brique manquante ». C’est une affirmation vérifiable — vérifions-la : factorisons les initiales de la chaîne \(B_2\) effectivement construite au §1.
# Les initiales de la chaine du papillon, et leur factorisation.
print("Initiales de la chaine CS(T2) :\n")
reductibles = []
for f in B2:
v = main_var(f, V2)
I = Poly(f, v).LC()
facs = [(str(fac), mult) for fac, mult in factor_list(I)[1]
if Poly(fac, *V2).total_degree() > 0]
if len(facs) > 1:
reductibles.append((str(v), str(I), facs))
print(f" mv={str(v):3s} initiale = {str(I):28s} facteurs non triviaux : {facs}")
print()
print(f"initiales portant DEUX facteurs non triviaux (donc scindables) : {len(reductibles)}")
print()
if not reductibles:
print("MESURE : aucune initiale n'est reductible -> la scission de Ritt NE SE")
print(" DECLENCHE PAS sur cette chaine. L'explication en prose du 03 ne")
print(" suffit donc pas : ce n'est pas l'initiale de la chaine qui rend")
print(" le test non concluant ici -- l'obstruction est ailleurs (§4).")
else:
print("MESURE : au moins une initiale est reductible -> scission disponible :", reductibles)Initiales de la chaine CS(T2) :
mv=a2 initiale = 1 facteurs non triviaux : []
mv=b1 initiale = 2*a2*c + 1 facteurs non triviaux : [('2*a2*c + 1', 1)]
mv=b2 initiale = a1 facteurs non triviaux : [('a1', 1)]
mv=c2 initiale = 1 facteurs non triviaux : []
mv=d1 initiale = 2*c*c2 + 1 facteurs non triviaux : [('2*c*c2 + 1', 1)]
mv=d2 initiale = c1 facteurs non triviaux : [('c1', 1)]
initiales portant DEUX facteurs non triviaux (donc scindables) : 0
MESURE : aucune initiale n'est reductible -> la scission de Ritt NE SE
DECLENCHE PAS sur cette chaine. L'explication en prose du 03 ne
suffit donc pas : ce n'est pas l'initiale de la chaine qui rend
le test non concluant ici -- l'obstruction est ailleurs (§4).Le résultat est net, et il corrige l’intuition du 03 : sur cette chaîne, les initiales valent \(1\) (aucune condition !), \(a_1\), \(2a_2c+1\), \(2cc_2+1\), \(c_1\) — toutes irréductibles. La scission de Ritt, telle qu’elle s’applique aux initiales de la chaîne, ne se déclenche pas ici.
Où scinder, alors ? La réponse est dans le §2, et elle est structurelle : la décomposition ne porte pas seulement sur les initiales de la chaîne — elle porte sur tout polynôme dont on adjoint les facteurs au système. Or ici l’obstruction ne vient pas de la chaîne : elle vient du dénominateur de la conclusion, \((d_2-a_2)(b_2-c_2)\), qui n’appartient pas à \(H_2\). La méthode complète adjoint ces conditions au système et scinde sur leurs facteurs — ce qui revient à séparer les quatre strates du §4. C’est le même geste que ritt_split_one, appliqué aux bons polynômes.
Scinder sur les deux facteurs du dénominateur donne quatre strates. Voici ce que vaut chacune — la dernière ligne est mesurée juste après.
| Strate | \((d_2-a_2)\) | \((b_2-c_2)\) | \(g_2\) | Ce qui se passe |
|---|---|---|---|---|
| non dégénérée | \(\neq 0\) | \(\neq 0\) | \(= 0\) | \(X\) et \(Y\) existent, et \(M\) est bien leur milieu |
| bord \((AD) \parallel (PQ)\) | \(=0\) | \(\neq 0\) | \(\neq 0\) possible | \(X\) est à l’infini : l’énoncé est muet |
| bord \((CB) \parallel (PQ)\) | \(\neq 0\) | \(=0\) | \(\neq 0\) possible | \(Y\) est à l’infini : l’énoncé est muet |
| doublement dégénéré | \(=0\) | \(=0\) | \(\equiv 0\) | voir ci-dessous — ce zéro ne prouve rien |
Le témoin explicite. Un point rationnel du premier bord, trouvé en résolvant \(H_2\) sous contrainte \(d_2 = a_2\) : le cercle \(c = 2\), la corde \(AD\) horizontale en \(y = 1\), et \(C = D = (2,1)\).
# Temoin rationnel sur le bord d2 = a2 : la corde AD est horizontale.
degen = {cc: 2, a1: -2, a2: 1, d1: 2, d2: 1, c1: 2, c2: 1, b1: Rational(2, 5), b2: Rational(-1, 5)}
print("Hypotheses H2 au point temoin :")
for nm, h in [("ha", ha), ("hb", hb), ("hab", hab), ("hc", hc), ("hd", hd), ("hcd", hcd)]:
print(f" {nm} = {h.subs(degen)}")
print()
print("d2 - a2 =", (d2 - a2).subs(degen), " -> (AD) est horizontale, parallele a (PQ)")
print("b2 - c2 =", (b2 - c2).subs(degen))
print("g2 =", g2.subs(degen), "\n")
# Geometrie du meme point, calculee directement : ou sont X et Y ?
print("Lecture geometrique du meme point :")
print(" (AD) : y = 1 (A = (-2,1), D = (2,1)) -> ne coupe JAMAIS l'axe (PQ) : y = 0")
yY_val = Rational(2, 3)
print(f" (CB) : C = (2,1), B = (2/5,-1/5) -> coupe l'axe en Y = ({yY_val}, 0) [fini]")
print()
print("CONCLUSION : X n'existe pas (a l'infini), Y est fini. L'ENONCE EST MUET --")
print(" il n'y a pas de milieu de [XY], donc rien a refuter.")Hypotheses H2 au point temoin :
ha = 0
hb = 0
hab = 0
hc = 0
hd = 0
hcd = 0
d2 - a2 = 0 -> (AD) est horizontale, parallele a (PQ)
b2 - c2 = -6/5
g2 = 24/5
Lecture geometrique du meme point :
(AD) : y = 1 (A = (-2,1), D = (2,1)) -> ne coupe JAMAIS l'axe (PQ) : y = 0
(CB) : C = (2,1), B = (2/5,-1/5) -> coupe l'axe en Y = (2/3, 0) [fini]
CONCLUSION : X n'existe pas (a l'infini), Y est fini. L'ENONCE EST MUET --
il n'y a pas de milieu de [XY], donc rien a refuter.# Strate doublement degeneree : les deux facteurs s'annulent -> g2 s'annule IDENTIQUEMENT.
g2_double = expand(g2.subs({d2: a2}).subs({b2: c2}))
print("g2 restreint a (d2 = a2) ET (b2 = c2) :", g2_double)
print()
print("Pourquoi : chaque terme de g2 porte l'un des deux facteurs --")
print(" terme 1 : (a1*d2 - a2*d1) * (b2 - c2) -> porte (b2 - c2)")
print(" terme 2 : (c1*b2 - c2*b1) * (d2 - a2) -> porte (d2 - a2)")
print("Sur la strate doublement degeneree, les DEUX termes meurent : aucun rendement.")
print("Ce zero est donc TRIVIAL (structurel) -- ce n'est PAS un certificat de theoreme :")
print("il dit seulement que le test ne peut plus rien y contredire.")g2 restreint a (d2 = a2) ET (b2 = c2) : 0
Pourquoi : chaque terme de g2 porte l'un des deux facteurs --
terme 1 : (a1*d2 - a2*d1) * (b2 - c2) -> porte (b2 - c2)
terme 2 : (c1*b2 - c2*b1) * (d2 - a2) -> porte (d2 - a2)
Sur la strate doublement degeneree, les DEUX termes meurent : aucun rendement.
Ce zero est donc TRIVIAL (structurel) -- ce n'est PAS un certificat de theoreme :
il dit seulement que le test ne peut plus rien y contredire.Le bilan du §4 n’est pas un échec de la méthode — c’est une restriction implicite de l’énoncé. Reste à établir la moitié positive : là où les deux dénominateurs ne s’annulent pas, la conclusion tient. C’est un énoncé de zéro de polynôme sur un ouvert — exactement le cadre où Geometry-01 a introduit la vérification de Schwartz–Zippel.
400 figures tirées au hasard sur le lieu non dégénéré ; on mesure \(|x_X + y_Y|\), qui vaut \(|g_2 / \text{den}|\) :
import math, random
random.seed(7)
def corde(m, cval):
'''Les deux intersections de y = m*x avec le cercle x^2 + y^2 - 2 c y - 1 = 0.'''
disc = 4*cval*cval*m*m + 4*(1 + m*m)
s = math.sqrt(disc)
x1 = (2*cval*m - s)/(2*(1 + m*m)); x2 = (2*cval*m + s)/(2*(1 + m*m))
return (x1, m*x1), (x2, m*x2)
def abscisse(P1, P2):
'''Abscisse de l'intersection de (P1 P2) avec y = 0.'''
(px, py), (qx, qy) = P1, P2
return px - py*(qx - px)/(qy - py)
# Le critere est RELATIF : x_X et y_Y peuvent etre grands (denominateurs petits) et
# une tolerance absolue jugerait alors la taille des nombres, pas la validite du theoreme.
ok = quasi_muettes = 0
rels, abss = [], []
for _ in range(400):
cval = random.uniform(0.5, 4.0)
m1 = random.uniform(-4, 4); m2 = random.uniform(-4, 4)
if abs(m1 - m2) < 1e-9:
continue
A_, B_ = corde(m1, cval); C_, D_ = corde(m2, cval)
d2v, a2v = D_[1], A_[1]; b2v, c2v = B_[1], C_[1]
if abs(d2v - a2v) < 1e-6 or abs(b2v - c2v) < 1e-6: # X ou Y quasi a l'infini
quasi_muettes += 1
continue
xXv, yYv = abscisse(A_, D_), abscisse(C_, B_)
s = abs(xXv + yYv)
abss.append(s); rels.append(s/(abs(xXv) + abs(yYv)))
ok += 1
rels.sort()
med = rels[len(rels)//2]; p99 = rels[int(0.99*len(rels))]
SEUIL = 1e-9 # tolerance declaree, sur l'ecart RELATIF
au_dessus = sum(1 for r in rels if r > SEUIL)
print(f"figures evaluees sur le lieu non degenere : {ok}")
print(f"figures ecartees (X ou Y quasi a l'infini): {quasi_muettes}")
print()
print(f"ecart ABSOLU |x_X + y_Y| : median {sorted(abss)[len(abss)//2]:.2e} max {max(abss):.2e}")
print(f"ecart RELATIF : median {med:.2e} p99 {p99:.2e} max {max(rels):.2e}")
print(f"figures au-dessus du seuil {SEUIL:.0e} : {au_dessus}")
print()
print("VERDICT :", (f"aucune figure au-dessus du seuil {SEUIL:.0e} -- la conclusion TIENT"
if au_dessus == 0 else "ECHEC : une figure non degeneree refute le theoreme"))
print()
print("Lecture : la mediane est au bruit machine (1e-16) ; la queue de distribution")
print(" monte a 1e-12 sur les figures a PETIT denominateur, ou x_X et y_Y")
print(" sont grands et ou l'annulation x_X + y_Y amplifie l'erreur d'arrondi")
print(" des intersections. C'est un effet de CONDITIONNEMENT, pas de theorie --")
print(" d'ou une tolerance declaree, et un ecart relatif comme critere.")figures evaluees sur le lieu non degenere : 400
figures ecartees (X ou Y quasi a l'infini): 0
ecart ABSOLU |x_X + y_Y| : median 3.33e-16 max 3.04e-08
ecart RELATIF : median 8.16e-16 p99 3.24e-12 max 6.50e-12
figures au-dessus du seuil 1e-09 : 0
VERDICT : aucune figure au-dessus du seuil 1e-09 -- la conclusion TIENT
Lecture : la mediane est au bruit machine (1e-16) ; la queue de distribution
monte a 1e-12 sur les figures a PETIT denominateur, ou x_X et y_Y
sont grands et ou l'annulation x_X + y_Y amplifie l'erreur d'arrondi
des intersections. C'est un effet de CONDITIONNEMENT, pas de theorie --
d'ou une tolerance declaree, et un ecart relatif comme critere.Les chiffres sont parlants : écart relatif médian \(8 \cdot 10^{-16}\) — le bruit machine — et une queue à \(7 \cdot 10^{-12}\) sur les figures à petit dénominateur, où \(x_X\) et \(y_Y\) sont grands et où l’annulation \(x_X + y_Y\) amplifie l’arrondi des intersections. C’est un effet de conditionnement, sur une tolérance relative déclarée (\(10^{-9}\)) : aucune figure ne la franchit. La moitié positive de l’énoncé est donc établie empiriquement sur les 400 figures.
Ce que la décomposition a changé. Le 03 produisait un verdict unique — « prem ≠ 0 » — qui ne veut rien dire sur une variété réductible. Le découpage en composantes le remplace par trois verdicts distincts :
| Composante | Verdict | Ce qui l’établit |
|---|---|---|
| \(d_2 \neq a_2\) et \(b_2 \neq c_2\) | prouvé | 400 figures ci-dessus (et la chaîne du 03 y suffit) |
| \(d_2 = a_2\) (ou l’autre bord) | muet — l’énoncé n’a plus d’objet | témoin rationnel du §4 |
| doublement dégénéré | \(g_2 \equiv 0\) trivialement | substitution symbolique du §4 |
L’énoncé correct du papillon porte donc une hypothèse de position que la version orale gardait implicite : aucune des deux cordes ne doit être parallèle à \((PQ)\). C’est l’archétype de ce que la littérature appelle (en souriant) le folklore « geometry problems never take care of degeneracies » — et c’est exactement la classe d’omissions que les systèmes à base de LLM reproduisent quand ils « démontrent » un énoncé sans générer ses non-dégénérescences.
Une méthode qui pardonne tout n’est pas une méthode. Test de résistance : sur le même lieu non dégénéré, un énoncé faux doit être rejeté.
Prenons les hypothèses de T2 et une conclusion délibérément fausse — la même que \(g_2\) avec le second terme doublé :
\[g_2^{\times} \;=\; (a_1 d_2 - a_2 d_1)(b_2 - c_2) \;+\; 2\,(c_1 b_2 - c_2 b_1)(d_2 - a_2)\]
qui affirme « \(x_X + 2\,y_Y = 0\) » — ce qu’aucune figure générique ne vérifie.
g2_faux = (a1*d2 - a2*d1)*(b2 - c2) + 2*(c1*b2 - c2*b1)*(d2 - a2)
R2f = wu_prem(g2_faux, B2, V2)
print("prem(g2_faux, CS) =", R2f if R2f == 0 else "polynome NON NUL")
print("VERDICT Wu :", "REJETE (reste non nul)" if R2f != 0 else "prouve ?! -- incoherent\n")
# Controle independant : la conclusion fausse est refutee sur une figure generique.
A_, B_ = corde(1.0, 2.0); C_, D_ = corde(2.0, 2.0)
xXv = abscisse(A_, D_); yYv = abscisse(C_, B_)
print(f"sur la figure generique (c=2, pentes 1 et 2) :")
print(f" x_X + y_Y = {xXv + yYv:+.2e} <- l'enonce VRAI est satisfait")
print(f" x_X + 2*y_Y = {xXv + 2*yYv:+.4f} <- l'enonce FAUX ne l'est pas")
print()
print("Deux lectures independantes concordent : l'enonce faux est rejete.")prem(g2_faux, CS) = polynome NON NUL
VERDICT Wu : REJETE (reste non nul)
sur la figure generique (c=2, pentes 1 et 2) :
x_X + y_Y = -1.39e-17 <- l'enonce VRAI est satisfait
x_X + 2*y_Y = +0.1055 <- l'enonce FAUX ne l'est pas
Deux lectures independantes concordent : l'enonce faux est rejete.Exercice 1 — le bord symétrique. Le §4 a construit le témoin du bord \(d_2 = a_2\). Faites le même travail pour le bord \(b_2 = c_2\) : construisez un témoin dont toutes les coordonnées sont rationnelles, vérifiant \(H_2\), avec \(b_2 = c_2\) et \(g_2 \neq 0\), puis établissez laquelle des deux abscisses part à l’infini. Indice : par symétrie du problème (\(A \leftrightarrow C\), \(B \leftrightarrow D\)), vous pouvez partir du témoin du §4 et échanger les rôles des deux cordes — mais vérifiez que les six hypothèses tiennent encore, une par une, avec
subs.
# Exercice 1 -- le bord b2 = c2 : a completer
# Etape 1 : construire un temoin rationnel verifiant H2 avec b2 == c2
# Etape 2 : verifier les six hypotheses par subs, comme au §4
# Etape 3 : montrer laquelle des deux abscisses part a l'infini
temoin_ex1 = None # a remplacer par le dictionnaire de substitution
abscisse_infinie_ex1 = None # a remplacer par "x_X" ou "y_Y"
print("Exercice a completer")Exercice a completerExercice 2 — faire se déclencher la scission. Le §3 a mesuré que les initiales de la chaîne du papillon sont toutes irréductibles. Construisez un système (géométrique ou non) dont la chaîne porte une initiale réductible dans sa deuxième cellule — puis faites tourner
ritt_split_onedessus et comparez l’ordre des polynômes de chaîne dans chaque branche avec celui du §3. Indice : dans \(H_s\), l’initiale réductible est portée par la cellule de variable principale la plus basse. Pour la déplacer au deuxième étage, il faut un polynôme dont la variable principale est intermédiaire et dont le coefficient dominant se factorise.
# Exercice 2 -- faire se declencher la scission au deuxieme etage : a completer
# Etape 1 : ecrire un systeme Hs2 dont la 2e cellule de chaine porte une initiale reductible
# Etape 2 : lancer ritt_split_one(Hs2, V) et compter les branches
# Etape 3 : comparer l'ordre des polynomes de chaine a celui du §3
branches_ex2 = None # a remplacer par la liste des branches
print("Exercice a completer")Exercice a completerExercice 3 — un théorème du corpus de Chou. Chou (1988) recense des centaines d’encodages classiques. Prenez-en un (par exemple : les trois médianes d’un triangle sont concourantes), encodez-le, lancez le test de Wu du 03, puis appliquez la mesure du §3 : factorisez les initiales de la chaîne obtenue. Attendu : le test doit conclure. La question intéressante est la seconde — et sa réponse n’est pas la même pour tous les théorèmes du corpus : c’est précisément ce qui décide si la décomposition est nécessaire ou non.
# Exercice 3 -- un theoreme du corpus de Chou : a completer
# Etape 1 : encoder le theoreme (variables, hypotheses H, conclusion g)
# Etape 2 : char_set_basic + wu_prem -> verdict
# Etape 3 : factoriser l'initiale de CHAQUE cellule de la chaine (mesure du §3)
verdict_ex3, initiales_reductibles_ex3 = None, None
print("Exercice a completer")Exercice a completer| Brique | Rôle | Où |
|---|---|---|
| identité \(g_2 = x_X(b_2-c_2) + y_Y(d_2-a_2)\) | la conclusion est un quotient, pas un polynôme | §2, vérifiée (assert) |
ritt_split_one |
la scission de Ritt, sur un système conçu pour la déclencher | §3 (3 branches) |
| initiales de CS(T2) | mesure : toutes irréductibles → la scission ne s’y déclenche pas | §3 |
| témoin rationnel | le bord \(d_2 = a_2\) : \(g_2 = 24/5\) là où \(X\) est à l’infini | §4 |
| 400 figures | le lieu non dégénéré satisfait le milieu au bruit machine | §5 |
| \(g_2^{\times}\) | un énoncé faux, rejeté par le moteur et par la figure | §6 |
Ce que ce notebook a ajouté au 03. Le 03 montrait comment une preuve automatique se construit. Celui-ci montre comment se lit un échec — et le résultat n’est ni « le théorème est faux » ni « l’outil est insuffisant » :
Ce que ce notebook ne fait pas. La récursion complète de Ritt–Ritt (une seule scission, borne déclarée au §3) ; la démonstration de terminaison et de complexité ; et le classement automatique d’une composante en « dégénérée » ou « légitime » — ici, c’est l’analyse géométrique humaine qui tranche, et ce partage des rôles est celui de Chou (1988).
G:\Mon Drive\MyIA\IA\Bibliographie IA\Symbolic\). Résultats : Wu seul 15/30 — dont deux problèmes (2021 P3, 2008 P1B) qu’aucun autre système évalué ne résout ; Wu&DD+AR 21/30, niveau médaille d’argent, sur un laptop CPU (AMD Ryzen 7 5800H, 16 Go, 5 min par problème) ; AlphaGeometry + Wu 27/30, premier résultat au-dessus d’une médaille d’or. Attention à l’attribution : DD+AR désigne deductive databases (un moteur de règles géométriques) et angle, ratio and distance chasing (recherche d’angles, de rapports et de distances) — des méthodes synthétiques. Ce n’est pas la décomposition de Ritt, qui est une brique algébrique de Wu. Le mot « Ritt » ne figure pas dans cet article.Série Geometry : Geometry-04 — DD+AR → Notebook de la série Geometry — SymbolicAI. Accrétion de recherche de la troisième étape. Fait partie du cycle complet du raisonnement vérifiable du dépôt CoursIA.