Geometry 02 — Prouver par l’algèbre

Public : Licence — deuxième étape de la série Geometry, le programme gradué de la preuve automatique en géométrie.

Ce que ce notebook suppose. Le notebook Geometry-01 — De la figure à l’équation : traduire une figure en hypothèse polynomiale \(H\), une propriété en conclusion \(C\), et tester \(C\) sous \(H\) par tirages aléatoires (Schwartz-Zippel).

Ce que vous emportez. Le passage du test à la preuve : l’idéal engendré par les hypothèses, l’appartenance de la conclusion à cet idéal via une base de Gröbner, le certificat qui l’accompagne, et le phénomène central que le 01 avait laissé dans l’ombre — les non-dégénérescences, et leur traitement algébrique par saturation.

Où en sommes-nous ?

Le 01 s’est arrêté sur un constat mesuré : sur \(100\) figures rectangle tirées au hasard, la conclusion \(C_1\) (le milieu de l’hypoténuse est équidistant de \(A\) et \(B\)) s’est annulée \(100\) fois, et Schwartz-Zippel bornait la probabilité d’un faux accord à \(7{,}7 \times 10^{-171}\). Autant dire : aucun doute pratique.

Mais un test, même vert à \(10^{-171}\) près, reste un test. La question que ce notebook pose — et résout — est d’une autre nature :

\(C_1\) s’annule-t-elle sur toute figure satisfaisant \(H\), sans exception, sans probabilité ?

La réponse tiendra en une identité d’une ligne, \(C_1 = 1 \cdot H\), que nous dégagerons par la machinerie générale des idéaux et des bases de Gröbner. Et cette machinerie nous réserve deux surprises : elle dit mieux que ce qu’on lui demande (le cercle circonscrit), elle sait dire non (le rectangle n’implique pas l’isocélé), et elle révèle que certains théorèmes géométriques sont faux tels qu’énoncés — jusqu’à ce qu’on leur adjoint des non-dégénérescences, dont l’algèbre a un traitement exact.

Plan

1. §1 Les objets du fil rouge, reconstruits
2. §2 L’idéal engendré par les hypothèses : payer la conclusion avec les hypothèses
3. §3 Bases de Gröbner : l’appartenance décidable
4. §4 Le certificat dit mieux : le cercle circonscrit
5. §5 La machine dit non : le rectangle n’implique pas l’isocélé
6. §6 Deux hypothèses : le vrai besoin, et un théorème faux
7. §7 L’astuce de Ritt : rendre une non-dégénérescence inversible
8. §8 Le prix : coût de la certitude
9. §9-§11 Trois exercices

import sys
import time

import sympy as sp

print("Python :", sys.version.split()[0])
print("sympy  :", sp.__version__)

Python : 3.13.15
sympy  : 1.14.0

§1 — Les objets du fil rouge

Exactement comme au 01 : trois points \(A\), \(B\), \(C\) à coordonnées symboliques, l’hypothèse « angle droit en \(A\) » comme nullité du produit scalaire \(\vec{AB} \cdot \vec{AC}\), et la conclusion comme différence de carrés de distances au milieu \(M\) de \([B, C]\).

\[H = (x_B - x_A)(x_C - x_A) + (y_B - y_A)(y_C - y_A) \qquad C_1 = MA^2 - MB^2\]

Tout le notebook est déterministe : aucun tirage aléatoire, aucune probabilité. C’est la marque du changement de nature — on ne teste plus, on démontre.

# Les objets du fil rouge, reconstruits comme au 01
xA, yA, xB, yB, xC, yC = sp.symbols('x_A y_A x_B y_B x_C y_C')

# Hypothese : angle droit en A, c'est-a-dire AB scalaire AC nul
H = (xB - xA) * (xC - xA) + (yB - yA) * (yC - yA)

# Milieu M de l'hypotenuse [B, C]
Mx, My = (xB + xC) / 2, (yB + yC) / 2

# Conclusion C1 : M equidistant de A et B (difference des carres)
C1 = sp.expand((Mx - xA) ** 2 + (My - yA) ** 2 - ((Mx - xB) ** 2 + (My - yB) ** 2))

print("H  =", H)
print("C1 =", C1)

H  = (-x_A + x_B)*(-x_A + x_C) + (-y_A + y_B)*(-y_A + y_C)
C1 = x_A**2 - x_A*x_B - x_A*x_C + x_B*x_C + y_A**2 - y_A*y_B - y_A*y_C + y_B*y_C

