Another example

Consider the following construction: we place a circle of radius 1 and center at (1,0), tangent to the side AB at E(r,s). Tracing a line through DE, meets side AC at F(n,c). We want to prove that d(AE)=d(AF)

Hypotheses :
(r,s) in circle: (r-1)^2+s^2-1
(r,s) in side AB: a(r-s)-s(m-b)
(n,c) in line DE: s(n-2)-(r-2)c
(n,c) in line AC: an-cm
tangency: (r-1,s) perpendicular to AB: (r-b)(r-1)+s^2

Thesis :
(n-m)^2+(c-a)^2=(m-r)^2+(a-s)^2

Theorem is not algebraically true:

NF(1,Ideal((r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))t-1))

1
-------------------------------

We have two independent variables, namely, {m, a}. But

Use R::=Q[ncrsbma]

H:=Ideal((r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2)

Dim(R/H)

3
-------------------------------
Now we enlarge our ring with slack variables and proceed to find non-degeneracy conditions in the privileged variables:

Use R::=Q[htncrsbma]

Elim(h..b,Ideal((r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))t-1))

Ideal(0)
-------------------------------

Thus the theorem is not generally true. Next we try discovery conditions:

Elim(h..b,Ideal((r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))))

Ideal(0)

So the theorem is not generally false.

We try using some common sense as well, adding some "evident" degeneracy conditions, such as ab(b-2)­0:

Elim(h..b,Ideal(ab(b-2)h-1,(r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))t-1))

Ideal(0)

Again, is not generally true, but...

Elim(h..b,Ideal(ab(b-2)h-1,(r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))))

Ideal(7334064023363320418313209011438936559226380203860462635896158200551856369707617646398052575168019076064629228927703259866611703801198420626941/1375504896591317280501164023579602056978667444754283094505064730927168633797221160315032582103357654894421733603430060755881767977751700m^3 + 7334064023363320418313209011438936559226380203860462635896158200551856369707617646398052575168019076064629228927703259866611703801198420626941/1375504896591317280501164023579602056978667444754283094505064730927168633797221160315032582103357654894421733603430060755881767977751700ma^2 - 7334064023363320418313209011438936559226380203860462635896158200551856369707617646398052575168019076064629228927703259866611703801198420626941/687752448295658640250582011789801028489333722377141547252532365463584316898610580157516291051678827447210866801715030377940883988875850m^2)

So it is generally false. This condition factors as m*something...

We try first with the condition m=0 (right triangles).

NF(1, Ideal(m,(r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2, ab(b-2)h-1,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))t-1))

0

So theorem is true for non degenerate right triangles.

But the theorem is also true for the other discovery condition:

Elim(h..b, Ideal(7334064023363320418313209011438936559226380203860462635896158200551856369707617646398052575168019076064629228927703259866611703801198420626941
/ 1375504896591317280501164023579602056978667444754283094505064730927168633797221160315032582103357654894421733603430060755881767977751700m^2+ 7334064023363320418313209011438936559226380203860462635896158200551856369707617646398052575168019076064629228927703259866611703801198420626941 / 1375504896591317280501164023579602056978667444754283094505064730927168633797221160315032582103357654894421733603430060755881767977751700a^2 - 7334064023363320418313209011438936559226380203860462635896158200551856369707617646398052575168019076064629228927703259866611703801198420626941 / 687752448295658640250582011789801028489333722377141547252532365463584316898610580157516291051678827447210866801715030377940883988875850m,
ab(b-2)h-1,(r-1)^2+s^2-1,
a(r-b)-s(m-b),
s(n-2)-(r-2)c,
an-cm,
(r-b)(r-1)+s^2,
((n-m)^2+(c-a)^2-((m-r)^2+(a-s)^2))t-1))

Ideal(-1)

The condition turns to be point (m,a) on the given circle!!!