Lecture du résultat

L’hypothèse \(H\) est un polynôme à six variables ; la conclusion \(C_1\) aussi, une fois le milieu substitué. La question « toute figure rectangle satisfait-elle \(C_1 = 0\) ? » devient :

le polynôme \(C_1\) s’annule-t-il partout où le polynôme \(H\) s’annule ?

§2 — L’idéal engendré par les hypothèses

L’observation clé est algébrique. Considérons l’ensemble de tous les multiples de \(H\) :

\[\langle H \rangle = \{ A \cdot H \;:\; A \ \text{polynôme} \}\]

C’est l’idéal engendré par \(H\). Il a une propriété de transfert immédiate :

si \(C \in \langle H \rangle\), alors \(C\) s’annule partout où \(H\) s’annule.

La raison tient en une ligne : si \(C = A \cdot H\) et \(H(\text{figure}) = 0\), alors \(C(\text{figure}) = A(\text{figure}) \cdot 0 = 0\). L’écriture \(C = A \cdot H\) est un certificat : quiconque peut le vérifier d’un simple développement. On dit que la conclusion est payée cash par les hypothèses.

Notre idéal est principal (un seul générateur) — le cas le plus simple possible. Le premier geste, naturel, est de tenter la division de \(C_1\) par \(H\).

# Division de C1 par H : quotient et reste disent tout
quotient, reste = sp.div(C1, H, xA, yA, xB, yB, xC, yC)
print("quotient :", quotient)
print("reste    :", reste)

# Verification independante du certificat : C1 - quotient * H doit etre nul
print("certificat C1 = quotient * H :", sp.expand(C1 - quotient * H) == 0)

quotient : 1
reste    : 0
certificat C1 = quotient * H : True

Lecture du résultat — le théorème est démontré

\(q = 1\), \(r = 0\) : la division ne laisse aucun reste, et le certificat se vérifie par un simple développement.

\[C_1 = 1 \cdot H\]

Autrement dit : après substitution du milieu, la conclusion est exactement l’hypothèse. Le théorème du milieu de l’hypoténuse tient en une identité polynomiale. Sa portée dépasse tout ce que le 01 pouvait affirmer :

• toute figure, pas une famille paramétrée ;
• y compris les figures dégénérées (\(A = B\), \(A = C\), points confondus) ;
• sur tout corps de coefficients, réels ou complexes.

Le 01 mesurait une probabilité ; le 02 exhibe un certificat. La probabilité disparaît de l’énoncé.

§3 — Bases de Gröbner : l’appartenance décidable

Si \(\langle H \rangle\) était toujours principal, une division suffirait et ce notebook s’arrêterait ici. Mais dès qu’un théorème a deux hypothèses \(H_1, H_2\), l’idéal \(\langle H_1, H_2 \rangle\) contient les combinaisons \(A \cdot H_1 + B \cdot H_2\), et la division naïve par une liste de polynômes dépend de l’ordre des diviseurs et de l’ordre des monômes : le même calcul peut laisser un reste non nul alors que la conclusion appartient à l’idéal (l’exemple canonique \(f = xy^2 - x\) divisé par \(xy + 1\) et \(y - 1\) est détaillé au chapitre 2 de Cox, Little et O’Shea, Ideals, Varieties, and Algorithms).

La base de Gröbner est la réparation exacte : une base de l’idéal dont le reste de division est canonique — indépendant de l’ordre des diviseurs — ce qui rend l’appartenance décidable :

\(C \in \langle H_1, \ldots, H_s \rangle\) si et seulement si le reste de \(C\) par la base de Gröbner est nul.

Et le calcul rend les coefficients du certificat \(C = \sum_i A_i G_i\). Appliquons la machinerie générale à notre idéal — trivial ici, mais c’est elle qui portera les sections suivantes.

# Base de Groebner de l'ideal <H>, ordre lexicographique
G = sp.groebner([H], xA, yA, xB, yB, xC, yC, order='lex')
print("G =", G)

coefs, reste = G.reduce(C1)
print("coefficients :", coefs)
print("reste        :", reste)
print("certificat   :", sp.expand(coefs[0] * H - C1) == 0)

G = GroebnerBasis([x_A**2 - x_A*x_B - x_A*x_C + x_B*x_C + y_A**2 - y_A*y_B - y_A*y_C + y_B*y_C], x_A, y_A, x_B, y_B, x_C, y_C, domain='ZZ', order='lex')
coefficients : [1]
reste        : 0
certificat   : True

Lecture du résultat

Pour un idéal principal, la base de Gröbner est le générateur lui-même, réécrit tête d’abord — aucune surprise. Ce qui compte est le verdict : reste \(0\), coefficients \([1]\). La machinerie générale confirme l’appartenance de \(C_1\) et redis le certificat du §2.

À partir de maintenant, nous disposons d’un décideur d’appartenance : pour n’importe quelle conclusion \(C\), G.reduce(C) répond oui (reste nul, avec certificat) ou non (reste non nul). Les trois sections qui suivent le mettent à l’épreuve dans les trois régimes possibles : il en dit plus, il dit non, il échoue — et l’échec est informatif.

§4 — Le certificat dit mieux : le cercle circonscrit

Le 01 concluait « \(MA = MB\) ». Mais un théorème de géométrie en cache souvent d’autres. Deux questions naturelles :

• \(C_p = MA^2 - MC^2\) (équidistance de \(A\) et \(C\)) : est-elle elle aussi payée par les hypothèses ?
• \(C_3 = MB^2 - MC^2\) (équidistance de \(B\) et \(C\)) : que dit la machine ?

# Cp : equidistance de A et C ; C3 : equidistance de B et C
Cp = sp.expand((Mx - xA) ** 2 + (My - yA) ** 2 - ((Mx - xC) ** 2 + (My - yC) ** 2))
C3 = sp.expand((Mx - xB) ** 2 + (My - yB) ** 2 - ((Mx - xC) ** 2 + (My - yC) ** 2))

coefs_p, reste_p = G.reduce(Cp)
print("Cp : coefficients =", coefs_p, "| reste =", reste_p)
print("C3 identiquement nul :", C3 == 0, "| reste par G =", G.reduce(C3)[1])

Cp : coefficients = [1] | reste = 0
C3 identiquement nul : True | reste par G = 0

Lecture du résultat — trois équidistances

Trois régimes distincts, mesurés :

• \(C_1 \in \langle H \rangle\) avec coefficient \(1\) : payée par l’hypothèse ;
• \(C_p \in \langle H \rangle\) avec coefficient \(1\) également — c’est encore \(C_p = H\) : payée aussi ;
• \(C_3\) est identiquement nul : \(M\) est le milieu de \([B, C]\), donc \(MB = MC\) est vrai de tout triangle, rectangle ou non — aucune hypothèse nécessaire.

En composant : \(MA = MB\), \(MA = MC\), \(MB = MC\) — le point \(M\) est équidistant des trois sommets. Le triangle rectangle a un cercle circonscrit, et son centre est le milieu de l’hypoténuse. Le théorème complet du 01 était plus riche que sa conclusion : la machine l’a dit sans qu’on le demande.

Retenons aussi la distinction fine entre deux façons d’être « toujours vrai » : par identité (\(C_3\), vrai de tout triangle) ou par appartenance à l’idéal (\(C_1\), vrai de tout triangle rectangle).

§5 — La machine dit non : le rectangle n’implique pas l’isocélé

Décidons l’appartenance d’une conclusion fausse. Candidat : « tout triangle rectangle est isocèle », c’est-à-dire \(C_{iso} = AB^2 - AC^2\).

# Temoin negatif : le rectangle implique-t-il AB = AC ?
Ciso = (xB - xA) ** 2 + (yB - yA) ** 2 - ((xC - xA) ** 2 + (yC - yA) ** 2)
reste_iso = G.reduce(Ciso)[1]
print("reste de Ciso par G :", reste_iso)
print("reste nul ?", reste_iso == 0)

# Contre-exemple : u = (3, 0), v = (0, 4) -- triangle 3-4-5, rectangle non isocele
sub_345 = {xA: 0, yA: 0, xB: 3, yB: 0, xC: 0, yC: 4}
print("sur la figure 3-4-5 : H =", H.subs(sub_345), "| Ciso =", Ciso.subs(sub_345))

reste de Ciso par G : -2*x_A*x_B + 2*x_A*x_C + x_B**2 - x_C**2 - 2*y_A*y_B + 2*y_A*y_C + y_B**2 - y_C**2
reste nul ? False
sur la figure 3-4-5 : H = 0 | Ciso = -7

Lecture du résultat

Le reste est non nul : \(C_{iso} \notin \langle H \rangle\). Parce que le reste par une base de Gröbner est canonique, sa non-nullité est une preuve de non-appartenance — la machine ne se trompe pas de sens.

Et le terrain confirme : sur le triangle \(3\)-\(4\)-\(5\), \(H = 0\) mais \(C_{iso} = -7\) (\(AB = 3\), \(AC = 4\)). Le « théorème » est faux, et l’algèbre l’avait dit avant le contre-exemple.

Une nuance honnête pour aller au fond : l’appartenance à l’idéal implique l’annulation sur les figures, mais la réciproque est plus subtile — sur les complexes, c’est l’appartenance à la racine de l’idéal qui caractérise l’annulation (Nullstellensatz de Hilbert). Pour trancher qu’une conclusion n’est pas une conséquence géométrique, le contre-exemple explicite reste l’argument décisif ; la machine non nulle + le \(3\)-\(4\)-\(5\) font ici cause commune.

§6 — Deux hypothèses : le vrai besoin, et un théorème faux

Passons à un théorème à deux hypothèses — le régime où la base de Gröbner devient nécessaire. Énoncé candidat :

si \(AB \perp AC\) et \(AB \perp AD\), alors \(C\), \(A\), \(D\) sont alignés.

(Deux perpendiculaires à une même droite en un même point : même direction.) Pour alléger, nous fixons \(A\) à l’origine par translation — un geste de normalisation standard, la propriété étant invariante par isométrie. Les hypothèses et la conclusion deviennent :

\[H_{2a} = x_B x_C + y_B y_C \qquad H_{2b} = x_B x_D + y_B y_D \qquad C = x_C y_D - x_D y_C\]

La conclusion est le produit vectoriel \(\vec{AC} \wedge \vec{AD}\) : nul si et seulement si les vecteurs sont alignés.

# A fixe a l'origine : six inconnues restantes
xD, yD = sp.symbols('x_D y_D')
H2a = xB * xC + yB * yC    # AB scalaire AC = 0
H2b = xB * xD + yB * yD    # AB scalaire AD = 0
CONCL = xC * yD - xD * yC  # A, C, D alignes (produit vectoriel nul)
print("H2a   =", H2a)
print("H2b   =", H2b)
print("CONCL =", CONCL)

G3 = sp.groebner([H2a, H2b], xB, yB, xC, yC, xD, yD, order='lex')
print("G3 =", G3)
reste3 = G3.reduce(CONCL)[1]
print("reste de CONCL :", reste3, "| nul ?", reste3 == 0)

H2a   = x_B*x_C + y_B*y_C
H2b   = x_B*x_D + y_B*y_D
CONCL = x_C*y_D - x_D*y_C
G3 = GroebnerBasis([x_B*x_C + y_B*y_C, x_B*x_D + y_B*y_D, x_C*y_B*y_D - x_D*y_B*y_C], x_B, y_B, x_C, y_C, x_D, y_D, domain='ZZ', order='lex')
reste de CONCL : x_C*y_D - x_D*y_C | nul ? False

Lecture du résultat — l’échec est informatif

Le reste est non nul : la machine ne démontre pas l’alignement à partir des seules hypothèses. Mais lisez la base :

\[G_3 = [\, x_B x_C + y_B y_C, \;\; x_B x_D + y_B y_D, \;\; y_B \cdot (x_C y_D - x_D y_C) \,]\]

Le troisième élément contient la conclusion elle-même, multipliée par \(y_B\). Tout est en place dans l’idéal — sauf l’inversibilité du facteur \(y_B\). Le théorème est-il pour autant faux ? Testons le cas qui fait douter.

Pour aller plus loin — Surviving proofs, The Importance of Understanding (05/09/2026) Sheydvasser recommande, en principe 2, de situer un échec dans son réseau de concepts. Ici, la base de Gröbner \(G_3\) ne démontre pas l’alignement à partir des seules hypothèses, mais elle exhibe la conclusion elle-même dans la base — c’est exactement l’inverse d’un mur silencieux : l’échec dit quelque chose. C’est le geste « lire structurellement » qu’elle défend à l’article 1 : un polynôme dans une base de Gröbner n’est pas juste un terme technique, c’est une position dans un réseau qui révèle où la preuve manque. Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/the-importance-of-understanding Archivé : G:DriveIA-Proves-Surviving-Proofs\2026-09-05_the-importance-of-understanding.html

# Contre-exemple : B = A rend les deux hypotheses trivialement vraies
sub_BA = {xB: 0, yB: 0, xC: 1, yC: 0, xD: 0, yD: 1}
print("H2a =", H2a.subs(sub_BA), "| H2b =", H2b.subs(sub_BA), "| CONCL =", CONCL.subs(sub_BA))

H2a = 0 | H2b = 0 | CONCL = 1

Lecture du résultat — le théorème est faux tel qu’énoncé

Avec \(B = A\) : les deux hypothèses valent \(0\) trivialement (le vecteur \(\vec{AB}\) est nul, « perpendiculaire » à tout), et la conclusion vaut \(1\) — \(C = (1,0)\) et \(D = (0,1)\) ne sont pas alignés avec \(A\).

Le théorème géométrique, énoncé avec des mots, sous-entendait \(B \neq A\) — la phrase « la perpendiculaire en \(A\) à la droite \(AB\) » n’a de sens que si \(B \neq A\). Cette condition invisible dans les équations est une non-dégénérescence. Toute la géométrie automatisée vit avec elles : un énoncé honnête est un système d’hypothèses plus ses non-dégénérescences. La question devient : comment dire « \(g \neq 0\) » dans un monde qui ne parle que de nullités de polynômes ?

Pour aller plus loin — Surviving proofs, Counterexamples and Contradictions (12/09/2026) Sheydvasser recommande de chercher le contre-exemple le plus simple d’abord. Ici, \(B = A\) est exactement ce contre-exemple catégorique : il rend les deux hypothèses trivialement vraies (le vecteur \(\vec{AB}\) est nul, donc perpendiculaire à tout) et la conclusion trivialement fausse. C’est le pattern Sheydvasser art. 2 : « dégénéré par construction → généraliser l’énoncé pour exclure la dégénérescence » — ici en exigeant \(B \neq A\), ce que la cellule [25] fait explicitement par saturation de l’idéal. Senia Sheydvasser, The Deranged Mathematician (Substack), URL https://derangedmathematician.substack.com/p/counterexamples-and-contradictions Archivé : G:DriveIA-Proves-Surviving-Proofs\2026-09-12_counterexamples-and-contradictions.html

§7 — L’astuce de Ritt : rendre \(g\) inversible

L’astuce (due à Ritt, systématisée par Wu) est d’une élégance totale : pour imposer \(g \neq 0\), on adjoint à l’idéal le polynôme

\[z \cdot g - 1\]

où \(z\) est une nouvelle variable. Si une figure satisfait les hypothèses et \(z \, g = 1\), alors \(g\) y est inversible — en particulier non nul. On démontre la conclusion dans l’idéal saturé ; l’opération s’appelle la saturation.

Ici \(g = x_B^2 + y_B^2\) : sur les figures réelles, \(g \neq 0\) signifie exactement \(B \neq A\).

# Non-degenerescence B != A : rendre g = xB^2 + yB^2 inversible
z = sp.symbols('z')
g_nd = xB ** 2 + yB ** 2
G4 = sp.groebner([H2a, H2b, z * g_nd - 1], xB, yB, xC, yC, xD, yD, z, order='lex')
reste4 = G4.reduce(CONCL)[1]
print("reste de CONCL apres saturation :", reste4)
print("theoreme demontre sous B != A :", reste4 == 0)

reste de CONCL apres saturation : 0
theoreme demontre sous B != A : True

Lecture du résultat — démontré, proprement cette fois

Reste nul : pour toute figure avec \(B \neq A\), deux perpendiculaires à \(AB\) en \(A\) portent des points alignés avec \(A\). Le théorème est maintenant vrai — c’est-à-dire : l’énoncé corrigé par sa non-dégénérescence est un théorème.

C’est exactement le geste que la méthode de Wu (objet du 03) industrialise : énoncé, hypothèses, conclusion, non-dégénérescences découvertes par la machinerie elle-même. Notons en passant une subtilité que nous laisserons au 03 : sur les complexes, \(x_B^2 + y_B^2 = 0\) a d’autres solutions que \(B = A\) (par exemple \(x_B = 1\), \(y_B = i\)) — la géométrie réelle mérite son propre traitement, et la saturation exacte de \(B \neq A\) réel demande un peu plus de soin. L’esprit du geste est intact.

§8 — Le prix : coût de la certitude

La base de Gröbner est l’outil décisionnel central de l’algèbre commutative effective — au prix d’une complexité au pire cas doublement exponentielle en le nombre de variables : les degrés des éléments de la base peuvent exploser. Nos exemples sont minuscules ; mesurons-les quand même, pour fixer les ordres de grandeur.

# Trois echelles : 1 hypothese, 2 hypotheses, 2 hypotheses + saturation
t0 = time.perf_counter()
_ = sp.groebner([H], xA, yA, xB, yB, xC, yC, order='lex')
t1 = time.perf_counter()
_ = sp.groebner([H2a, H2b], xB, yB, xC, yC, xD, yD, order='lex')
t2 = time.perf_counter()
_ = sp.groebner([H2a, H2b, z * g_nd - 1], xB, yB, xC, yC, xD, yD, z, order='lex')
t3 = time.perf_counter()
print("groebner, 1 hypothese (6 var)   : %.4f s" % (t1 - t0))
print("groebner, 2 hypotheses (6 var)  : %.4f s" % (t2 - t1))
print("groebner, sature (7 var)        : %.4f s" % (t3 - t2))

groebner, 1 hypothese (6 var)   : 0.0005 s
groebner, 2 hypotheses (6 var)  : 0.0004 s
groebner, sature (7 var)        : 0.0018 s

Lecture du résultat

Quelques millisecondes au plus chacun : nos idéaux sont de jouets. Sur des systèmes industriels — cinématique de robot, cryptographie, démonstration automatique à grande échelle — le même calcul peut prendre des heures ou saturer la mémoire, et le choix de l’ordre des variables devient un art.

Pour les énoncés géométriques, il existe une voie structurellement plus économique : la méthode de Wu, fondée sur la pseudo-division et les ensembles caractéristiques, qui exploite la forme triangulaire des hypothèses géométriques. C’est l’objet du 03 — et le fil rouge continuera : le même théorème du milieu, démontré par une troisième voie.

§9 — Exercice 1 : Pythagore appartient à l’idéal

Le 01 vérifiait \(P = AB^2 + AC^2 - BC^2\) par tirages ; le certificat attendu ici est une appartenance : montrez que \(P \in \langle H \rangle\) et lisez le coefficient.

• Étape 1. Construisez \(P\) (pensez à sp.expand).
• Étape 2. Réduisez \(P\) par la base G.
• Étape 3. Rendez (coefs, reste) — le coefficient attendu est un entier.

# Exercice 1 : Pythagore appartient a l'ideal
# Etape 1 : construire P = AB^2 + AC^2 - BC^2
# Etape 2 : reduire P par la base G
# Etape 3 : retourner (coefs, reste)
P_ex1 = None        # TODO etudiant : construire P
resultat_ex1 = None  # TODO etudiant : (coefs, reste) de G.reduce(P_ex1)
print("Exercice 1 : P et le verdict d'appartenance")

Exercice 1 : P et le verdict d'appartenance

# Verification de l'exercice 1
if resultat_ex1 is None:
    print("Exercice 1 a completer")
else:
    coefs_e1, reste_e1 = resultat_ex1
    print("coefficient :", coefs_e1, "| reste :", reste_e1)
    print("certificat P = coefficient * H attendu :", reste_e1 == 0)

Exercice 1 a completer

§10 — Exercice 2 : la machine dit non, encore

Le théorème « tout triangle rectangle est tel que \(AB = BC\) » (côté et hypoténuse égaux) : testez l’appartenance de \(AB^2 - BC^2\) à \(\langle H \rangle\), puis produisez un contre-exemple chiffré — une figure rectangle où l’écart est visible.

• Étape 1. Construisez \(Q = AB^2 - BC^2\).
• Étape 2. Réduisez par G et rendez le reste.
• Étape 3. Choisissez des coordonnées rectangle (le \(3\)-\(4\)-\(5\) du §5 reste disponible) et calculez \(H\) et \(Q\) dessus : rendez le dictionnaire de substitution.

# Exercice 2 : AB = BC ?
# Etape 1 : construire Q = AB^2 - BC^2
# Etape 2 : reduire par G
# Etape 3 : contre-exemple chiffre (dictionnaire de substitution)
Q_ex2 = None          # TODO etudiant : construire Q
reste_ex2 = None      # TODO etudiant : G.reduce(Q_ex2)[1]
sub_ex2 = None        # TODO etudiant : dictionnaire {xA: ..., ..., yC: ...}
print("Exercice 2 : verdict d'appartenance + contre-exemple")

Exercice 2 : verdict d'appartenance + contre-exemple

# Verification de l'exercice 2
if reste_ex2 is None or sub_ex2 is None:
    print("Exercice 2 a completer")
else:
    print("reste :", reste_ex2, "| nul ?", reste_ex2 == 0)
    print("sur la figure : H =", H.subs(sub_ex2), "| Q =", Q_ex2.subs(sub_ex2))

Exercice 2 a completer

§11 — Exercice 3 : saturations partielles

La saturation du §7 imposait \(x_B^2 + y_B^2 \neq 0\) d’un seul geste. On peut viser plus fin : saturer par \(x_B\) seul (\(z \cdot x_B - 1\), c’est-à-dire \(x_B \neq 0\)), puis par \(y_B\) seul.

• Étape 1. Construisez les deux bases saturées et réduisez CONCL par chacune : rendez les deux restes.
• Étape 2. Réflexion (à écrire en commentaire dans la cellule) : la première saturation démontre le théorème sur la zone \(x_B \neq 0\) seulement. Vérifiez ce que valent les hypothèses et la conclusion quand \(x_B = 0\) mais \(y_B \neq 0\) — que force \(H_{2a}\) sur \(y_C\), \(H_{2b}\) sur \(y_D\) ? La conclusion tient-elle quand même ?
• Étape 3. Concluez : pourquoi la saturation complète du §7 reste-t-elle le bon geste unique ?

# Exercice 3 : saturations partielles z*x_B - 1 et z*y_B - 1
# Etape 1 : les deux bases et les deux restes de CONCL
# Etape 2 : que se passe-t-il sur la zone x_B = 0, y_B != 0 ?
# Etape 3 : pourquoi la saturation complete est-elle le geste general ?
reste_part1 = None  # TODO etudiant : reste de CONCL par groebner([H2a, H2b, z*xB - 1])
reste_part2 = None  # TODO etudiant : reste de CONCL par groebner([H2a, H2b, z*yB - 1])
print("Exercice 3 : deux saturations partielles")

Exercice 3 : deux saturations partielles

# Verification de l'exercice 3
if reste_part1 is None or reste_part2 is None:
    print("Exercice 3 a completer")
else:
    print("reste avec z*x_B - 1 :", reste_part1, "| nul ?", reste_part1 == 0)
    print("reste avec z*y_B - 1 :", reste_part2, "| nul ?", reste_part2 == 0)

Exercice 3 a completer

Conclusion

Question	Outil	Verdict mesuré
\(C_1\) payée par \(H\) ?	division, base de Gröbner	oui — certificat \(C_1 = 1 \cdot H\), reste \(0\)
cercle circonscrit ?	appartenance de \(C_p\), \(C_3\)	oui — \(C_p = 1 \cdot H\), \(C_3 \equiv 0\)
rectangle \(\Rightarrow\) isocèle ?	reste canonique + \(3\)-\(4\)-\(5\)	non — reste non nul, contre-exemple
deux perpendiculaires \(\Rightarrow\) alignement ?	Gröbner de \(\langle H_{2a}, H_{2b} \rangle\)	faux tel quel (\(B = A\)), base contenant \(y_B \cdot C\)
…avec \(B \neq A\) ?	saturation \(z \cdot g - 1\)	démontré — reste \(0\)

Ce que vous emportez :

• l’idéal des hypothèses et sa propriété de transfert — l’appartenance est un certificat ;
• la base de Gröbner comme décideur d’appartenance (restes canoniques, coefficients du certificat) ;
• les non-dégénérescences : les énoncés géométriques sont faux sans elles, et la saturation \(z \cdot g - 1\) les rend algébriques ;
• le sens des deux limites : coût doublement exponentiel au pire cas, et subtilité réelle vs complexe.

L’étape suivante, Geometry-03 — la méthode de Wu, remplace la base de Gröbner par la pseudo-division et les ensembles caractéristiques, la voie que les systèmes réels de preuve géométrique ont préférée — appliquée au même fil rouge.