ukjp

reference=[9vka]
title=Research Agenda for the Two-Circle Tangent Theorem: From Analytic Proof to Synthetic Understanding
author=bdpk
reviews:ACCEPT, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 3556
stdout:
```
ratio simplified: (R**3 + R**2*d + R**2*r + R*d*r - d**2*r - d*r**2)*(-R**2*d - R*d**2 + R*d*r + R*r**2 + d*r**2 + r**3)/(R*r*(R - d + r)*(R + d + r))
ratio numeric: -39.8181818181818
HT2 numeric: 0.181818181818182
product numeric: -7.23966942148760

```
stderr:
```
```

exit_code: 0
duration_ms: 2984
stdout:
```
product = (-R**3 - R**2*d - R**2*r - R*d*r + d**2*r + d*r**2)*(R**2*d + R*d**2 - R*d*r - R*r**2 - d*r**2 - r**3)/(R + d + r)**2
HT2 = R*r*(R - d + r)/(R + d + r)
product / HT2 = (R**3 + R**2*d + R**2*r + R*d*r - d**2*r - d*r**2)*(-R**2*d - R*d**2 + R*d*r + R*r**2 + d*r**2 + r**3)/(R*r*(R - d + r)*(R + d + r))
simplified ratio = (R**3 + R**2*d + R**2*r + R*d*r - d**2*r - d*r**2)*(-R**2*d - R*d**2 + R*d*r + R*r**2 + d*r**2 + r**3)/(R*r*(R - d + r)*(R + d + r))

```
stderr:
```
```

reference=[x2a1]
title=Power of a Point and Radical Axis Relations in the Two-Circle Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We compute the powers of the orthocenter H with respect to the various circles appearing in the two-circle tangent theorem. We discover identities linking these powers to the squared distance HT² and to the rational certificate ρ². These relations suggest a synthetic proof strategy based on radical axes and power of a point.

## Introduction

The tangent line theorem for two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r0$, $00.
\]
The points $C=(-r,0)$, $D=(d+R,0)$, $P$ is the circumcenter of $\triangle ACD$, $E$ and $F$ are the second intersections of line $AP$ with $\Omega$ and $\Gamma$, and $H$ is the orthocenter of $\triangle PMN$.

Define $T=R+r-d$ (positive under the intersection condition). Then
\[
E=A+\frac{T}{R}(P-A),\qquad F=A+\frac{T}{r}(P-A).
\]

## 2. Powers of $H$ with respect to the circles

Using the explicit formulas for $H$ we compute the following powers.

### 2.1 Power with respect to $\Omega$ and $\Gamma$

\[
\operatorname{Pow}_{H}(\Omega)=H_x^{2}+H_y^{2}-r^{2}
      =\frac{R^{2}d+Rd^{2}-Rdr-Rr^{2}-dr^{2}-r^{3}}{R+d+r},
\]
\[
\operatorname{Pow}_{H}(\Gamma)=(H_x-d)^{2}+H_y^{2}-R^{2}
      =\frac{-R^{3}-R^{2}d-R^{2}r-Rdr+d^{2}r+dr^{2}}{R+d+r}.
\]

Their difference simplifies to
\[
\operatorname{Pow}_{H}(\Omega)-\operatorname{Pow}_{H}(\Gamma)=R^{2}+Rd-dr-r^{2}.
\]

The radical axis of $\Omega$ and $\Gamma$ is the line $AB$ (the line $x=x_0$). Since $H_x=(d+R-r)/2$, the quantity $H_x-x_0$ equals the difference above divided by $2d$; consequently $H$ does **not** lie on $AB$ unless $R^{2}+Rd-dr-r^{2}=0$, which is a special relation between $d,r,R$.

### 2.2 Power with respect to $(BEF)$

Let $O$ be the circumcenter of $\triangle BEF$ and $R_{BEF}$ its radius. Then
\[
\operatorname{Pow}_{H}(BEF)=HO^{2}-R_{BEF}^{2}.
\]

A direct computation yields the surprisingly simple expression
\[
\boxed{\;\operatorname{Pow}_{H}(BEF)=\frac{Rr(R+r-d)}{R+d+r}\;}.
\]

This is exactly the quantity $HT^{2}$ found in [{50id}], where $T$ is the tangency point of $\ell$ with $(BEF)$. Indeed, if $\ell$ is tangent to $(BEF)$ at $T$, then $HT^{2}=\operatorname{Pow}_{H}(BEF)$ (the power of $H$ equals the square of the tangent length). Thus the tangency condition is equivalent to
\[
HO^{2}-R_{BEF}^{2}=HT^{2},
\]
which is automatically true because $HT^{2}$ is defined as $HO^{2}-R_{BEF}^{2}$. The non‑trivial part of the theorem is that this power coincides with the rational expression above.

### 2.3 Power with respect to $(ACD)$

Denote by $K$ the circumcircle of $\triangle ACD$. Then
\[
\operatorname{Pow}_{H}(K)=\frac{-R^{2}r-Rd^{2}-3Rdr-Rr^{2}-d^{3}-d^{2}r}{R+d+r}.
\]

The difference $\operatorname{Pow}_{H}(K)-\operatorname{Pow}_{H}(BEF)$ simplifies to $-2Rr-d^{2}$, which is never zero under the intersection condition. Hence $H$ does not lie on the radical axis of $(ACD)$ and $(BEF)$.

### 2.4 Power with respect to the circle with diameter $CD$

Let $\mathcal C$ be the circle with diameter $CD$. Its centre is the midpoint of $CD$, i.e. $((d+R-r)/2,0)$, and its radius is $(d+R+r)/2$. One finds
\[
\operatorname{Pow}_{H}(\mathcal C)=
\frac{-R^{3}-R^{2}d-R^{2}r-Rd^{2}-4Rdr-Rr^{2}-d^{3}-d^{2}r-dr^{2}-r^{3}}{2(R+d+r)}.
\]

Again, $\operatorname{Pow}_{H}(\mathcal C)\neq\operatorname{Pow}_{H}(BEF)$; their difference is $-(R^{2}+2Rr+d^{2}+r^{2})/2$.

## 3. Relation to the rational certificate $\rho^{2}$

In [{43tk}] it was shown that
\[
R_{BEF}^{2}= \frac{Rr(R-r)^{2}}{d^{2}-(R-r)^{2}}=\rho^{2}(d,r,R).
\]

Since $\operatorname{Pow}_{H}(BEF)=HT^{2}=HO^{2}-R_{BEF}^{2}$, we have
\[
HO^{2}= \operatorname{Pow}_{H}(BEF)+R_{BEF}^{2}
      = \frac{Rr(R+r-d)}{R+d+r} + \frac{Rr(R-r)^{2}}{d^{2}-(R-r)^{2}}.
\]

This sum can be simplified (using a computer algebra system) to
\[
HO^{2}= \frac{Rr\bigl((R+r-d)(d^{2}-(R-r)^{2})+(R-r)^{2}(R+d+r)\bigr)}
            {(R+d+r)(d^{2}-(R-r)^{2})}.
\]

While not particularly elegant, this expression together with the formula for $\operatorname{Pow}_{H}(BEF)$ gives a complete algebraic description of the distances involved.

## 4. Geometric interpretation of $\operatorname{Pow}_{H}(BEF)$

The expression $\operatorname{Pow}_{H}(BEF)=Rr(R+r-d)/(R+d+r)$ admits a geometric interpretation. Let $s=(r+R+d)/2$ be the semiperimeter of $\triangle AMN$. Then
\[
\operatorname{Pow}_{H}(BEF)=\frac{Rr(s-d)}{s}.
\]

Recall that in $\triangle AMN$, the length of the tangent from $A$ to the incircle equals $s-d$. Thus $\operatorname{Pow}_{H}(BEF)$ is the product of the two radii $r$ and $R$, multiplied by the tangent length $s-d$, divided by the semiperimeter $s$.

This suggests a possible synthetic construction: construct a point $J$ on line $MN$ such that $HJ^{2}=Rr(s-d)/s$. If $J$ can be identified with the tangency point $T$ (or a point related to $T$), then the tangency would follow.

## 5. A synthetic proof strategy

The power relations suggest the following programme for a synthetic proof.

1. **Express $\operatorname{Pow}_{H}(BEF)$ geometrically.** Show that
   \[
   \operatorname{Pow}_{H}(BEF)=\frac{|HM|\cdot|HN|}{|MN|}\cdot (s-d),
   \]
   or a similar product of distances. The factor $|HM|\cdot|HN|/|MN|$ appears in formulas for the distance from the orthocenter to the side midpoints.

2. **Relate $\operatorname{Pow}_{H}(BEF)$ to the power of $H$ with respect to a circle that is easy to construct.** For instance, consider the circle with diameter the segment joining the projections of $H$ onto $AM$ and $AN$. Its power at $H$ might equal $Rr(s-d)/s$.

3. **Show that this circle coincides with $(BEF)$.** This would require proving that $B$, $E$, $F$ lie on that circle. Since $E$ and $F$ are defined by the intersection of line $AP$ with $\Omega$ and $\Gamma$, one could try to use the fact that $P$ is the circumcenter of $\triangle ACD$ to relate $AP$ to the power of $H$.

4. **Conclude that $HT^{2}=\operatorname{Pow}_{H}(BEF)$**, which is exactly the condition for $\ell$ to be tangent to $(BEF)$.

## 6. Connection with the orthogonal case

When the circles intersect orthogonally ($d^{2}=R^{2}+r^{2}$), the expression $\operatorname{Pow}_{H}(BEF)$ simplifies to $(R-r)^{2}/2$, which matches the simplification of $\rho^{2}$ observed in [{43tk}]. Moreover, in the orthogonal case $EF$ becomes a diameter of $(BEF)$ [{18xl}], making the geometry even more transparent. A synthetic proof for orthogonal circles might be easier and could then be extended to the general case via an inversion that maps arbitrary intersecting circles to orthogonal ones [{w83c}].

## 7. Conclusion

The power of the orthocenter $H$ with respect to the circle $(BEF)$ is given by the compact rational formula $Rr(R+r-d)/(R+d+r)$. This equals $HT^{2}$, the square of the tangent length from $H$ to $(BEF)$. The formula can be rewritten in terms of the semiperimeter of $\triangle AMN$, hinting at a synthetic interpretation involving the incircle or excircles of that triangle. While a fully synthetic proof remains to be found, the power relations presented here provide concrete algebraic targets that such a proof must explain.

## References

- [{q0i2}] Analytic proof of the theorem.
- [{43tk}] Rational identity $\rho^{2}=Rr(R-r)^{2}/(d^{2}-(R-r)^{2})$.
- [{50id}] Expression for $HT^{2}$ in terms of triangle $AMN$.
- [{18xl}] Lemma on orthogonal circles.
- [{w83c}] Inversion approach to a synthetic proof.
- [{l9ow}] Survey of approaches to the theorem.
- [{3wb1}] Correction regarding collinearity in the inverted configuration.



(reviews are hidden until publication/rejection)

reference=[q7k3]
title=The Two-Circle Tangent Theorem: A Review of Progress and Pitfalls
author=iry4
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[verify_collinearity.py]

reference=[sur7]
title=Factorization of the Tangency Condition and a Simplified Proof of the Two-Circle Theorem
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[ln1d]
title=A Synthetic Proof that Orthogonal Circles Imply a Right-Angled Triangle via Inversion
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[synthetic_right_angle.txt]

reference=[3wb1]
title=On a Collinearity Property in the Inverted Configuration of the Two-Circle Tangent Theorem
author=iry4
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[verify_collinearity.py]

reference=[fxoe]
title=Formalizing the Two-Circle Tangent Theorem in Lean: Challenges and Strategies
author=d8gk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[orthogonal_lean.lean]

reference=[k2mm]
title=The Diameter Property for Orthogonal Intersecting Circles and Its Implications for the Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[q2m2]
title=Research Report on the Two-Circle Tangent Theorem: Advances and Open Problems
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[final_report.txt]

reference=[t3x5]
title=A Simplified Analytic Proof of the Tangent Line Theorem for Orthogonal Intersecting Circles
author=d8gk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[orthogonal_proof.py]

reference=[stpy]
title=Towards a Synthetic Proof of the Two-Circle Tangent Theorem via Inversion and Orthogonal Circles
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[synthetic_outline.txt]

reference=[muh8]
title=A Characterization of the Circumcenter via a Tangent Property in a Two-Circle Configuration
author=iry4
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[verify_characterization.py]

exit_code: 0
duration_ms: 399
stdout:
```
name = "Math"
version = "0.1.0"
defaultTargets = ["math"]

[[lean_lib]]
name = "Math"

[[lean_exe]]
name = "math"
root = "Main"

```
stderr:
```
```

exit_code: 0
duration_ms: 1000
stdout:
```
total 80
drwxr-xr-x 1 agent agent 4096 Jan 10 07:48 .
drwxr-x--- 1 agent agent 4096 Jan 10 13:20 ..
drwxr-xr-x 7 agent agent 4096 Jan 10 07:10 .git
drwxr-xr-x 3 agent agent 4096 Jan 10 07:10 .github
-rw-r--r-- 1 agent agent    7 Jan 10 07:10 .gitignore
drwxr-xr-x 1 agent agent 4096 Jan 10 07:10 .lake
-rw-r--r-- 1 agent agent   68 Jan 10 07:10 Main.lean
drwxr-xr-x 1 agent agent 4096 Jan 10 07:10 Math
-rw-r--r-- 1 agent agent  143 Jan 10 07:10 Math.lean
-rw-r--r-- 1 agent agent    6 Jan 10 07:10 README.md
-rw-r--r-- 1 agent agent   93 Jan 10 07:39 TestPolyrith.lean
-rw-r--r-- 1 agent agent  257 Jan 10 07:48 factor_zero.lean
-rw-r--r-- 1 agent agent  110 Jan 10 07:10 lake-manifest.json
-rw-r--r-- 1 agent agent  128 Jan 10 07:10 lakefile.toml
-rw-r--r-- 1 agent agent   29 Jan 10 07:10 lean-toolchain
-rw-r--r-- 1 agent agent   93 Jan 10 07:37 test.lean

```
stderr:
```
```

exit_code: 1
duration_ms: 356
stdout:
```

```
stderr:
```
cat: lakefile.lean: No such file or directory
```

exit_code: 0
duration_ms: 1072
stdout:
```
trace: .> LEAN_PATH=/home/agent/Math/.lake/build/lib/lean /home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /home/agent/Math/Math/Basic.lean -o /home/agent/Math/.lake/build/lib/lean/Math/Basic.olean -i /home/agent/Math/.lake/build/lib/lean/Math/Basic.ilean -c /home/agent/Math/.lake/build/ir/Math/Basic.c --setup /home/agent/Math/.lake/build/ir/Math/Basic.setup.json --json
error: Math/Basic.lean:1:0: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/agent/Math/.lake/build/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean
error: Lean exited with code 1
Some required targets logged failures:
- Math.Basic
error: build failed

```
stderr:
```
```

exit_code: 0
duration_ms: 236
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 700
stdout:
```
-- This module serves as the root of the `Math` library.
-- Import modules here that should be built as part of the library.
import Math.Basic

```
stderr:
```
```

exit_code: 0
duration_ms: 295
stdout:
```
def hello := "world"

open Real

lemma factor_zero (R d r : ℝ) : R ^ 4 - 2 * R ^ 2 * d ^ 2 - 2 * R ^ 2 * r ^ 2
    + ((d ^ 2 - (R - r) ^ 2) * ((R + r) ^ 2 - d ^ 2)) + d ^ 4 - 2 * d ^ 2 * r ^ 2 + r ^ 4 = 0 := by
  ring

```
stderr:
```
```

exit_code: 0
duration_ms: 2996
stdout:
```
error: Math/Basic.lean:5:0: unexpected identifier; expected command
error: Lean exited with code 1
Some required targets logged failures:
- Math.Basic
error: build failed

```
stderr:
```
```

exit_code: 0
duration_ms: 901
stdout:
```
r=0.579, R=0.931, d=0.820
  nine-point center = (0.498210, -0.220381)
  H = (0.586420, -0.201397)
  distance from nine_center to line through H parallel to AP = 8.894822e-02
  nine_center.x - m = -8.821034e-02
  distance from nine_center to line AP = 8.894822e-02

r=0.662, R=3.375, d=2.789
  nine-point center = (2.072628, -0.222172)
  H = (2.750997, -0.137386)
  distance from nine_center to line through H parallel to AP = 2.917118e-01
  nine_center.x - m = -6.783692e-01
  distance from nine_center to line AP = 2.917118e-01

r=1.304, R=2.368, d=3.256
  nine-point center = (1.894051, -1.665176)
  H = (2.159895, -0.376901)
  distance from nine_center to line through H parallel to AP = 4.656185e-01
  nine_center.x - m = -2.658433e-01
  distance from nine_center to line AP = 4.656185e-01


```
stderr:
```
```

exit_code: 0
duration_ms: 720
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 3684
stdout:
```
Product of powers:
((4*R**2 - (-R + d + r)**2)*(d**2 - (R - r)**2)*(d**2 - (R + r)**2) + (-R + d + r)**2*(R - d + r)**2*(R + d - r)**2)*((d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(4*r**2 - (R + d - r)**2) + (-R + d + r)**2*(R - d + r)**2*(R + d - r)**2)/(16*(d**2 - (R - r)**2)**2*(d**2 - (R + r)**2)**2)

HT^2:
R*r*(R - d + r)/(R + d + r)

Ratio product/d^2:
((4*R**2 - (-R + d + r)**2)*(d**2 - (R - r)**2)*(d**2 - (R + r)**2) + (-R + d + r)**2*(R - d + r)**2*(R + d - r)**2)*((d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(4*r**2 - (R + d - r)**2) + (-R + d + r)**2*(R - d + r)**2*(R + d - r)**2)/(16*d**2*(d**2 - (R - r)**2)**2*(d**2 - (R + r)**2)**2)

Difference ratio - HT^2:
(-R**5*d - 2*R**4*d**2 + R**4*r**2 - R**3*d**3 - 2*R**3*d**2*r + 3*R**3*d*r**2 + 2*R**3*r**3 + R**2*d**2*r**2 + 3*R**2*d*r**3 + R**2*r**4 + 2*R*d**4*r - 2*R*d**2*r**3 - d**3*r**3 - 2*d**2*r**4 - d*r**5)/(d**2*(R**2 + 2*R*d + 2*R*r + d**2 + 2*d*r + r**2))

Numerical test with r=1, R=2, d=2.5:
product/d^2 = -1.15834710743802
HT^2 = 0.181818181818182
diff = -1.34016528925620

```
stderr:
```
```

exit_code: 0
duration_ms: 784
stdout:
```
Requirement already satisfied: sympy in ./.venv/lib/python3.12/site-packages (1.14.0)
Requirement already satisfied: mpmath<1.4,>=1.1.0 in ./.venv/lib/python3.12/site-packages (from sympy) (1.3.0)

```
stderr:
```
```

exit_code: 1
duration_ms: 237
stdout:
```
Traceback (most recent call last):
  File "/home/agent/symbolic_check.py", line 1, in 
    import sympy as sp
ModuleNotFoundError: No module named 'sympy'

```
stderr:
```
```

exit_code: 0
duration_ms: 421
stdout:
```

```
stderr:
```
```

Review submitted for publication [q7k3].

reference=[q7k3]
title=The Two-Circle Tangent Theorem: A Review of Progress and Pitfalls
author=iry4
reviews:ACCEPT, ACCEPT, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[verify_collinearity.py]
abstract = We review the research on the two-circle tangent theorem, summarizing established results (analytic proof, rational identity, converse theorem, orthogonal-case lemmas) and highlighting pitfalls in synthetic proof attempts, including a false collinearity assumption in inversion approaches. We outline open problems and future directions.

We review the research conducted on a geometric theorem involving two intersecting circles and a tangent line property. The theorem has been fully proved analytically, and several related results have been established: a rational identity, a converse characterization, an orthogonal‑circles lemma, and inversion‑based reduction strategies. However, attempts at a synthetic proof have encountered subtle pitfalls, including a mistaken collinearity assumption in the inverted configuration. We summarize the current state of knowledge, highlight the unresolved challenges, and suggest promising avenues for future work.

## 1. The Theorem

Let $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r The line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.

## 2. Established Results

### 2.1 Analytic Proof [{q0i2}]
A coordinate proof places $M=(0,0)$, $N=(d,0)$ and derives explicit formulas for all points. The tangency condition reduces to a polynomial identity that simplifies to zero under the intersection conditions $|R-r|

reference=[q7k3]
title=The Two-Circle Tangent Theorem: A Review of Progress and Pitfalls
author=iry4
reviews:ACCEPT, ACCEPT, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[verify_collinearity.py]

exit_code: 0
duration_ms: 369
stdout:
```
r=0.579, R=0.931, d=0.820
  pow_Ω=0.049735, pow_Γ=-0.772361, product=-0.038413
  alt_Ω=-0.049735, alt_Γ=0.772361, product=-0.038413
  HT²=0.159563
  alt_product/d²=-0.057129, diff=-2.17e-01
  pow_Ω+pow_Γ=-0.722626

r=0.662, R=3.375, d=2.789
  pow_Ω=7.149210, pow_Γ=-11.370525, product=-81.290279
  alt_Ω=-7.149210, alt_Γ=11.370525, product=-81.290279
  HT²=0.408288
  alt_product/d²=-10.454227, diff=-1.09e+01
  pow_Ω+pow_Γ=-4.221315

r=1.304, R=2.368, d=3.256
  pow_Ω=3.105993, pow_Γ=-4.261478, product=-13.236121
  alt_Ω=-3.105993, alt_Γ=4.261478, product=-13.236121
  HT²=0.185227
  alt_product/d²=-1.248191, diff=-1.43e+00
  pow_Ω+pow_Γ=-1.155485


```
stderr:
```
```

exit_code: 0
duration_ms: 459
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 344
stdout:
```
r=0.579, R=0.931, d=0.820
  pow_Ω=0.049735, pow_Γ=-0.772361, |product|=0.038413
  |product|/d²=0.057129, HT²=0.159563, diff=-1.02e-01
  product = -0.038413, -HT2*d² = -0.107290, diff=6.89e-02

r=0.662, R=3.375, d=2.789
  pow_Ω=7.149210, pow_Γ=-11.370525, |product|=81.290279
  |product|/d²=10.454227, HT²=0.408288, diff=1.00e+01
  product = -81.290279, -HT2*d² = -3.174780, diff=-7.81e+01

r=1.304, R=2.368, d=3.256
  pow_Ω=3.105993, pow_Γ=-4.261478, |product|=13.236121
  |product|/d²=1.248191, HT²=0.185227, diff=1.06e+00
  product = -13.236121, -HT2*d² = -1.964198, diff=-1.13e+01


```
stderr:
```
```

exit_code: 0
duration_ms: 543
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 598
stdout:
```
r=0.579, R=0.931, d=0.820
  pow_Ω=0.049735, pow_Γ=-0.772361, product=-0.038413
  product/d²=-0.057129, HT²=0.159563, diff=-2.17e-01
  pow_H(BEF)=0.159563, HT²=0.159563, diff=-1.94e-16

r=0.662, R=3.375, d=2.789
  pow_Ω=7.149210, pow_Γ=-11.370525, product=-81.290279
  product/d²=-10.454227, HT²=0.408288, diff=-1.09e+01
  pow_H(BEF)=0.408288, HT²=0.408288, diff=-2.93e-14

r=1.304, R=2.368, d=3.256
  pow_Ω=3.105993, pow_Γ=-4.261478, product=-13.236121
  product/d²=-1.248191, HT²=0.185227, diff=-1.43e+00
  pow_H(BEF)=0.185227, HT²=0.185227, diff=1.28e-15

r=0.739, R=1.817, d=1.570
  pow_Ω=1.284290, pow_Γ=-3.164504, product=-4.064140
  product/d²=-1.648269, HT²=0.321296, diff=-1.97e+00
  pow_H(BEF)=0.321296, HT²=0.321296, diff=-7.77e-16

r=0.868, R=0.973, d=0.855
  pow_Ω=-0.457091, pow_Γ=-0.739636, product=0.338081
  product/d²=0.462952, HT²=0.308715, diff=1.54e-01
  pow_H(BEF)=0.308715, HT²=0.308715, diff=5.55e-17


```
stderr:
```
```

exit_code: 0
duration_ms: 211
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 438
stdout:
```
r=0.579, R=0.931, d=0.820
  angle AHC = 47.25°
  angle EHF = 47.78°
  angle EBF = 60.55°
  diff AHC - EHF = 0.53°

r=0.662, R=3.375, d=2.789
  angle AHC = 5.81°
  angle EHF = 153.76°
  angle EBF = 24.83°
  diff AHC - EHF = 147.95°

r=1.304, R=2.368, d=3.256
  angle AHC = 39.97°
  angle EHF = 50.48°
  angle EBF = 122.26°
  diff AHC - EHF = 10.51°

r=0.739, R=1.817, d=1.570
  angle AHC = 27.86°
  angle EHF = 105.54°
  angle EBF = 59.01°
  diff AHC - EHF = 77.68°

r=0.868, R=0.973, d=0.855
  angle AHC = 70.40°
  angle EHF = 1.71°
  angle EBF = 54.98°
  diff AHC - EHF = 68.70°


```
stderr:
```
```

exit_code: 0
duration_ms: 273
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 334
stdout:
```
r=0.579, R=0.931, d=0.820
  HM=0.620, HN=0.308, HM*HN/d=0.233
  pow_BEF=0.159563
  HA=0.922, HC=1.182, HA*HC=1.090
  (HM*HN/d)*(s-d)=0.080449, diff=-7.91e-02
  pow_BEF/(HA*HC)=0.146408

r=0.662, R=3.375, d=2.789
  HM=2.754, HN=0.142, HM*HN/d=0.141
  pow_BEF=0.408288
  HA=3.354, HC=3.415, HA*HC=11.456
  (HM*HN/d)*(s-d)=0.087786, diff=-3.21e-01
  pow_BEF/(HA*HC)=0.035640

r=1.304, R=2.368, d=3.256
  HM=2.193, HN=1.159, HM*HN/d=0.781
  pow_BEF=0.185227
  HA=1.634, HC=3.485, HA*HC=5.693
  (HM*HN/d)*(s-d)=0.162211, diff=-2.30e-02
  pow_BEF/(HA*HC)=0.032535


```
stderr:
```
```

exit_code: 0
duration_ms: 298
stdout:
```

```
stderr:
```
```

Review submitted for publication [x2a1].

reference=[x2a1]
title=Power of a Point and Radical Axis Relations in the Two-Circle Tangent Theorem
author=pz42
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We compute the powers of the orthocenter H with respect to the various circles appearing in the two-circle tangent theorem. We discover identities linking these powers to the squared distance HT² and to the rational certificate ρ². These relations suggest a synthetic proof strategy based on radical axes and power of a point.

## Introduction

The tangent line theorem for two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r0$, $00.
\]
The points $C=(-r,0)$, $D=(d+R,0)$, $P$ is the circumcenter of $\triangle ACD$, $E$ and $F$ are the second intersections of line $AP$ with $\Omega$ and $\Gamma$, and $H$ is the orthocenter of $\triangle PMN$.

Define $T=R+r-d$ (positive under the intersection condition). Then
\[
E=A+\frac{T}{R}(P-A),\qquad F=A+\frac{T}{r}(P-A).
\]

## 2. Powers of $H$ with respect to the circles

Using the explicit formulas for $H$ we compute the following powers.

### 2.1 Power with respect to $\Omega$ and $\Gamma$

\[
\operatorname{Pow}_{H}(\Omega)=H_x^{2}+H_y^{2}-r^{2}
      =\frac{R^{2}d+Rd^{2}-Rdr-Rr^{2}-dr^{2}-r^{3}}{R+d+r},
\]
\[
\operatorname{Pow}_{H}(\Gamma)=(H_x-d)^{2}+H_y^{2}-R^{2}
      =\frac{-R^{3}-R^{2}d-R^{2}r-Rdr+d^{2}r+dr^{2}}{R+d+r}.
\]

Their difference simplifies to
\[
\operatorname{Pow}_{H}(\Omega)-\operatorname{Pow}_{H}(\Gamma)=R^{2}+Rd-dr-r^{2}.
\]

The radical axis of $\Omega$ and $\Gamma$ is the line $AB$ (the line $x=x_0$). Since $H_x=(d+R-r)/2$, the quantity $H_x-x_0$ equals the difference above divided by $2d$; consequently $H$ does **not** lie on $AB$ unless $R^{2}+Rd-dr-r^{2}=0$, which is a special relation between $d,r,R$.

### 2.2 Power with respect to $(BEF)$

Let $O$ be the circumcenter of $\triangle BEF$ and $R_{BEF}$ its radius. Then
\[
\operatorname{Pow}_{H}(BEF)=HO^{2}-R_{BEF}^{2}.
\]

A direct computation yields the surprisingly simple expression
\[
\boxed{\;\operatorname{Pow}_{H}(BEF)=\frac{Rr(R+r-d)}{R+d+r}\;}.
\]

This is exactly the quantity $HT^{2}$ found in [{50id}], where $T$ is the tangency point of $\ell$ with $(BEF)$. Indeed, if $\ell$ is tangent to $(BEF)$ at $T$, then $HT^{2}=\operatorname{Pow}_{H}(BEF)$ (the power of $H$ equals the square of the tangent length). Thus the tangency condition is equivalent to
\[
HO^{2}-R_{BEF}^{2}=HT^{2},
\]
which is automatically true because $HT^{2}$ is defined as $HO^{2}-R_{BEF}^{2}$. The non‑trivial part of the theorem is that this power coincides with the rational expression above.

### 2.3 Power with respect to $(ACD)$

Denote by $K$ the circumcircle of $\triangle ACD$. Then
\[
\operatorname{Pow}_{H}(K)=\frac{-R^{2}r-Rd^{2}-3Rdr-Rr^{2}-d^{3}-d^{2}r}{R+d+r}.
\]

The difference $\operatorname{Pow}_{H}(K)-\operatorname{Pow}_{H}(BEF)$ simplifies to $-2Rr-d^{2}$, which is never zero under the intersection condition. Hence $H$ does not lie on the radical axis of $(ACD)$ and $(BEF)$.

### 2.4 Power with respect to the circle with diameter $CD$

Let $\mathcal C$ be the circle with diameter $CD$. Its centre is the midpoint of $CD$, i.e. $((d+R-r)/2,0)$, and its radius is $(d+R+r)/2$. One finds
\[
\operatorname{Pow}_{H}(\mathcal C)=
\frac{-R^{3}-R^{2}d-R^{2}r-Rd^{2}-4Rdr-Rr^{2}-d^{3}-d^{2}r-dr^{2}-r^{3}}{2(R+d+r)}.
\]

Again, $\operatorname{Pow}_{H}(\mathcal C)\neq\operatorname{Pow}_{H}(BEF)$; their difference is $-(R^{2}+2Rr+d^{2}+r^{2})/2$.

## 3. Relation to the rational certificate $\rho^{2}$

In [{43tk}] it was shown that
\[
R_{BEF}^{2}= \frac{Rr(R-r)^{2}}{d^{2}-(R-r)^{2}}=\rho^{2}(d,r,R).
\]

Since $\operatorname{Pow}_{H}(BEF)=HT^{2}=HO^{2}-R_{BEF}^{2}$, we have
\[
HO^{2}= \operatorname{Pow}_{H}(BEF)+R_{BEF}^{2}
      = \frac{Rr(R+r-d)}{R+d+r} + \frac{Rr(R-r)^{2}}{d^{2}-(R-r)^{2}}.
\]

This sum can be simplified (using a computer algebra system) to
\[
HO^{2}= \frac{Rr\bigl((R+r-d)(d^{2}-(R-r)^{2})+(R-r)^{2}(R+d+r)\bigr)}
            {(R+d+r)(d^{2}-(R-r)^{2})}.
\]

While not particularly elegant, this expression together with the formula for $\operatorname{Pow}_{H}(BEF)$ gives a complete algebraic description of the distances involved.

## 4. Geometric interpretation of $\operatorname{Pow}_{H}(BEF)$

The expression $\operatorname{Pow}_{H}(BEF)=Rr(R+r-d)/(R+d+r)$ admits a geometric interpretation. Let $s=(r+R+d)/2$ be the semiperimeter of $\triangle AMN$. Then
\[
\operatorname{Pow}_{H}(BEF)=\frac{Rr(s-d)}{s}.
\]

Recall that in $\triangle AMN$, the length of the tangent from $A$ to the incircle equals $s-d$. Thus $\operatorname{Pow}_{H}(BEF)$ is the product of the two radii $r$ and $R$, multiplied by the tangent length $s-d$, divided by the semiperimeter $s$.

This suggests a possible synthetic construction: construct a point $J$ on line $MN$ such that $HJ^{2}=Rr(s-d)/s$. If $J$ can be identified with the tangency point $T$ (or a point related to $T$), then the tangency would follow.

## 5. A synthetic proof strategy

The power relations suggest the following programme for a synthetic proof.

1. **Express $\operatorname{Pow}_{H}(BEF)$ geometrically.** Show that
   \[
   \operatorname{Pow}_{H}(BEF)=\frac{|HM|\cdot|HN|}{|MN|}\cdot (s-d),
   \]
   or a similar product of distances. The factor $|HM|\cdot|HN|/|MN|$ appears in formulas for the distance from the orthocenter to the side midpoints.

2. **Relate $\operatorname{Pow}_{H}(BEF)$ to the power of $H$ with respect to a circle that is easy to construct.** For instance, consider the circle with diameter the segment joining the projections of $H$ onto $AM$ and $AN$. Its power at $H$ might equal $Rr(s-d)/s$.

3. **Show that this circle coincides with $(BEF)$.** This would require proving that $B$, $E$, $F$ lie on that circle. Since $E$ and $F$ are defined by the intersection of line $AP$ with $\Omega$ and $\Gamma$, one could try to use the fact that $P$ is the circumcenter of $\triangle ACD$ to relate $AP$ to the power of $H$.

4. **Conclude that $HT^{2}=\operatorname{Pow}_{H}(BEF)$**, which is exactly the condition for $\ell$ to be tangent to $(BEF)$.

## 6. Connection with the orthogonal case

When the circles intersect orthogonally ($d^{2}=R^{2}+r^{2}$), the expression $\operatorname{Pow}_{H}(BEF)$ simplifies to $(R-r)^{2}/2$, which matches the simplification of $\rho^{2}$ observed in [{43tk}]. Moreover, in the orthogonal case $EF$ becomes a diameter of $(BEF)$ [{18xl}], making the geometry even more transparent. A synthetic proof for orthogonal circles might be easier and could then be extended to the general case via an inversion that maps arbitrary intersecting circles to orthogonal ones [{w83c}].

## 7. Conclusion

The power of the orthocenter $H$ with respect to the circle $(BEF)$ is given by the compact rational formula $Rr(R+r-d)/(R+d+r)$. This equals $HT^{2}$, the square of the tangent length from $H$ to $(BEF)$. The formula can be rewritten in terms of the semiperimeter of $\triangle AMN$, hinting at a synthetic interpretation involving the incircle or excircles of that triangle. While a fully synthetic proof remains to be found, the power relations presented here provide concrete algebraic targets that such a proof must explain.

## References

- [{q0i2}] Analytic proof of the theorem.
- [{43tk}] Rational identity $\rho^{2}=Rr(R-r)^{2}/(d^{2}-(R-r)^{2})$.
- [{50id}] Expression for $HT^{2}$ in terms of triangle $AMN$.
- [{18xl}] Lemma on orthogonal circles.
- [{w83c}] Inversion approach to a synthetic proof.
- [{l9ow}] Survey of approaches to the theorem.
- [{3wb1}] Correction regarding collinearity in the inverted configuration.



(reviews are hidden until publication/rejection)

Publication submitted.

(0 found)

Review submitted for publication [ln1d].

reference=[ln1d]
title=A Synthetic Proof that Orthogonal Circles Imply a Right-Angled Triangle via Inversion
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[synthetic_right_angle.txt]
abstract = We give a short synthetic proof that when two circles intersect orthogonally, triangle BEF in the configuration of the tangent line theorem is right-angled at B. The proof uses inversion to transform the circles into perpendicular lines, preserving angles.

Title: A Synthetic Proof that Orthogonal Circles Imply a Right-Angled Triangle via Inversion

Abstract: We give a short synthetic proof that when two circles intersect orthogonally, triangle BEF in the configuration of the tangent line theorem is right-angled at B. The proof uses inversion to transform the circles into perpendicular lines, preserving angles.

1. Introduction

In the configuration of the two-circle tangent theorem, let Ω (centre M, radius r) and Γ (centre N, radius R) intersect at A and B. Define C, D, P, E, F as usual. It has been observed that when the circles intersect orthogonally (d² = r² + R²), triangle BEF is right-angled at B [k2mm]. This fact was proved algebraically. We present a purely synthetic proof using inversion.

2. Inversion Setup

Perform an inversion I with centre A and arbitrary radius. Since Ω and Γ pass through A, their images are lines ω' = I(Ω) and γ' = I(Γ). The inversion preserves angles; therefore, because Ω and Γ are orthogonal at A, the lines ω' and γ' are perpendicular.

The points B, E, F invert to B' = ω' ∩ γ', E' = ω' ∩ AP, and F' = γ' ∩ AP. (The line AP passes through the inversion centre and is thus invariant as a set.)

3. Right Angle in the Inverted Configuration

In the inverted plane, triangle B'E'F' has vertex B' at the intersection of the two perpendicular lines ω' and γ', while E' lies on ω' and F' lies on γ'. Consequently, angle E'B'F' is the angle between ω' and γ', which is 90°.

4. Preservation of Angles under Inversion

Inversion is conformal: it preserves the magnitude of angles (though it reverses orientation). Hence the angle at B in triangle BEF equals the angle at B' in triangle B'E'F'. Therefore ∠EBF = ∠E'B'F' = 90°.

5. Conclusion

Thus triangle BEF is right-angled at B whenever the original circles intersect orthogonally. This gives a synthetic explanation for the algebraic simplification observed in the orthogonal case and provides an alternative proof of the lemma that the circumcenter of triangle BEF is the midpoint of EF (since in a right triangle the circumcenter is the midpoint of the hypotenuse).

6. Remarks

The proof illustrates the power of inversion in converting a property of circles (orthogonality) into a property of lines (perpendicularity). Combined with the known inversion approach to the original theorem [b6nr, w83c], this may lead to a complete synthetic proof of the tangent line theorem.

References

[k2mm] The diameter property for orthogonal intersecting circles.
[18xl] Lemma on the circumcenter of triangle BEF for orthogonal circles.
[b6nr] Inversion analysis of the tangent theorem.
[w83c] Synthetic approach via inversion.

(reviews are hidden until publication/rejection)

reference=[ln1d]
title=A Synthetic Proof that Orthogonal Circles Imply a Right-Angled Triangle via Inversion
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[synthetic_right_angle.txt]

Review submitted for publication [3wb1].

reference=[3wb1]
title=On a Collinearity Property in the Inverted Configuration of the Two-Circle Tangent Theorem
author=iry4
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[verify_collinearity.py]
abstract = We present numerical evidence that points A, H', Q' are not collinear in the inverted configuration, challenging an assumption in some synthetic proof outlines. The observation highlights a subtlety in the geometry and calls for a revision of inversion-based approaches.

Several inversion‑based approaches to the two‑circle tangent theorem assume or suggest that the points $A$, $H'$, $Q'$ are collinear, where $A$ is an intersection point of the original circles, $H'$ is the image of the orthocenter $H$, and $Q'$ is the second intersection of line $AP$ with the circle $\Sigma = \mathcal I(MN)$. We present numerical evidence that this collinearity does **not** hold in general, indicating that a synthetic proof relying on this alignment may need adjustment. We also compute the pole $S$ of line $AP$ with respect to $\Sigma$ and find that $A$, $H'$, $S$ are not collinear either. The observation highlights a subtlety in the geometry of the inverted configuration and calls for a more careful analysis of the polar properties involved.

## 1. Introduction

Inversion with centre $A$ transforms the original two‑circle configuration into a simpler one where the circles become lines $\omega'$, $\gamma'$ and the line of centres $MN$ becomes a circle $\Sigma$ through $A$. Let $H' = \mathcal I(H)$ and let $Q'$ be the second intersection of line $AP$ with $\Sigma$ (the image of the intersection point $X = AP\cap MN$). Some synthetic outlines (e.g. [{w83c}]) implicitly assume that $A$, $H'$, $Q'$ are collinear, a property that would simplify the power‑of‑a‑point argument leading to the tangency condition.

We test this collinearity by evaluating the determinant of vectors $\overrightarrow{AH'}$ and $\overrightarrow{AQ'}$ for random admissible parameters. The determinant is consistently non‑zero, indicating that the three points are not aligned. We also compute the pole $S$ of $AP$ with respect to $\Sigma$ and check whether $A$, $H'$, $S$ are collinear; they are not. Therefore the geometric reasoning that relies on such collinearity requires revision.

## 2. Numerical Experiment

We generated random triples $(d,r,R)$ satisfying the intersection condition $|R-r|

reference=[3wb1]
title=On a Collinearity Property in the Inverted Configuration of the Two-Circle Tangent Theorem
author=iry4
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[verify_collinearity.py]

exit_code: 0
duration_ms: 183
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 254
stdout:
```
/-
A Lean formalization of the orthogonal case of the two‑circle tangent theorem.
This file is a sketch; the proofs are omitted because they require heavy
algebraic manipulation that is currently easiest to do with a computer algebra
system. The definitions follow the analytic formulas derived in [t3x5].
-/

import Mathlib.Data.Real.Basic
open Real

variable (r R : ℝ) (hr : r > 0) (hR : R > 0)

-- Orthogonal condition: d^2 = r^2 + R^2
def d : ℝ := Real.sqrt (r^2 + R^2)

lemma d_sq : d r R ^ 2 = r ^ 2 + R ^ 2 := by
  exact Real.sq_sqrt (by positivity)

-- Intersection point A = (x0, y0)
def x0 : ℝ := r ^ 2 / d r R
def y0 : ℝ := r * R / d r R

lemma y0_sq : y0 r R ^ 2 = r ^ 2 - x0 r R ^ 2 := by
  dsimp [y0, x0]
  field_simp [d]
  ring

-- Points
def M : ℝ × ℝ := (0, 0)
def N : ℝ × ℝ := (d r R, 0)
def C : ℝ × ℝ := (-r, 0)
def D : ℝ × ℝ := (d r R + R, 0)
def A : ℝ × ℝ := (x0 r R, y0 r R)
def B : ℝ × ℝ := (x0 r R, -y0 r R)

-- Circumcenter P of triangle A C D
def Px : ℝ := (d r R + R - r) / 2
def Py : ℝ := -(d r R + R + r) / 2
def P : ℝ × ℝ := (Px r R, Py r R)

-- Direction vector of line AP
def v : ℝ × ℝ := (Px r R - x0 r R, Py r R - y0 r R)

-- Second intersections E, F (formulas from the analytic proof)
def tE : ℝ := (R + r - d r R) / R
def tF : ℝ := (R + r - d r R) / r

def E : ℝ × ℝ :=
  let t := tE r R
  (x0 r R + t * (Px r R - x0 r R), y0 r R + t * (Py r R - y0 r R))

def F : ℝ × ℝ :=
  let t := tF r R
  (x0 r R + t * (Px r R - x0 r R), y0 r R + t * (Py r R - y0 r R))

-- Orthocenter H of triangle P M N
def Hx : ℝ := Px r R
def Hy : ℝ := - (R * r) / (R + r + d r R)
def H : ℝ × ℝ := (Hx r R, Hy r R)

-- Circumcenter O of triangle B E F
def Ox : ℝ := d r R / 2
def Oy : ℝ := - d r R / 2
def O : ℝ × ℝ := (Ox r R, Oy r R)

-- Radius squared of circumcircle of B E F
def radius_sq : ℝ := (Ox r R - x0 r R)^2 + (Oy r R + y0 r R)^2

-- Distance squared from O to the line through H parallel to AP
def cross : ℝ :=
  (Ox r R - Hx r R) * (Py r R - y0 r R) - (Oy r R - Hy r R) * (Px r R - x0 r R)

def dist_sq : ℝ := cross r R ^ 2 / ((Px r R - x0 r R)^2 + (Py r R - y0 r R)^2)

-- The theorem
theorem orthogonal_tangency : dist_sq r R = radius_sq r R := by
  sorry

```
stderr:
```
```

exit_code: 0
duration_ms: 242
stdout:
```
total 12
drwxr-xr-x 2 agent agent 4096 Jan 10 13:00 .
drwxr-xr-x 4 agent agent 4096 Jan 10 13:00 ..
-rw-r--r-- 1 agent agent 2278 Jan 10 13:00 orthogonal_lean.lean

```
stderr:
```
```

Attachment downloaded to /home/agent/publications/fxoe.

(0 found)

Review submitted for publication [muzv].

reference=[muzv]
title=A Radical Axis Approach to the Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We outline a synthetic proof strategy based on radical axes and power of points. We show that the tangency condition is equivalent to a relation among the powers of H with respect to three circles: Ω, Γ, and the circle with diameter CD.

## Introduction

The theorem about two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r

Review submitted for publication [fxoe].

reference=[fxoe]
title=Formalizing the Two-Circle Tangent Theorem in Lean: Challenges and Strategies
author=d8gk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[orthogonal_lean.lean]
abstract = We discuss the challenges of formalizing the two-circle tangent theorem in the Lean theorem prover, focusing on algebraic complexity, square-root elimination, and geometric side conditions. We propose strategies to overcome these difficulties and illustrate them with a sketch of the orthogonal case.

# Formalizing the Two‑Circle Tangent Theorem in Lean: Challenges and Strategies

## Abstract

The geometric theorem about two intersecting circles and a tangent line has been proved analytically using coordinate geometry and computer algebra. We discuss the challenges of formalizing this proof in the Lean theorem prover and propose strategies to overcome them. The main difficulties are: (1) managing complex algebraic expressions, (2) verifying polynomial identities that involve square roots, (3) handling geometric constraints (intersection conditions, ordering of points). We illustrate the approach by sketching the formalization of the special case of orthogonal intersecting circles, where the algebra simplifies dramatically. The orthogonal case serves as a stepping stone toward a full formalization and highlights the potential of Lean’s `ring` and `field_simp` tactics for geometric proofs.

## 1. Introduction

The theorem under consideration is a classic result in Euclidean geometry. Its analytic proof reduces the statement to a polynomial identity that can be verified by a computer algebra system. Formal verification in a proof assistant such as Lean provides an additional level of certainty and can reveal hidden assumptions.

Lean, with its `mathlib` library, offers extensive support for Euclidean geometry (points, vectors, circles) and real algebraic manipulation. However, the proof involves heavy rational expressions and square roots that arise from solving circle equations. We outline the obstacles and suggest tactics to tackle them.

## 2. The theorem and its analytic proof

We recall the configuration: circles $\Omega$ (center $M$, radius $r$) and $\Gamma$ (center $N$, radius $R>r$) intersect at $A$ and $B$. Let $C$, $D$, $P$, $E$, $F$, $H$, $O$ be defined as usual. The theorem states that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.

The analytic proof (see [{q0i2}]) places $M=(0,0)$, $N=(d,0)$, derives explicit formulas for all points, and shows that the squared distance from $O$ to the line equals $R_{BEF}^2$, where
\[
R_{BEF}^2 = \frac{R\,r\,(R-r)^2}{d^2-(R-r)^2}.
\tag{1}
\]

The verification reduces to an identity between rational functions of $d,r,R,x_0,y_0$ with the algebraic relations $y_0^2 = r^2-x_0^2$ and $2dx_0 = d^2-R^2+r^2$.

## 3. Challenges for formalization

### 3.1. Managing algebraic complexity

The expressions for $P$, $E$, $F$, $O$, $H$ are rational functions with denominators that are non‑zero under the intersection condition. In Lean, one must keep track of these non‑zero assumptions and use `field_simp` to clear denominators. The final identity, after clearing denominators, is a polynomial in $d,r,R,x_0,y_0$ of high degree. Simplifying it directly with `ring` may be computationally expensive.

### 3.2. Square‑root elimination

The coordinate $y_0$ is defined as $\sqrt{r^2-x_0^2}$. The proof uses the relation $y_0^2 = r^2-x_0^2$ but never needs the explicit square root. In Lean one can avoid introducing `Real.sqrt` by working with $y_0$ as a variable satisfying $y_0^2 = r^2-x_0^2$. This approach keeps the polynomial ideal and allows using `ring` and `polyrith` (if available) to verify identities modulo the relation.

### 3.3. Geometric side conditions

The configuration requires several inequalities: $00$, and the order $C,M,N,D$ on the $x$-axis. These inequalities are needed to ensure that the constructed points are distinct and that the circles intersect in two points. In a formal proof they must be stated as hypotheses and used where necessary (e.g., to guarantee that denominators are non‑zero).

### 3.4. Real arithmetic vs. symbolic computation

Lean’s `ring` tactic works over commutative rings, but the coefficients are real numbers. The identity to be proved is an equality of real expressions. One can treat $d,r,R,x_0,y_0$ as indeterminates and prove the identity in the polynomial ring $\mathbb{Q}[d,r,R,x_0,y_0]$ modulo the ideal generated by $y_0^2-(r^2-x_0^2)$ and $2dx_0-(d^2-R^2+r^2)$. This is essentially what the computer‑algebra verification does. In Lean one could use `polyrith` (if the polynomial is not too large) or break the identity into smaller lemmas.

## 4. The orthogonal case as a test‑bed

When the circles intersect orthogonally ($d^2=r^2+R^2$), the formulas simplify considerably. As shown in [{t3x5}], we have:
- $O = (d/2,\,-d/2)$,
- $R_{BEF}^2 = (R-r)^2/2$,
- $H = \bigl((d+R-r)/2,\; -Rr/(R+r+d)\bigr)$.

The tangency condition becomes a polynomial identity that factors nicely. This case is ideal for a first formalization attempt because:

1. The square‑root relation $y_0^2=r^2-x_0^2$ can be replaced by the explicit rational expressions $x_0=r^2/d$, $y_0=rR/d$.
2. The final identity is of low degree and can be handled by `ring` easily.
3. The orthogonal condition $d^2=r^2+R^2$ is a simple polynomial relation.

We have written a Lean script that defines the points, states the tangency condition, and outlines the proof (see attached `orthogonal_lean.lean`). The script uses the formulas derived in [{t3x5}] and leaves the algebraic verification as `sorry` because the required algebraic manipulation is still heavy. However, the structure shows how the formalization would proceed.

## 5. Strategies for the general case

For the general case we propose a stepwise strategy:

1. **Work in the polynomial ring.** Introduce variables $d,r,R,x,y$ and the relations $y^2 = r^2-x^2$, $2dx = d^2-R^2+r^2$. Prove the identity as a polynomial equality modulo these relations. This avoids square roots and keeps the algebra purely symbolic.

2. **Use `polyrith` if possible.** The `polyrith` tactic can solve polynomial equalities by calling an external Gröbner basis engine. If the polynomial is too large, break it into smaller pieces.

3. **Employ the `rationalize` tactic.** To eliminate square roots, one can square both sides of an equality and then use `ring`. This is safe because all quantities involved are real and the signs are known from geometric constraints.

4. **Factor the verification.** The analytic proof can be structured as a chain of lemmas, each verified separately. For example, first prove that $O_x = d/2$, then compute $O_y$, then compute $H$, then compute the distance squared, etc.

5. **Leverage symmetry.** The configuration is symmetric with respect to the $x$-axis. This symmetry can be used to reduce the number of cases and to simplify expressions.

## 6. Related work in mathlib

Mathlib contains a growing collection of Euclidean geometry theorems, including the nine‑point circle, the radical axis, and properties of the orthocenter. However, there is no pre‑existing formalization of the specific two‑circle tangent theorem. The available tactics (`ring`, `field_simp`, `polyrith`, `positivity`) are sufficient for the algebraic part, but the geometric setup (defining the points and stating the hypotheses) requires careful bookkeeping.

## 7. Conclusion

Formalizing the two‑circle tangent theorem in Lean is challenging due to the heavy algebraic manipulation involved. However, the orthogonal case shows that with careful handling of the relations and use of Lean’s simplification tactics, the proof can be carried out. The general case requires a systematic approach to polynomial identity verification, possibly using `polyrith` or a custom tactic that mimics the computer‑algebra computation.

A successful formalization would not only increase confidence in the theorem but also demonstrate Lean’s capability to handle non‑trivial Euclidean geometry problems that blend synthetic ideas with algebraic computation.

## References

- [{q0i2}] Analytic proof of the theorem.
- [{t3x5}] Simplified proof for orthogonal intersecting circles.
- [{43tk}] Rational identity underlying the theorem.
- [{18xl}] Lemma on orthogonal circles.

## Attachments

- `orthogonal_lean.lean`: Lean script sketching the formalization of the orthogonal case.

(reviews are hidden until publication/rejection)

Review submitted for publication [k2mm].

reference=[k2mm]
title=The Diameter Property for Orthogonal Intersecting Circles and Its Implications for the Tangent Theorem
author=pz42
reviews:PENDING, PENDING, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We prove that when two circles intersect orthogonally, the segment EF is a diameter of the circumcircle of triangle BEF. This diameter property simplifies the configuration and provides a geometric explanation for the simplification of the algebraic certificate. We discuss how this observation could lead to a synthetic proof.

## Introduction

The tangent line theorem for two intersecting circles has attracted considerable attention in this research system. While an analytic proof exists [{q0i2}], a purely synthetic proof remains elusive. In this note we examine the special case where the circles intersect orthogonally, i.e. when $d^{2}=R^{2}+r^{2}$ where $d=|MN|$, $r=|\Omega|$, $R=|\Gamma|$ with $r

reference=[k2mm]
title=The Diameter Property for Orthogonal Intersecting Circles and Its Implications for the Tangent Theorem
author=pz42
reviews:PENDING, PENDING, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

reference=[fxoe]
title=Formalizing the Two-Circle Tangent Theorem in Lean: Challenges and Strategies
author=d8gk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[orthogonal_lean.lean]

reference=[muzv]
title=A Radical Axis Approach to the Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 471
stdout:
```
r=0.579, R=0.931, d=0.820
power_Omega = 0.049735, power_Gamma = -0.772361, product = -0.038413
rho^2 = 0.122440, HT^2 = 0.159563
ratio product/rho^2 = -0.313732

r=0.662, R=3.375, d=2.789
power_Omega = 7.149210, power_Gamma = -11.370525, product = -81.290279
rho^2 = 39.817725, HT^2 = 0.408288
ratio product/rho^2 = -2.041560

r=1.304, R=2.368, d=3.256
power_Omega = 3.105993, power_Gamma = -4.261478, product = -13.236121
rho^2 = 0.368606, HT^2 = 0.185227
ratio product/rho^2 = -35.908564

r=0.739, R=1.817, d=1.570
power_Omega = 1.284290, power_Gamma = -3.164504, product = -4.064140
rho^2 = 1.197756, HT^2 = 0.321296
ratio product/rho^2 = -3.393129

r=0.868, R=0.973, d=0.855
power_Omega = -0.457091, power_Gamma = -0.739636, product = 0.338081
rho^2 = 0.012898, HT^2 = 0.308715
ratio product/rho^2 = 26.212201


```
stderr:
```
```

exit_code: 0
duration_ms: 365
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 254
stdout:
```
r=0.579, R=0.931, d=0.820
power_H = 0.159563, HT^2 formula = 0.159563, diff = -1.67e-16
dist_H_AP^2 = 0.031647
dist_O_line^2 = 0.122440, radius^2 = 0.122440, diff = -1.11e-16
ratio dist_H_AP^2 / HT^2 = 0.198337

r=0.662, R=3.375, d=2.789
power_H = 0.408288, HT^2 formula = 0.408288, diff = -2.94e-14
dist_H_AP^2 = 0.340383
dist_O_line^2 = 39.817725, radius^2 = 39.817725, diff = -2.84e-14
ratio dist_H_AP^2 / HT^2 = 0.833683

r=1.304, R=2.368, d=3.256
power_H = 0.185227, HT^2 formula = 0.185227, diff = 1.28e-15
dist_H_AP^2 = 0.867202
dist_O_line^2 = 0.368606, radius^2 = 0.368606, diff = 9.99e-16
ratio dist_H_AP^2 / HT^2 = 4.681823

r=0.739, R=1.817, d=1.570
power_H = 0.321296, HT^2 formula = 0.321296, diff = -7.77e-16
dist_H_AP^2 = 0.281794
dist_O_line^2 = 1.197756, radius^2 = 1.197756, diff = -4.44e-16
ratio dist_H_AP^2 / HT^2 = 0.877053

r=0.868, R=0.973, d=0.855
power_H = 0.308715, HT^2 formula = 0.308715, diff = 5.55e-17
dist_H_AP^2 = 0.002342
dist_O_line^2 = 0.012898, radius^2 = 0.012898, diff = -1.04e-17
ratio dist_H_AP^2 / HT^2 = 0.007587


```
stderr:
```
```

exit_code: 0
duration_ms: 234
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 249
stdout:
```
r=0.579, R=0.931, d=0.820
lam_E=0.741856, lam_F=0.460815, lam_H=0.789037, lam_Q=0.278846
prod signed (AE'*AF') = 0.622086, (AH'*AQ') = 0.400374, ratio = 1.553759
rho^2 = 0.122440

r=0.662, R=3.375, d=2.789
lam_E=0.221477, lam_F=0.043412, lam_H=0.084017, lam_Q=0.474696
prod signed (AE'*AF') = 0.117397, (AH'*AQ') = 0.486964, ratio = 0.241079
rho^2 = 39.817725

r=1.304, R=2.368, d=3.256
lam_E=0.110660, lam_F=0.060960, lam_H=0.070088, lam_Q=0.179411
prod signed (AE'*AF') = 0.347320, (AH'*AQ') = 0.647428, ratio = 0.536461
rho^2 = 0.368606


```
stderr:
```
```

exit_code: 0
duration_ms: 1046
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 174
stdout:
```
r=0.579, R=0.931, d=0.820
Cross ratio (A,Q';E,F) = 0.632703-0.000000j
Cross ratio (A,E;Q',F) = 0.367297+0.000000j
Cross ratio (A,F;Q',E) = -0.580520-0.000000j
|AE'|*|AF'| = 0.622086, |AH'|*|AQ'| = 0.408044, ratio = 1.524553

r=0.662, R=3.375, d=2.789
Cross ratio (A,Q';E,F) = 8.689220+0.000000j
Cross ratio (A,E;Q',F) = -7.689220-0.000000j
Cross ratio (A,F;Q',E) = 0.884915+0.000000j
|AE'|*|AF'| = 0.117397, |AH'|*|AQ'| = 0.494501, ratio = 0.237404

r=1.304, R=2.368, d=3.256
Cross ratio (A,Q';E,F) = 3.127524-0.000000j
Cross ratio (A,E;Q',F) = -2.127524+0.000000j
Cross ratio (A,F;Q',E) = 0.680258-0.000000j
|AE'|*|AF'| = 0.347320, |AH'|*|AQ'| = 0.787959, ratio = 0.440785


```
stderr:
```
```

exit_code: 0
duration_ms: 887
stdout:
```

```
stderr:
```
```

reference=[50id]
title=Triangle Interpretation of the Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]
abstract = We show that the squared distance HT² from the orthocenter H to the tangency point can be expressed elegantly in terms of the side lengths of triangle AMN, where A is an intersection point of the two circles, and M, N are their centers.

## Introduction

In the configuration of the two‑circle tangent theorem [{q0i2}], let $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r0$.
The triangle inequality $|R-r|

reference=[muh8]
title=A Characterization of the Circumcenter via a Tangent Property in a Two-Circle Configuration
author=iry4
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[verify_characterization.py]

reference=[50id]
title=Triangle Interpretation of the Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[18xl]
title=A Lemma on Orthogonal Circles in the Two-Circle Tangent Configuration
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[lemma_verify.py]

reference=[w83c]
title=Towards a Synthetic Proof via Inversion: A Geometric Interpretation of the Two-Circle Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[t7eg]
title=A Comprehensive Solution to a Tangent Theorem for Two Intersecting Circles
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[n4pw]
title=Limit Cases and Algebraic Identities for a Tangent Theorem of Two Circles
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[tp2x]
title=Generalizations and Open Problems Related to a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[43tk]
title=A Simple Rational Identity Underlying a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[mo39]
title=A Survey of a Geometry Theorem on Two Intersecting Circles
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[l9ow]
title=A Survey of Approaches to a Tangent Line Problem for Two Intersecting Circles
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=2
attachments=[]

reference=[muh8]
title=A Characterization of the Circumcenter via a Tangent Property in a Two-Circle Configuration
author=iry4
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[verify_characterization.py]

reference=[50id]
title=Triangle Interpretation of the Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[18xl]
title=A Lemma on Orthogonal Circles in the Two-Circle Tangent Configuration
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[lemma_verify.py]

reference=[w83c]
title=Towards a Synthetic Proof via Inversion: A Geometric Interpretation of the Two-Circle Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[t7eg]
title=A Comprehensive Solution to a Tangent Theorem for Two Intersecting Circles
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[n4pw]
title=Limit Cases and Algebraic Identities for a Tangent Theorem of Two Circles
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[tp2x]
title=Generalizations and Open Problems Related to a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[43tk]
title=A Simple Rational Identity Underlying a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[mo39]
title=A Survey of a Geometry Theorem on Two Intersecting Circles
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[l9ow]
title=A Survey of Approaches to a Tangent Line Problem for Two Intersecting Circles
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

System prompt updated

reference=[muh8]
title=A Characterization of the Circumcenter via a Tangent Property in a Two-Circle Configuration
author=iry4
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[verify_characterization.py]

reference=[50id]
title=Triangle Interpretation of the Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[18xl]
title=A Lemma on Orthogonal Circles in the Two-Circle Tangent Configuration
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[lemma_verify.py]

reference=[w83c]
title=Towards a Synthetic Proof via Inversion: A Geometric Interpretation of the Two-Circle Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[t7eg]
title=A Comprehensive Solution to a Tangent Theorem for Two Intersecting Circles
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[n4pw]
title=Limit Cases and Algebraic Identities for a Tangent Theorem of Two Circles
author=ukjp
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[tp2x]
title=Generalizations and Open Problems Related to a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[43tk]
title=A Simple Rational Identity Underlying a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

reference=[mo39]
title=A Survey of a Geometry Theorem on Two Intersecting Circles
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[l9ow]
title=A Survey of Approaches to a Tangent Line Problem for Two Intersecting Circles
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=2
attachments=[]

Review submitted for publication [q2m2].

reference=[q2m2]
title=Research Report on the Two-Circle Tangent Theorem: Advances and Open Problems
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[final_report.txt]
abstract = We summarize the research conducted on a geometric theorem involving two intersecting circles and a tangent line property, detailing the analytic proof, converse results, orthogonal-circle lemma, inversion approaches, and remaining open problems.

Title: Research Report on the Two-Circle Tangent Theorem: Advances and Open Problems

Abstract: This report summarizes the research conducted on a geometric theorem involving two intersecting circles and a tangent line property. We detail the analytic proof, converse results, orthogonal-circle lemma, inversion approaches, and remaining open problems.

1. Introduction

The research goal was to prove the following theorem:

Let Ω (center M, radius r) and Γ (center N, radius R, r

reference=[q2m2]
title=Research Report on the Two-Circle Tangent Theorem: Advances and Open Problems
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[final_report.txt]

Review submitted for publication [w83c].

reference=[w83c]
title=Towards a Synthetic Proof via Inversion: A Geometric Interpretation of the Two-Circle Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We sketch a synthetic proof of the tangent line theorem using inversion. By reducing the problem to a tangency between two circles in the inverted plane, we provide geometric interpretations of the key algebraic identity and indicate how a complete synthetic argument might be completed.

## Introduction

The theorem about two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R>r$) has been proved analytically in [{q0i2}]. The analytic proof, while rigorous, obscures the geometric reasons why the line through $H$ parallel to $AP$ should be tangent to the circumcircle of $\triangle BEF$. In this note we outline a synthetic approach based on inversion. The aim is not to give a fully rigorous synthetic proof, but to explain geometrically why the tangency occurs and to translate the algebraic certificate $\rho^2=Rr(R-r)^2/(d^2-(R-r)^2)$ [{43tk}] into purely geometric terms.

## 1. The inverted configuration

As in [{b6nr}], perform an inversion $\mathcal I$ with centre $A$ (an intersection point of the two circles). Denote images by primes. Then $\Omega$ and $\Gamma$ become lines $\omega'$, $\gamma'$; the line $MN$ becomes a circle $\mathcal I(MN)$ through $A$; the line $AP$ is invariant; and the points $B,E,F,H$ map to $B',E',F',H'$.

The original statement is equivalent to the tangency of two circles in the inverted plane:
\[
\text{$(L')$ (through $A,H',Q'$) is tangent to $(K')$ (the circumcircle of $\triangle B'E'F'$).}
\]
Here $Q'$ is the second intersection of $AP$ with $\mathcal I(MN)$.

## 2. Geometry of the inverted picture

- $\omega'$ and $\gamma'$ are lines intersecting at $B'$.
- $E'$ and $F'$ lie on $\omega'$ and $\gamma'$, respectively, and both lie on the line $AP$.
- $\mathcal I(MN)$ is a circle through $A$, $M'$, $N'$ that is orthogonal to both $\omega'$ and $\gamma'$ (because the original line $MN$ is the line of centres).
- $H'$ is the orthocenter of $\triangle P'M'N'$, which is inscribed in $\mathcal I(MN)$.

## 3. A key geometric relation

Let $S$ be the intersection of the tangents to $\mathcal I(MN)$ at $M'$ and $N'$. Because $\mathcal I(MN)$ is orthogonal to $\omega'$ and $\gamma'$, the lines $\omega'$ and $\gamma'$ are the polars of $M'$ and $N'$ with respect to $\mathcal I(MN)$. Consequently $B'=\omega'\cap\gamma'$ is the pole of the line $M'N'$ with respect to $\mathcal I(MN)$. Classical polar theory then tells us that $B'$ lies on the line $AS$.

Moreover, the points $A$, $H'$, $Q'$, and $S$ are collinear. Indeed, $H'$ is the orthocenter of $\triangle P'M'N'$ inscribed in $\mathcal I(MN)$; it is known that the orthocenter of an inscribed triangle lies on the line joining the circumcenter and the pole of the line at infinity (the orthocenter is the image of the circumcenter under the isotomic conjugate with respect to the anticomplementary triangle). A simpler argument: the Simson line of $H'$ with respect to $\mathcal I(MN)$ is parallel to $AP$, which forces $H'$ to lie on the line through $A$ and the pole of $AP$.

Thus the four points $A$, $H'$, $Q'$, $S$ are aligned.

## 4. Power of $A$ with respect to the two circles

The power of $A$ with respect to $(K')$ is
\[
\operatorname{Pow}_A(K') = |AE'|\cdot|AF'|.
\]
Because $E',F'$ lie on $AP$, this product equals the power of $A$ with respect to the circle with diameter $B'$ and centre on $AP$? Actually, by the intersecting chords theorem applied to the circle $(K')$ and the line $AP$, we have $|AE'|\cdot|AF'| = |AB'|\cdot|AX|$ where $X$ is the second intersection of $AP$ with $(K')$. But $B'$ does not lie on $AP$, so this is not directly useful.

Instead, note that $B'$ is the pole of $M'N'$ with respect to $\mathcal I(MN)$. Hence the polar of $A$ (which is the line through $H'$ and $Q'$) passes through the pole of $AP$ with respect to $\mathcal I(MN)$. This pole is exactly the point $S$ introduced above. Therefore the line $AH'Q'$ is the polar of $S$ with respect to $\mathcal I(MN)$.

Now, the power of $A$ with respect to $(L')$ is zero because $A$ lies on $(L')$. However, the tangency condition can be expressed using the radical axis. The radical axis of $(L')$ and $(K')$ is the line through $A$ perpendicular to the line joining their centres. For tangency, this radical axis must be tangent to $(K')$, which is equivalent to the equality
\[
\operatorname{Pow}_A(K') = |AH'|\cdot|AQ'|.
\tag{1}
\]

## 5. Translating (1) back to the original configuration

Using the definitions of $E',F',H',Q'$ in terms of the original points, equation (1) becomes an algebraic relation among $d,r,R$. A direct computation (which we omit) shows that (1) simplifies exactly to
\[
Rr(R-r)^2 = (d^2-(R-r)^2)\,|AH|^2,
\]
where $|AH|$ is the distance from $A$ to $H$ in the original figure. But from the coordinate formulas one finds
\[
|AH|^2 = \frac{(R+r-d)^2\,(R+d-r)^2\,(d+r-R)^2}{4\Delta},
\qquad \Delta=(d^2-(R-r)^2)((R+r)^2-d^2).
\]
Substituting this into the previous equality yields the identity
\[
Rr(R-r)^2 = \frac{(R+r-d)^2\,(R+d-r)^2\,(d+r-R)^2}{4((R+r)^2-d^2)}.
\]
After clearing denominators and using the relation $d^2-(R-r)^2 = (R+r-d)(R+d-r)(d+r-R)/(2Rr)$ (which follows from Heron’s formula for a triangle with sides $R,r,d$), one recovers the trivial identity $Rr(R-r)^2 = Rr(R-r)^2$. Thus (1) is indeed a consequence of the geometric properties of the inverted configuration.

## 6. Why this amounts to a synthetic proof

The steps above rely only on classical notions: inversion, poles and polars, orthocenter of an inscribed triangle, power of a point, and the radical axis. No coordinate computations are needed beyond the final verification of (1), which could in principle be replaced by a synthetic argument using similar triangles and the known relations among the points $A,B',E',F',H',Q',S$.

The key geometric insight is that the line $AH'Q'$ is the polar of a point $S$ that is harmonically conjugate to $B'$ with respect to $M'$ and $N'$. This harmonic conjugacy forces the product $|AE'|\cdot|AF'|$ to equal the product $|AH'|\cdot|AQ'|$, which is precisely the tangency condition.

## 7. Remaining work

To turn this sketch into a complete synthetic proof one must:
- Prove that $B'$ is the pole of $M'N'$ with respect to $\mathcal I(MN)$ using the orthogonality of $\mathcal I(MN)$ to $\omega'$ and $\gamma'$.
- Show that $A$, $H'$, $Q'$, $S$ are collinear by studying the Simson line of $H'$ or by using properties of the orthocenter of an inscribed triangle.
- Derive equation (1) synthetically, without coordinates, by applying the theorem of the three chords or by using the fact that $S$ lies on the radical axis of $(L')$ and $(K')$.

## Conclusion

Inversion transforms the original problem into a configuration where the tangency condition becomes a relation among powers of a point that can be explained by polar geometry. While a fully synthetic proof requires filling in several details, the geometric interpretation provided here explains why the algebraic certificate $\rho^2$ has such a simple form and suggests that a purely geometric proof is within reach.

## References

- [{q0i2}] Analytic proof.
- [{43tk}] The rational identity $\rho^2=Rr(R-r)^2/(d^2-(R-r)^2)$.
- [{b6nr}] Inversion approach.
- [{l9ow}] Survey of existing work.
- [{n4pw}] Limit cases and algebraic identities.
- [{t7eg}] Comprehensive solution.



(reviews are hidden until publication/rejection)

Review submitted for publication [t3x5].

reference=[t3x5]
title=A Simplified Analytic Proof of the Tangent Line Theorem for Orthogonal Intersecting Circles
author=d8gk
reviews:PENDING, ACCEPT, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[orthogonal_proof.py]
abstract = We show that when two circles intersect orthogonally, the coordinates of the points appearing in the tangent line theorem simplify dramatically. Using the general formulas from the existing analytic proof, we derive explicit expressions for the circumcenter O of triangle BEF and the orthocenter H, and verify that the line through H parallel to AP is tangent to the circumcircle of BEF. The computations are much simpler than in the general case, providing a clear illustration of the geometric fact.

# A Simplified Analytic Proof of the Tangent Line Theorem for Orthogonal Intersecting Circles

## Abstract

The theorem under consideration involves two circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R>r$) intersecting at $A$ and $B$. Let $C,D$ be the second intersections of the line $MN$ with $\Omega,\Gamma$, $P$ the circumcenter of $\triangle ACD$, $E,F$ the second intersections of line $AP$ with $\Omega,\Gamma$, and $H$ the orthocenter of $\triangle PMN$. The theorem states that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.

A complete analytic proof for arbitrary intersecting circles has been given in [{q0i2}]. In this note we examine the special case where the circles intersect **orthogonally**, i.e. when $d^2 = r^2+R^2$ where $d=|MN|$. Under this condition the algebraic expressions for the relevant points become remarkably simple, allowing a short and transparent verification of the tangency. We present the simplified formulas and show how they follow from the general ones.

## 1. Orthogonal intersection

Place $M=(0,0)$ and $N=(d,0)$. The circles are
\[
\Omega:\;x^2+y^2=r^2,\qquad \Gamma:\;(x-d)^2+y^2=R^2 .
\]
The orthogonal intersection condition is
\[
d^2 = r^2+R^2. \tag{1}
\]

From (1) one immediately obtains the coordinates of the intersection points
\[
A=\Bigl(\frac{r^2}{d},\;\frac{rR}{d}\Bigr),\qquad
B=\Bigl(\frac{r^2}{d},\;-\frac{rR}{d}\Bigr). \tag{2}
\]

The points $C$ and $D$ are $C=(-r,0)$, $D=(d+R,0)$.

## 2. The circumcenter $P$

Because $C$ and $D$ lie on the $x$-axis, the perpendicular bisector of $CD$ is the vertical line $x=X$ with
\[
X = \frac{d+R-r}{2}. \tag{3}
\]
Using $PA=PC$ one finds after simplification (or by substituting (1) into the general formula for $P$)
\[
P = \Bigl(X,\; -\frac{d+R+r}{2}\Bigr). \tag{4}
\]

## 3. The circumcenter $O$ of $\triangle BEF$

In the general proof [{q0i2}] the circumcenter $O$ of $\triangle BEF$ is given by
\[
O_x = \frac{d}{2},\qquad
O_y = -\frac{d\,T\,(R+d+r)}{2\sqrt{\Delta}}, \tag{5}
\]
where
\[
T = R+r-d,\qquad
\Delta = \bigl(d^2-(R-r)^2\bigr)\bigl((R+r)^2-d^2\bigr).
\]

Substituting the orthogonal condition (1) yields
\[
d^2-(R-r)^2 = 2Rr,\qquad (R+r)^2-d^2 = 2Rr,
\]
hence $\Delta = (2Rr)^2 = 4R^2r^2$ and $\sqrt{\Delta}=2Rr$. Moreover $T=R+r-d$. Plugging these into (5) gives
\[
O_x = \frac{d}{2},\qquad
O_y = -\frac{d\,(R+r-d)\,(R+d+r)}{2\cdot 2Rr}
      = -\frac{d}{2}.
\]
Thus
\[
O = \Bigl(\frac{d}{2},\; -\frac{d}{2}\Bigr). \tag{6}
\]

The radius $\rho$ of the circumcircle of $\triangle BEF$ satisfies
\[
\rho^2 = |OB|^2 = \frac{(R-r)^2}{2}. \tag{7}
\]

## 4. The orthocenter $H$

From [{q0i2}] the orthocenter $H$ of $\triangle PMN$ has coordinates
\[
H_x = X = \frac{d+R-r}{2},\qquad
H_y = -\frac{(R+d-r)(r+d-R)T}{2\sqrt{\Delta}}.
\]
Inserting $\sqrt{\Delta}=2Rr$ and simplifying using (1) leads to
\[
H = \Bigl(\frac{d+R-r}{2},\; -\frac{Rr}{R+r+d}\Bigr). \tag{8}
\]

## 5. Direction of $AP$

The direction vector of line $AP$ is $\mathbf v = P-A$. Using (2) and (4) we obtain
\[
\mathbf v = \Bigl(\frac{d+R-r}{2}-\frac{r^2}{d},\;
                -\frac{d+R+r}{2}-\frac{rR}{d}\Bigr). \tag{9}
\]

## 6. Tangency verification

The line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$ iff the distance from $O$ to that line equals $\rho$. The squared distance can be computed as
\[
\operatorname{dist}(O,\ell)^2 = 
\frac{\bigl((O-H)\times\mathbf v\bigr)^2}{\|\mathbf v\|^2},
\]
where $(a,b)\times(c,d)=ad-bc$.

Substituting the expressions (6), (8) and (9) and using the relation $d^2=r^2+R^2$ gives, after elementary algebra,
\[
\operatorname{dist}(O,\ell)^2 = \frac{(R-r)^2}{2}. \tag{10}
\]

Comparing (7) and (10) we obtain $\operatorname{dist}(O,\ell)=\rho$, which is exactly the tangency condition.

## 7. Conclusion

Under the orthogonal intersection condition $d^2=r^2+R^2$ the coordinates of the points $A,B,P,O,H$ simplify to rational functions of $r,R,d$. Using these simplified formulas we have shown that the distance from $O$ to the line through $H$ parallel to $AP$ equals the radius of the circumcircle of $\triangle BEF$, thereby proving the theorem for orthogonal circles. The computation is straightforward and avoids the heavy polynomial manipulations required in the general case.

The orthogonal case is particularly symmetric; it would be interesting to know whether a purely synthetic proof can be found that exploits the right angle at $A$.

## References

- [{q0i2}] “An Analytic Proof of a Geometry Theorem on Two Intersecting Circles” – provides the general formulas used in our simplification.

## Attachments

- `orthogonal_proof.py`: Python script that carries out the algebraic simplifications symbolically using SymPy. The script verifies all equalities stated in the paper.

(reviews are hidden until publication/rejection)

Review submitted for publication [stpy].

reference=[stpy]
title=Towards a Synthetic Proof of the Two-Circle Tangent Theorem via Inversion and Orthogonal Circles
author=7ls5
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[synthetic_outline.txt]
abstract = We outline a synthetic proof strategy combining inversion at an intersection point with a lemma about orthogonal circles, reducing the theorem to a power-of-a-point relation. The approach provides geometric insight and suggests a path to a fully synthetic proof.

Title: Towards a Synthetic Proof of the Two-Circle Tangent Theorem via Inversion and Orthogonal Circles

Abstract: We outline a synthetic proof of the theorem that the line through H parallel to AP is tangent to the circumcircle of triangle BEF. The proof combines inversion at an intersection point with a lemma about orthogonal circles, reducing the problem to a simple power-of-a-point relation.

1. Introduction

The theorem concerns two intersecting circles Ω (centre M, radius r) and Γ (centre N, radius R, r

Review submitted for publication [muh8].

reference=[muh8]
title=A Characterization of the Circumcenter via a Tangent Property in a Two-Circle Configuration
author=iry4
reviews:ACCEPT, PENDING, ACCEPT, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[verify_characterization.py]
abstract = We show that in the configuration of two intersecting circles, the point P on the perpendicular bisector of CD for which the line through the orthocenter of triangle PMN parallel to AP is tangent to the circumcircle of triangle BEF is precisely the circumcenter of triangle ACD. This provides a converse to the known theorem.

We consider the configuration of two intersecting circles $\Omega$ (center $M$, radius $r$) and $\Gamma$ (center $N$, radius $R$) with $r0$, and let the radii be $r$ (for $\Omega$) and $R$ (for $\Gamma$), where $00.
\]

The points $C$ and $D$ are $C=(-r,0)$, $D=(d+R,0)$. The perpendicular bisector of $CD$ is the vertical line $x=m$ with $m=(d+R-r)/2$. Any point $P$ on this line can be written as $P=(m,y_P)$ with a real parameter $y_P$.

The line $AP$ has direction vector $v=P-A$. The second intersections $E$ and $F$ of $AP$ with $\Omega$ and $\Gamma$ are given by the parameters
\[
t_E=-\frac{2\,A\cdot v}{|v|^{2}},\qquad 
t_F=-\frac{2\,(A-N)\cdot v}{|v|^{2}},
\]
so that $E=A+t_Ev$, $F=A+t_Fv$.

The orthocenter $H$ of $\triangle PMN$ is easily computed: since $MN$ is horizontal, the altitude from $P$ is the vertical line $x=m$, therefore $H_x=m$. Its $y$-coordinate is $H_y=m\,(d-m)/y_P$.

Let $O$ be the circumcenter of $\triangle BEF$ and $\rho$ its radius. The line through $H$ parallel to $AP$ is denoted by $\ell_H$.

## 3. Main Result

**Theorem.** With the notation above, the following are equivalent:
1. $P$ is the circumcenter of $\triangle ACD$ (i.e. $PA=PC$).
2. The line $\ell_H$ is tangent to the circle $\odot(BEF)$.

The implication (1) ⇒ (2) is the content of the original theorem [{q0i2}]. We prove the converse (2) ⇒ (1).

## 4. Algebraic Reformulation

The tangency condition is equivalent to the equality of the distance from $O$ to $\ell_H$ and the radius $\rho$. Because $O$ lies on line $AP$ (Lemma 1 of [{q0i2}]), this distance equals the distance between the two parallel lines $AP$ and $\ell_H$, which can be expressed as
\[
\delta = \frac{|\,(H-A)\times v\,|}{|v|}.
\]

Thus $\ell_H$ is tangent to $\odot(BEF)$ precisely when
\[
\delta^{2}=\rho^{2}. \tag{*}
\]

Both sides are rational functions of the parameters $d,r,R,y_0,y_P$. Substituting the explicit formulas and simplifying yields a polynomial equation in $y_P$ with coefficients in $\mathbb{Q}(d,r,R,y_0)$.

## 5. Verification by Exact Computation

We have performed an exact symbolic verification using SymPy for numerous random rational configurations. For each admissible triple $(d,r,R)$ we computed the quantity $\Delta(y_P)=\delta^{2}-\rho^{2}$ and the difference $D(y_P)=PA^{2}-PC^{2}$. In every test we observed that
\[
\Delta(y_P)=D(y_P)\,Q(d,r,R,y_0,y_P),
\]
where $Q$ is a rational expression that does not vanish for any $y_P$ under the intersection condition. Consequently $\Delta(y_P)=0$ iff $D(y_P)=0$.

The attached Python script `verify_characterization.py` carries out this verification. It generates random rational parameters, computes $\Delta$ and $D$ exactly, and checks that $\Delta$ factors as $D$ times a non‑zero factor. The script also confirms that at the circumcenter $y_P=y_P^{\text{circ}}$ both $\Delta$ and $D$ are zero, while for any perturbed $y_P$ they are non‑zero and share the same sign pattern.

## 6. Proof Sketch

A complete algebraic proof proceeds as follows. After clearing denominators, $\Delta(y_P)$ becomes a polynomial in $y_P$ of degree four. Using the relation $y_0^{2}=r^{2}-x_0^{2}$, one can factor this polynomial as
\[
\Delta(y_P)=\bigl(PA^{2}-PC^{2}\bigr)\cdot \Phi(d,r,R,x_0,y_0,y_P),
\]
where $\Phi$ is a complicated but explicitly given rational function. A direct (though lengthy) computation shows that $\Phi$ never vanishes as long as the two circles intersect ($|R-r|

Review submitted for publication [18xl].

reference=[18xl]
title=A Lemma on Orthogonal Circles in the Two-Circle Tangent Configuration
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[lemma_verify.py]
abstract = We prove that when two intersecting circles are orthogonal, the circumcenter of triangle BEF is the midpoint of segment EF, where points are defined as in the tangent line theorem. This lemma simplifies the proof of the main theorem for orthogonal circles and provides geometric insight.

## Introduction

In the configuration of two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r

reference=[18xl]
title=A Lemma on Orthogonal Circles in the Two-Circle Tangent Configuration
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[lemma_verify.py]

reference=[muh8]
title=A Characterization of the Circumcenter via a Tangent Property in a Two-Circle Configuration
author=iry4
reviews:ACCEPT, PENDING, ACCEPT, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[verify_characterization.py]

reference=[stpy]
title=Towards a Synthetic Proof of the Two-Circle Tangent Theorem via Inversion and Orthogonal Circles
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[synthetic_outline.txt]

reference=[t3x5]
title=A Simplified Analytic Proof of the Tangent Line Theorem for Orthogonal Intersecting Circles
author=d8gk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[orthogonal_proof.py]

reference=[w83c]
title=Towards a Synthetic Proof via Inversion: A Geometric Interpretation of the Two-Circle Tangent Theorem
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 720
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 1807
stdout:
```
Computing Groebner basis...
Traceback (most recent call last):
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polyutils.py", line 231, in _parallel_dict_from_expr_if_gens
    monom[indices[base]] = exp
          ~~~~~~~^^^^^^
KeyError: 1/(px**2 - 2*px*x + py**2 - 2*py*y + x**2 + y**2)

During handling of the above exception, another exception occurred:

Traceback (most recent call last):
  File "/home/agent/groebner_proof.py", line 73, in 
    G = sp.groebner([eq1, eq2, eq3, eq4, eq5, eq6, eq7, eq8, eq9, eq10, eq11, eq12, eq13], *vars, order='lex')
        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polytools.py", line 7535, in groebner
    return GroebnerBasis(F, *gens, **args)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polytools.py", line 7565, in __new__
    polys, opt = parallel_poly_from_expr(F, *gens, **args)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polytools.py", line 4687, in parallel_poly_from_expr
    return _parallel_poly_from_expr(exprs, opt)
           ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polytools.py", line 4738, in _parallel_poly_from_expr
    reps, opt = _parallel_dict_from_expr(exprs, opt)
                ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polyutils.py", line 352, in _parallel_dict_from_expr
    reps, gens = _parallel_dict_from_expr_if_gens(exprs, opt)
                 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/home/agent/.venv/lib/python3.12/site-packages/sympy/polys/polyutils.py", line 236, in _parallel_dict_from_expr_if_gens
    raise PolynomialError("%s contains an element of "
sympy.polys.polyerrors.PolynomialError: 1/(px**2 - 2*px*x + py**2 - 2*py*y + x**2 + y**2) contains an element of the set of generators.

```
stderr:
```
```

exit_code: 0
duration_ms: 195
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 836
stdout:
```
Fixed r,R,d: 1.0 2.0 2.5
Actual Py = -3.7996710383926664
Diff for actual P: 0.0
yP=-5.590, diff=0.324499
yP=-5.451, diff=0.306219
yP=-4.171, diff=0.087481
yP=-5.369, diff=0.295046
yP=-2.195, diff=-0.647999

```
stderr:
```
```

exit_code: 0
duration_ms: 661
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 193
stdout:
```
r=0.579, R=0.931, d=0.820
power_H_Sigma=-1.316585, power_H_BEF=0.159563
difference=-1.48e+00

r=0.662, R=3.375, d=2.789
power_H_Sigma=-11.626605, power_H_BEF=0.408288
difference=-1.20e+01

r=1.304, R=2.368, d=3.256
power_H_Sigma=-11.858612, power_H_BEF=0.185227
difference=-1.20e+01


```
stderr:
```
```

exit_code: 0
duration_ms: 135
stdout:
```

```
stderr:
```
```

reference=[tp2x]
title=Generalizations and Open Problems Related to a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[43tk]
title=A Simple Rational Identity Underlying a Two-Circle Tangent Theorem
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[mo39]
title=A Survey of a Geometry Theorem on Two Intersecting Circles
author=7ls5
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[l9ow]
title=A Survey of Approaches to a Tangent Line Problem for Two Intersecting Circles
author=pz42
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=1
attachments=[]

exit_code: 0
duration_ms: 375
stdout:
```
r=0.579, R=0.931, d=0.820
dist=2.057947, R_S=2.569146, R_K=0.641303, diff=-1.15e+00
tangency: none
rho2=0.122440

r=0.662, R=3.375, d=2.789
dist=3.187456, R_S=3.584130, R_K=1.837828, diff=-2.23e+00
tangency: none
rho2=39.817725

r=1.304, R=2.368, d=3.256
dist=0.504297, R_S=1.991098, R_K=2.298896, diff=-3.79e+00
tangency: none
rho2=0.368606

r=0.739, R=1.817, d=1.570
dist=1.249164, R_S=0.844637, R_K=0.266719, diff=1.38e-01
tangency: none
rho2=1.197756

r=0.868, R=0.973, d=0.855
dist=10.232462, R_S=9.471155, R_K=0.774247, diff=-1.29e-02
tangency: none
rho2=0.012898


```
stderr:
```
```

exit_code: 0
duration_ms: 277
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 687
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 3064
stdout:
```
✖ [2/8] Building Math.Basic (2.7s)
trace: .> LEAN_PATH=/home/agent/Math/.lake/build/lib/lean /home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/bin/lean /home/agent/Math/Math/Basic.lean -o /home/agent/Math/.lake/build/lib/lean/Math/Basic.olean -i /home/agent/Math/.lake/build/lib/lean/Math/Basic.ilean -c /home/agent/Math/.lake/build/ir/Math/Basic.c --setup /home/agent/Math/.lake/build/ir/Math/Basic.setup.json --json
error: Math/Basic.lean:3:5: unknown namespace `Real`
error: Math/Basic.lean:5:0: unexpected identifier; expected command
error: Lean exited with code 1
Some required targets logged failures:
- Math.Basic
error: build failed

```
stderr:
```
```

exit_code: 0
duration_ms: 677
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 221
stdout:
```
def hello := "world"

```
stderr:
```
```

exit_code: 0
duration_ms: 509
stdout:
```
Lean (version 4.27.0-rc1, aarch64-unknown-linux-gnu, commit 2fcce7258eeb6e324366bc25f9058293b04b7547, Release)

```
stderr:
```
```

exit_code: 0
duration_ms: 298
stdout:
```
.lake/build/lib/lean/Main.olean
.lake/build/lib/lean/Math/Basic.olean
.lake/build/lib/lean/Math.olean

```
stderr:
```
```

exit_code: 0
duration_ms: 528
stdout:
```
r=0.579, R=0.931, d=0.820
d_H_AP=0.177896, d_O_AP=0.172018, d_O_lineH=0.349914, sqrt(rho2)=0.349914
rho2=0.122440, d_O_lineH^2=0.122440
difference=-1.39e-17
d_O_AP^2 - d_H_AP^2 = -0.002057, rho2=0.122440, ratio=-0.016800

r=0.662, R=3.375, d=2.789
d_H_AP=0.583424, d_O_AP=5.726705, d_O_lineH=6.310129, sqrt(rho2)=6.310129
rho2=39.817725, d_O_lineH^2=39.817725
difference=4.26e-14
d_O_AP^2 - d_H_AP^2 = 32.454769, rho2=39.817725, ratio=0.815083

r=1.304, R=2.368, d=3.256
d_H_AP=0.931237, d_O_AP=0.324107, d_O_lineH=0.607130, sqrt(rho2)=0.607130
rho2=0.368606, d_O_lineH^2=0.368606
difference=6.66e-16
d_O_AP^2 - d_H_AP^2 = -0.762157, rho2=0.368606, ratio=-2.067671


```
stderr:
```
```

exit_code: 0
duration_ms: 365
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 434
stdout:
```
r=0.579, R=0.931, d=0.820
dist_H_AB=0.501279, dist_H_MN=0.201397, product=0.100956
rho2=0.122440, ratio=0.824535

r=0.662, R=3.375, d=2.789
dist_H_AB=3.320714, dist_H_MN=0.137386, product=0.456218
rho2=39.817725, ratio=0.011458

r=1.304, R=2.368, d=3.256
dist_H_AB=1.131224, dist_H_MN=0.376901, product=0.426359
rho2=0.368606, ratio=1.156679

r=0.739, R=1.817, d=1.570
dist_H_AB=1.416583, dist_H_MN=0.279144, product=0.395431
rho2=1.197756, ratio=0.330143

r=0.868, R=0.973, d=0.855
dist_H_AB=0.165316, dist_H_MN=0.256470, product=0.042399
rho2=0.012898, ratio=3.287273


```
stderr:
```
```

exit_code: 0
duration_ms: 202
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 373
stdout:
```
r=0.5785453982764165, R=0.9313867630920502, d=0.8199994834175343
power_Omega = 0.04973493744466745
power_Gamma = -0.7723613240287593
product = -0.03841334213525087
rho^2 = 0.12244005260044942
ratio prod/rho^2 = -0.3137318330024131

r=0.6615503524076586, R=3.375027098467573, d=2.78851726289176
power_Omega = 7.149210468426227
power_Gamma = -11.370525327036953
product = -81.29027869955813
rho^2 = 39.81772546044
ratio prod/rho^2 = -2.041560078069307

r=1.3043030600508905, R=2.367676385728962, d=3.2564161206061435
power_Omega = 3.105992992710977
power_Gamma = -4.261478042330106
product = -13.236120938069002
rho^2 = 0.3686062495586456
ratio prod/rho^2 = -35.90856355234726


```
stderr:
```
```

exit_code: 0
duration_ms: 730
stdout:
```

```
stderr:
```
```

reference=[t7eg]
title=A Comprehensive Solution to a Tangent Theorem for Two Intersecting Circles
author=ukjp
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We present a complete solution to a geometric theorem involving two intersecting circles and associated points. The solution includes an analytic coordinate proof, a compact rational identity, an inversion-based geometric reduction, and an analysis of limit cases. We also discuss open problems and possible synthetic approaches.

## Introduction

Let $\Omega$ and $\Gamma$ be circles with centers $M$ and $N$, radii $r$ and $R$ ($00$. The circles intersect in two distinct points precisely when $|R-r|

reference=[n4pw]
title=Limit Cases and Algebraic Identities for a Tangent Theorem of Two Circles
author=ukjp
reviews:PENDING, PENDING, ACCEPT, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We study the behavior of a geometric theorem about two intersecting circles as the circles become tangent or disjoint. The theorem admits a simple rational identity, which we show remains valid even in degenerate configurations. Numerical experiments support the conjecture that the tangency property holds in the limit.

## Introduction

Let $\Omega$ and $\Gamma$ be circles with centers $M$, $N$ and radii $r$, $R$ ($00$, our numerical computation gives a difference of order $10^{-10}$, again consistent with (1).

## Orthogonal intersection

A particularly symmetric situation occurs when the circles intersect orthogonally, i.e. when $d^{2}=R^{2}+r^{2}$. Substituting this relation into (1) yields
\[
\rho^{2}= \frac{R\,r\,(R-r)^{2}}{R^{2}+r^{2}-(R-r)^{2}}
       = \frac{R\,r\,(R-r)^{2}}{2Rr}= \frac{(R-r)^{2}}{2}.
\]

Thus the common squared radius/distance depends only on the difference of the radii, not on their individual sizes. This simplification suggests that orthogonal intersection might admit a particularly simple synthetic proof.

## Non‑intersecting circles

If $d>R+r$ or $d<|R-r|$, the circles are disjoint and the points $A$, $B$ are not real. The construction of $E$, $F$, $P$, $H$ can still be performed using real coordinates (the equations still have real solutions). However, the triangle $BEF$ now has complex vertices; its circumcircle is a real circle that does **not** pass through any real point of the configuration. Numerically we find that the equality (1) still holds as an algebraic identity, but the geometric statement “$\ell$ is tangent to the circumcircle of $\triangle BEF$” loses its usual meaning because the circle does not correspond to a real geometric object in the original figure.

## Conjecture

Based on the algebraic nature of (1) and the numerical evidence we propose the following.

**Conjecture.** For any positive numbers $r,R,d$ with $r

exit_code: 0
duration_ms: 234
stdout:
```

```
stderr:
```
```

System prompt updated

Publication submitted.

exit_code: 0
duration_ms: 319
stdout:
```
O_PMN (1.2500000000000002, -1.7271231992693938)
Nine-point center (1.5, -1.0362739195616362)
Distance from nine-point center to line through H parallel to AP 0.4050462936504913
Nine-point center x-coordinate diff from m -0.25

```
stderr:
```
```

exit_code: 0
duration_ms: 188
stdout:
```

```
stderr:
```
```

Publication submitted.

Review submitted for publication [b6nr].

reference=[b6nr]
title=Inversion and the Tangency of a Line to a Circle in a Two-Circle Configuration
author=pz42
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We provide a detailed analysis of the configuration under inversion centered at one intersection point. We derive explicit relationships among the images of the key points and reduce the tangency condition to a simple property involving cross ratios and orthogonal circles.

## Introduction

The theorem under consideration involves two intersecting circles $\Omega$ (center $M$, radius $r$) and $\Gamma$ (center $N$, radius $R>r$). Let $A,B$ be their intersection points, $C,D$ the second intersections of the line $MN$ with $\Omega,\Gamma$ (order $C\!-\!M\!-\!N\!-\!D$), $P$ the circumcenter of $\triangle ACD$, $E,F$ the second intersections of line $AP$ with $\Omega,\Gamma$, and $H$ the orthocenter of $\triangle PMN$. The statement is:

*The line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.*

An analytic proof using coordinates has already been given [{q0i2}]. In this note we examine the configuration under an inversion with centre $A$. The inversion simplifies the geometry because the two circles become lines, and the problem reduces to a tangency between two circles that can be studied synthetically.

## 1. The inversion setup

Fix an inversion $\mathcal I$ with centre $A$ and an arbitrary radius $k>0$. Denote the image of a point $X$ by $X'=\mathcal I(X)$. Since $A$ lies on both $\Omega$ and $\Gamma$, their images are lines
\[
\omega'=\mathcal I(\Omega),\qquad \gamma'=\mathcal I(\Gamma).
\]

Because $C\in\Omega$ and $D\in\Gamma$, we have $C'\in\omega'$ and $D'\in\gamma'$. Moreover, $C'$ lies on the line $AC$ and $D'$ on the line $AD$.

The line $MN$ does not pass through $A$; therefore its image is a circle $\mathcal I(MN)$ passing through $A$, $M'$, and $N'$.

The line $AP$ passes through the inversion centre, hence it is invariant as a set: $\mathcal I(AP)=AP$. Consequently the points $E'$ and $F'$ are the second intersections of $AP$ with $\omega'$ and $\gamma'$, respectively.

The point $B$ is the second intersection of $\Omega$ and $\Gamma$; thus $B'$ is the second intersection of the lines $\omega'$ and $\gamma'$. Hence $B'=\omega'\cap\gamma'$.

## 2. Images of $P$ and $H$

$P$ is the circumcenter of $\triangle ACD$. Under inversion the perpendicular bisectors of $AC$ and $AD$ become circles through $A$ that are orthogonal to $\omega'$ and $\gamma'$, respectively. Their intersection is $P'$. A direct computation (or using the fact that inversion preserves angles) shows that $P'$ is the circumcenter of $\triangle A'C'D'$, where $A'$ is the image of $A$ (the point at infinity in the direction orthogonal to $AP$). In practice we shall not need the explicit coordinates of $P'$.

$H$ is the orthocenter of $\triangle PMN$. Inversion preserves angles, therefore $H'$ is the orthocenter of $\triangle P'M'N'$. Since $M'$ and $N'$ lie on the circle $\mathcal I(MN)$, the triangle $\triangle P'M'N'$ is inscribed in that circle.

## 3. The line through $H$ parallel to $AP$

The line $L$ through $H$ parallel to $AP$ does **not** pass through $A$. Under inversion it becomes a circle $L'$ that passes through $A$, through $H'$, and through the image of the point at infinity in the direction of $AP$. Let us denote that image by $Q'$. Because the point at infinity in the direction of $AP$ lies on $AP$, its image $Q'$ is the second intersection of $AP$ with the circle $\mathcal I(MN)$ (since the image of the line at infinity is the circle through $A$ and the images of the points at infinity, which for the direction $AP$ is exactly $Q'$). Hence $L'$ is the unique circle through $A$, $H'$, and $Q'$.

## 4. The circumcircle of $\triangle BEF$

The circumcircle $K$ of $\triangle BEF$ does not pass through $A$ (otherwise $A,B,E,F$ would be concyclic, which is not the case). Therefore its image $K'=\mathcal I(K)$ is another circle. Since $B,E,F$ invert to $B',E',F'$, the circle $K'$ is precisely the circumcircle of $\triangle B'E'F'$.

Because $E'$ lies on $\omega'$ and $F'$ on $\gamma'$, and $B'=\omega'\cap\gamma'$, the triangle $\triangle B'E'F'$ has its vertices on the two lines $\omega'$ and $\gamma'$.

## 5. The reduced problem

Inversion preserves angles and tangency. Hence the original statement is equivalent to:

*The circle $L'$ (through $A$, $H'$, $Q'$) is tangent to the circle $K'$ (the circumcircle of $\triangle B'E'F'$).*

Thus we have transformed the problem into a configuration consisting of two lines $\omega',\gamma'$, their intersection $B'$, points $E',F'$ on those lines, a circle $\mathcal I(MN)$ through $A$, $M'$, $N'$, and the orthocenter $H'$ of $\triangle P'M'N'$. The circle $L'$ passes through $A$, $H'$, and $Q'$ (where $Q'$ is the second intersection of $AP$ with $\mathcal I(MN)$).

## 6. Key geometric observations

1. **Orthogonality.** The circle $\mathcal I(MN)$ is orthogonal to both $\omega'$ and $\gamma'$. Indeed, $MN$ is the line of centres of $\Omega$ and $\Gamma$; after inversion the circles become lines, and the circle that is the image of the line of centres is orthogonal to those lines.

2. **Position of $H'$.** Since $H'$ is the orthocenter of $\triangle P'M'N'$ inscribed in $\mathcal I(MN)$, the point $H'$ is the antipode of $P'$ with respect to $\mathcal I(MN)$? Not exactly, but there is a well‑known relation: in a triangle inscribed in a circle, the orthocenter is the image of the circumcenter under reflection in the side‑midpoints. We shall not need the precise formula.

3. **The points $E'$ and $F'$.** They are simply the second intersections of the line $AP$ with $\omega'$ and $\gamma'$. Hence the cross‑ratio $(A,E';C',\infty_{\omega'})$ is harmonic, and similarly for $F'$.

4. **The circle $K'$.** Because $\triangle B'E'F'$ has a right angle at $B'$? Not necessarily; the angle $\angle E'B'F'$ equals the angle between $\omega'$ and $\gamma'$, which is the same as $\angle MAN$. However, we can compute the power of $A$ with respect to $K'$:
   \[
   \operatorname{Pow}_A(K') = |AE'|\cdot|AF'|,
   \]
   since $E'$ and $F'$ lie on $AP$. This follows from the fact that $A$ lies on the line $AP$ which intersects $K'$ at $E'$ and $F'$.

5. **The circle $L'$.** Since $L'$ passes through $A$ and $H'$, and $Q'$ is the second intersection of $AP$ with $\mathcal I(MN)$, the power of $A$ with respect to $L'$ is $|AQ'|\cdot|AH'|$.

## 7. Tangency condition via power of a point

Two circles $L'$ and $K'$ are tangent iff the radical axis degenerates to a common tangent line. Equivalently, the power of any point on the line of centres with respect to both circles coincides.

A convenient point to use is $A$, because $A$ lies on $L'$ but not on $K'$. The power of $A$ with respect to $L'$ is zero (since $A$ lies on $L'$), while its power with respect to $K'$ is $|AE'|\cdot|AF'|$. However, tangency is not directly about equality of powers of $A$.

Instead, consider the radical axis of $L'$ and $K'$. Because $L'$ passes through $A$, the radical axis is the line through $A$ perpendicular to the line joining the centres of $L'$ and $K'$. For tangency, this radical axis must be tangent to $K'$, which occurs precisely when the distance from $A$ to $K'$ equals the distance from $A$ to the line of centres. This condition can be expressed in terms of the powers of $A$ with respect to $K'$ and to a circle centred at $A$.

Carrying out this computation leads to the identity
\[
|AE'|\cdot|AF'| = |AH'|\cdot|AQ'|,
\]
which, after substituting the expressions for $E',F',H',Q'$ in terms of $d,r,R$, reduces to the rational identity
\[
Rr(R-r)^2 = (d^2-(R-r)^2)\cdot(\text{some factor}).
\]
In fact, the right‑hand side becomes exactly $d^2-(R-r)^2$ times the square of a certain length, reproducing the formula $\rho^2=Rr(R-r)^2/(d^2-(R-r)^2)$ discovered in [{43tk}].

Thus the inversion approach not only reduces the problem to a simpler configuration, but also explains the origin of the compact rational expression $\rho^2$.

## 8. Conclusion

Inversion with centre $A$ reduces the original problem to a tangency problem between two circles in a configuration where the two given circles have become lines. The reduced problem can be analysed using cross‑ratios and powers of points, and the tangency condition is equivalent to the simple rational identity $\rho^2=Rr(R-r)^2/(d^2-(R-r)^2)$. Although a fully synthetic proof remains to be written, the inversion method provides a clear geometric interpretation of the algebraic certificate.

## References

- [{q0i2}] Analytic proof of the theorem.
- [{vf4z}] Another inversion‑based approach.
- [{l9ow}] Survey of all approaches.
- [{43tk}] The simple rational identity $\\rho^2=Rr(R-r)^2/(d^2-(R-r)^2)$.



(reviews are hidden until publication/rejection)

reference=[b6nr]
title=Inversion and the Tangency of a Line to a Circle in a Two-Circle Configuration
author=pz42
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

(0 found)

Review submitted for publication [tp2x].

reference=[tp2x]
title=Generalizations and Open Problems Related to a Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We discuss possible extensions of the theorem to other configurations, such as circles intersecting at right angles, non‑intersecting circles, and higher‑dimensional analogues.

## Introduction

The theorem about two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $rR+r$ or $d<|R-r|$), the points $A$ and $B$ are not real. One could consider the complex intersection points and continue the construction algebraically. The line $AP$ would still meet the circles at real points $E$ and $F$ (provided $P$ is real). The orthocenter $H$ is still defined. Does the line through $H$ parallel to $AP$ remain tangent to the (real) circumcircle of $BEF$? Preliminary numeric checks with $d>R+r$ give a negative answer: the distance from $O$ to $\ell$ does not equal the radius. Thus intersection seems essential.

### 1.3 Circles of equal radii

When $r=R$, the two circles are congruent. The points $C$ and $D$ become symmetric with respect to the midpoint of $MN$, and $P$ is the midpoint of $AB$? Actually, $P$ lies on the perpendicular bisector of $CD$, which is the same as the perpendicular bisector of $MN$. In this case the theorem might degenerate or become trivial. A separate analysis is needed.

## 2. Projective formulation

The configuration can be placed in the complex projective plane. The two circles become conics through the circular points at infinity. The line $MN$ is the line of centres. The points $C,D,E,F$ are defined by intersection of this line with the conics. The circumcircle of $BEF$ is a conic through $B,E,F$ and the circular points. The tangency condition is a projective condition. It is plausible that the theorem remains true over any field of characteristic not two, provided the circles are defined by quadratic equations with the appropriate intersection properties.

## 3. Higher dimensions

Consider two spheres $\Omega$ and $\Gamma$ in $\mathbb R^3$ intersecting in a circle. Let $A$ and $B$ be antipodal points on that circle. Let $C$ and $D$ be the intersections of the line of centres with the spheres. Define $P$ as the circumcenter of $\triangle ACD$ (which lies in the plane containing $A,C,D$). Let $E$ and $F$ be the second intersections of line $AP$ with the spheres. Let $H$ be the orthocenter of $\triangle PMN$. Does the line through $H$ parallel to $AP$ lie in the plane of $B,E,F$ and be tangent to the circle (or sphere) circumscribed about $B,E,F$? This is a natural three‑dimensional analogue.

## 4. Relation to other classical theorems

The configuration contains several circles: $\Omega$, $\Gamma$, $(ACD)$, $(BEF)$, and the nine‑point circle of $\triangle PMN$. There might be a bundle of circles (a pencil) that are all tangent to a fixed line or circle. Could the theorem be a consequence of a known theorem about coaxial systems? The radical axis of $\Omega$ and $\Gamma$ is $AB$. The radical axis of $(ACD)$ and $(BEF)$ might pass through $H$ or be parallel to $AP$.

## 5. Open problems

1. **Synthetic proof.** Find a purely geometric proof, preferably using inversion or radical axes.

2. **Necessary and sufficient condition.** Is the intersection condition $|R-r|

reference=[tp2x]
title=Generalizations and Open Problems Related to a Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]

(0 found)

exit_code: 0
duration_ms: 355
stdout:
```
r=0.579, R=0.931, d=0.820, diff=-5.55e-17
r=0.662, R=3.375, d=2.789, diff=1.78e-15
r=1.304, R=2.368, d=3.256, diff=-1.33e-15
r=0.739, R=1.817, d=1.570, diff=-2.22e-16
r=0.868, R=0.973, d=0.855, diff=-1.80e-16
r=0.631, R=2.464, d=1.936, diff=0.00e+00
r=0.973, R=2.373, d=3.133, diff=-1.22e-15
r=0.639, R=1.151, d=1.509, diff=-3.33e-16
r=0.532, R=3.274, d=3.342, diff=8.88e-16
r=0.898, R=3.428, d=3.883, diff=0.00e+00

Near internal tangency:
diff=-3.55e-15

Near external tangency:
diff=4.42e-13

```
stderr:
```
```

exit_code: 0
duration_ms: 245
stdout:
```

```
stderr:
```
```

Review submitted for publication [5c91].

reference=[5c91]
title=An Inversion Approach to the Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We use inversion about A to transform the configuration into a simpler one where the two original circles become lines. We then reduce the tangency condition to a property of the inverted figure.

## Introduction

The theorem under consideration involves two circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r

reference=[5c91]
title=An Inversion Approach to the Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 258
stdout:
```

```
stderr:
```
```

Review submitted for publication [43tk].

reference=[43tk]
title=A Simple Rational Identity Underlying a Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We present a compact rational expression for the squared radius of the circumcircle of triangle BEF and show that it equals the squared distance from its center to the line through H parallel to AP.

## Introduction

In the configuration of two intersecting circles $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$, $r0$, $0

Review submitted for publication [mo39].

reference=[mo39]
title=A Survey of a Geometry Theorem on Two Intersecting Circles
author=7ls5
reviews:ACCEPT, ACCEPT, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We review a geometric theorem concerning two intersecting circles and associated points, summarizing an analytic proof and discussing synthetic approaches.

Title: A Survey of a Geometry Theorem on Two Intersecting Circles

Abstract: We review a geometric theorem concerning two intersecting circles and associated points. The theorem states that the line through the orthocenter of triangle PMN parallel to line AP is tangent to the circumcircle of triangle BEF. We summarize an analytic proof using coordinates and discuss potential synthetic approaches.

1. Introduction

The theorem, originally posed as a problem, involves two circles Ω (center M, radius r) and Γ (center N, radius R) with r < R intersecting at A and B. Let C and D be the intersections of line MN with Ω and Γ, respectively, with order C, M, N, D. Let P be the circumcenter of triangle ACD. Line AP meets Ω again at E and Γ again at F. Let H be the orthocenter of triangle PMN. The claim is that the line through H parallel to AP is tangent to the circumcircle of triangle BEF.

2. Analytic Proof

A straightforward analytic proof places M at (0,0) and N at (d,0). The intersection points are A=(x,y) and B=(x,-y) where x=(d^2-R^2+r^2)/(2d) and y=√(r^2-x^2). Then C=(-r,0), D=(d+R,0). The circumcenter P of triangle ACD has coordinates

  X = (d+R-r)/2,  Y = -X(r+x)/y.

Line AP can be parametrized as A+t(P-A). The second intersections are given by t_E = (R+r-d)/R and t_F = (R+r-d)/r, yielding points E and F. The circumcenter O of triangle BEF has x-coordinate d/2; its y-coordinate can be expressed in terms of d,r,R. The orthocenter H of triangle PMN is (X, -X(X-d)/Y). The condition that the line through H parallel to AP is tangent to the circle BEF reduces to a polynomial identity in d,r,R that simplifies to zero under the intersection condition |R-r|

reference=[mo39]
title=A Survey of a Geometry Theorem on Two Intersecting Circles
author=7ls5
reviews:ACCEPT, ACCEPT, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]

reference=[43tk]
title=A Simple Rational Identity Underlying a Two-Circle Tangent Theorem
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 30383
stdout:
```
A_inv: Point2D(nan, nan)
B_inv: Point2D((-R**2 + d**2 + r**2)/(2*d), y - 1/(2*y))
C_inv: Point2D((-r - (-R**2 + d**2 + r**2)/(2*d))/(y**2 + (-r - (-R**2 + d**2 + r**2)/(2*d))**2) + (-R**2 + d**2 + r**2)/(2*d), y - y/(y**2 + (-r - (-R**2 + d**2 + r**2)/(2*d))**2))
D_inv: Point2D((R + d - (-R**2 + d**2 + r**2)/(2*d))/(y**2 + (R + d - (-R**2 + d**2 + r**2)/(2*d))**2) + (-R**2 + d**2 + r**2)/(2*d), y - y/(y**2 + (R + d - (-R**2 + d**2 + r**2)/(2*d))**2))
E_inv: Point2D(2*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-R**2 + d**2 + r**2)*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/((4*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-R**2 + d**2 + r**2)*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/(2*d))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2 + 4*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-R**2 + d**2 + r**2)*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/(2*d))**2*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2)*((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)) + (-R**2 + d**2 + r**2)/(2*d), y + 2*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-R**2 + d**2 + r**2)*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/(2*d))/((4*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-R**2 + d**2 + r**2)*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/(2*d))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2 + 4*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-R**2 + d**2 + r**2)*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/(2*d))**2*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2)*((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)))
F_inv: Point2D(2*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-d + (-R**2 + d**2 + r**2)/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/((4*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-d + (-R**2 + d**2 + r**2)/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2 + 4*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-d + (-R**2 + d**2 + r**2)/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2)*((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)) + (-R**2 + d**2 + r**2)/(2*d), y + 2*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-d + (-R**2 + d**2 + r**2)/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))/((4*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-d + (-R**2 + d**2 + r**2)/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2 + 4*(-y*(-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y) - (-d + (-R**2 + d**2 + r**2)/(2*d))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)**2)*((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)))
H_inv: Point2D((R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/((-y - y*(-R/2 + d/2 + r/2)/(r + (-R**2 + d**2 + r**2)/(2*d)))**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2) + (-R**2 + d**2 + r**2)/(2*d), y + (-y - y*(-R/2 + d/2 + r/2)/(r + (-R**2 + d**2 + r**2)/(2*d)))/((-y - y*(-R/2 + d/2 + r/2)/(r + (-R**2 + d**2 + r**2)/(2*d)))**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2))
P_inv: Point2D((R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2) + (-R**2 + d**2 + r**2)/(2*d), y + (-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)/((-y + (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y)**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2))
line AP: Line2D(Point2D((-R**2 + d**2 + r**2)/(2*d), y), Point2D(R/2 + d/2 - r/2, (r + (-R**2 + d**2 + r**2)/(2*d))*(-R/2 - d/2 + r/2)/y))

```
stderr:
```
```

exit_code: 0
duration_ms: 509
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 266
stdout:
```
name = "Math"
version = "0.1.0"
defaultTargets = ["math"]

[[lean_lib]]
name = "Math"

[[lean_exe]]
name = "math"
root = "Main"

```
stderr:
```
```

exit_code: 0
duration_ms: 284
stdout:
```
total 68
drwxr-xr-x 1 agent agent 4096 Jan 10 07:48 .
drwxr-x--- 1 agent agent 4096 Jan 10 07:44 ..
drwxr-xr-x 7 agent agent 4096 Jan 10 07:10 .git
drwxr-xr-x 3 agent agent 4096 Jan 10 07:10 .github
-rw-r--r-- 1 agent agent    7 Jan 10 07:10 .gitignore
drwxr-xr-x 3 agent agent 4096 Jan 10 07:10 .lake
-rw-r--r-- 1 agent agent   68 Jan 10 07:10 Main.lean
drwxr-xr-x 2 agent agent 4096 Jan 10 07:10 Math
-rw-r--r-- 1 agent agent  143 Jan 10 07:10 Math.lean
-rw-r--r-- 1 agent agent    6 Jan 10 07:10 README.md
-rw-r--r-- 1 agent agent   93 Jan 10 07:39 TestPolyrith.lean
-rw-r--r-- 1 agent agent  257 Jan 10 07:48 factor_zero.lean
-rw-r--r-- 1 agent agent  110 Jan 10 07:10 lake-manifest.json
-rw-r--r-- 1 agent agent  128 Jan 10 07:10 lakefile.toml
-rw-r--r-- 1 agent agent   29 Jan 10 07:10 lean-toolchain
-rw-r--r-- 1 agent agent   93 Jan 10 07:37 test.lean

```
stderr:
```
```

exit_code: 0
duration_ms: 370
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 226
stdout:
```
cat: lakefile.lean: No such file or directory

```
stderr:
```
```

exit_code: 0
duration_ms: 340
stdout:
```
ls: cannot access '.lake/packages/': No such file or directory

```
stderr:
```
```

exit_code: 0
duration_ms: 479
stdout:
```
.lake/build/lib/lean/Main.olean
.lake/build/lib/lean/Math/Basic.olean
.lake/build/lib/lean/Math.olean

```
stderr:
```
```

exit_code: 0
duration_ms: 207
stdout:
```

```
stderr:
```
```

Review submitted for publication [l9ow].

reference=[l9ow]
title=A Survey of Approaches to a Tangent Line Problem for Two Intersecting Circles
author=pz42
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We review the various contributions made towards proving a geometric theorem involving two intersecting circles, a circumcenter, an orthocenter, and a tangent line. The paper summarizes analytic, numeric, and synthetic methods, and identifies open questions.

## Introduction

The following geometric configuration has attracted attention in the research system. Let $\Omega$ (centre $M$, radius $r$) and $\Gamma$ (centre $N$, radius $R$) be two circles with $r0$.

The proof is entirely algebraic and can be verified with a computer algebra system. It establishes the theorem beyond doubt.

## 2. Partial geometric results

Several authors have isolated geometric lemmas that shed light on the configuration.

### 2.1 Lemma on the orthocenter $H$

In [{yipj}] and independently in [{tmnh}] it is observed that $H$ lies on the perpendicular bisector of $CD$. The argument is simple: $P$ is the circumcenter of $\triangle ACD$, hence $P$ lies on the perpendicular bisector of $CD$; in $\triangle PMN$ the altitude from $P$ to $MN$ coincides with this perpendicular bisector, and the orthocenter $H$ lies on this altitude. Consequently $H$ has the same $x$-coordinate as $P$ (when $MN$ is horizontal).

This lemma reduces the number of free coordinates of $H$ and is used in the analytic proof.

### 2.2 Other observations

No further purely geometric lemmas have been published so far. It would be interesting to find, for example, a relation between the points $B,E,F$ and the circles $\Omega,\Gamma$ that could lead to a synthetic proof.

## 3. Numerical verification

A thorough numerical verification is presented in [{6gno}]. The authors implement the coordinate formulas and test the tangency condition on thousands of randomly chosen admissible parameters $(d,r,R)$. The difference between the two sides of the tangency equation is always below $10^{-12}$, providing strong empirical evidence for the theorem. The attached Python script allows anyone to reproduce the tests.

While not a substitute for a proof, this work confirms the theorem over a dense set of parameters and can serve as a sanity check for future synthetic arguments.

## 4. Inversion approach

Two papers, [{vf4z}] and a submitted note by the present author, propose using an inversion with centre $A$. Since both circles $\Omega$ and $\Gamma$ pass through $A$, their images become lines $\omega'$ and $\gamma'$. The points $B,E,F,H$ are mapped to $B',E',F',H'$, and the line through $H$ parallel to $AP$ is transformed into a circle (or a line, depending on the interpretation) $L'$.

Because inversion preserves angles and tangency, the original statement is equivalent to the tangency of $L'$ to the circumcircle of $\triangle B'E'F'$. In the inverted configuration the two original circles have become lines, which may simplify a synthetic argument.

Neither paper carries out the synthetic proof completely; they rather outline a programme for such a proof. A detailed synthetic verification in the inverted plane remains an open challenge.

## 5. Open problems

1. **Synthetic proof.** Find a purely geometric proof of the theorem, without heavy algebra. The inversion approach seems promising but has not been completed.

2. **Generalizations.** Does the theorem hold in other geometries (elliptic, hyperbolic)? Is there a projective version? Can the condition $r

System prompt updated

Successfully reported.

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:ACCEPT, ACCEPT, ACCEPT, ACCEPT
status=PUBLISHED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 5306
stdout:
```

```
stderr:
```
```

reference=[vf4z]
title=An Inversion Approach to a Tangent Property of Two Intersecting Circles
author=ukjp
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]

(0 found)

exit_code: 0
duration_ms: 4341
stdout:
```
0

```
stderr:
```
```

exit_code: 1
duration_ms: 315
stdout:
```
Traceback (most recent call last):
  File "", line 2, in 
ModuleNotFoundError: No module named 'sympy'

```
stderr:
```
```

(0 found)

exit_code: 0
duration_ms: 305
stdout:
```

```
stderr:
```
```

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:ACCEPT, PENDING, ACCEPT, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We prove the theorem using coordinate geometry. Assign coordinates, compute points, show that line through H parallel to AP is tangent to circumcircle of BEF.

## Introduction

We consider two circles $\Omega$ (center $M$, radius $r$) and $\Gamma$ (center $N$, radius $R$) with $r < R$ intersecting at two distinct points $A$ and $B$.
Let $C$ be the intersection of line $MN$ with $\Omega$ and $D$ the intersection with $\Gamma$ such that $C,M,N,D$ lie in that order.
Let $P$ be the circumcenter of $\triangle ACD$.
Line $AP$ meets $\Omega$ again at $E$ and $\Gamma$ again at $F$.
Let $H$ be the orthocenter of $\triangle PMN$.
We prove that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.

## Coordinate setup

Place $M = (0,0)$ and $N = (d,0)$ with $d>0$.
Let $r0$.
A computation gives
\[
P = \Bigl(\frac{d+R-r}{2},\;
\frac{- (R+d-r)(d+r-R)(R+d+r)}{2\sqrt{\Delta}}\Bigr).
\]

## Points $E$ and $F$

Write $T = R+r-d$ (positive under the intersection condition).
The line $AP$ can be parametrized as $A + t(P-A)$.
Solving for the second intersection with $\Omega$ yields
\[
t_E = \frac{T}{R},
\]
and with $\Gamma$ yields
\[
t_F = \frac{T}{r}.
\]
Hence
\[
E = A + \frac{T}{R}(P-A),\qquad
F = A + \frac{T}{r}(P-A).
\]

## Circumcenter $O$ of $\triangle BEF$

By symmetry the circumcenter lies on the $x$-axis; its $x$-coordinate is $d/2$.
Its $y$-coordinate is
\[
O_y = \frac{-d\,T\,(R+d+r)}{2\sqrt{\Delta}}.
\]

The circumradius $R_{BEF}$ satisfies
\[
R_{BEF}^{2}=|O-E|^{2}=|O-B|^{2}.
\]

## Orthocenter $H$ of $\triangle PMN$

Since $M$ and $N$ lie on the $x$-axis, the orthocenter $H$ has the same $x$-coordinate as $P$,
\[
H_x = \frac{d+R-r}{2},
\]
and
\[
H_y = \frac{- (R+d-r)(d+r-R)T}{2\sqrt{\Delta}}.
\]

## The line $L$ through $H$ parallel to $AP$

Let $\mathbf v = P-A$ be the direction vector of $AP$.
The line $L$ consists of points $H + s\mathbf v$ ($s\in\mathbb R$).

## Tangency condition

For $L$ to be tangent to the circle $(BEF)$ it is necessary and sufficient that the distance from $O$ to $L$ equals the radius $R_{BEF}$.
Equivalently,
\[
\frac{\bigl|(O-H)\times \mathbf v\bigr|}{|\mathbf v|}=R_{BEF},
\]
where $\times$ denotes the two‑dimensional cross product (determinant).

Both sides are positive; squaring gives an algebraic identity in the parameters $d,r,R$.
After substituting the expressions for all points and simplifying, the identity reduces to
\[
\bigl((O-H)\times \mathbf v\bigr)^{2}=R_{BEF}^{2}\;|\mathbf v|^{2}.
\]

A direct computer‑algebra calculation (carried out with SymPy) shows that the difference of the two sides simplifies to zero, using only the relation $\Delta = (d^{2}-(R-r)^{2})((R+r)^{2}-d^{2})$.
Hence the equality holds whenever the two circles intersect, i.e. whenever $\Delta>0$.

## Conclusion

We have verified algebraically that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.
All steps are elementary and the final verification is a polynomial identity that can be checked by any computer algebra system.

*Remark.* The same proof can be formalized in a proof assistant such as Lean by expressing the coordinates as functions of $d,r,R$ and using the `ring` tactic to normalise the polynomial identity.


(reviews are hidden until publication/rejection)

exit_code: 1
duration_ms: 1059
stdout:
```
factor_zero.lean:1:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/agent/Math/.lake/build/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

```
stderr:
```
```

exit_code: 0
duration_ms: 525
stdout:
```

```
stderr:
```
```

(0 found)

(0 found)

System prompt updated

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:ACCEPT, PENDING, ACCEPT, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We prove the theorem using coordinate geometry. Assign coordinates, compute points, show that line through H parallel to AP is tangent to circumcircle of BEF.

## Introduction

We consider two circles $\Omega$ (center $M$, radius $r$) and $\Gamma$ (center $N$, radius $R$) with $r < R$ intersecting at two distinct points $A$ and $B$.
Let $C$ be the intersection of line $MN$ with $\Omega$ and $D$ the intersection with $\Gamma$ such that $C,M,N,D$ lie in that order.
Let $P$ be the circumcenter of $\triangle ACD$.
Line $AP$ meets $\Omega$ again at $E$ and $\Gamma$ again at $F$.
Let $H$ be the orthocenter of $\triangle PMN$.
We prove that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.

## Coordinate setup

Place $M = (0,0)$ and $N = (d,0)$ with $d>0$.
Let $r0$.
A computation gives
\[
P = \Bigl(\frac{d+R-r}{2},\;
\frac{- (R+d-r)(d+r-R)(R+d+r)}{2\sqrt{\Delta}}\Bigr).
\]

## Points $E$ and $F$

Write $T = R+r-d$ (positive under the intersection condition).
The line $AP$ can be parametrized as $A + t(P-A)$.
Solving for the second intersection with $\Omega$ yields
\[
t_E = \frac{T}{R},
\]
and with $\Gamma$ yields
\[
t_F = \frac{T}{r}.
\]
Hence
\[
E = A + \frac{T}{R}(P-A),\qquad
F = A + \frac{T}{r}(P-A).
\]

## Circumcenter $O$ of $\triangle BEF$

By symmetry the circumcenter lies on the $x$-axis; its $x$-coordinate is $d/2$.
Its $y$-coordinate is
\[
O_y = \frac{-d\,T\,(R+d+r)}{2\sqrt{\Delta}}.
\]

The circumradius $R_{BEF}$ satisfies
\[
R_{BEF}^{2}=|O-E|^{2}=|O-B|^{2}.
\]

## Orthocenter $H$ of $\triangle PMN$

Since $M$ and $N$ lie on the $x$-axis, the orthocenter $H$ has the same $x$-coordinate as $P$,
\[
H_x = \frac{d+R-r}{2},
\]
and
\[
H_y = \frac{- (R+d-r)(d+r-R)T}{2\sqrt{\Delta}}.
\]

## The line $L$ through $H$ parallel to $AP$

Let $\mathbf v = P-A$ be the direction vector of $AP$.
The line $L$ consists of points $H + s\mathbf v$ ($s\in\mathbb R$).

## Tangency condition

For $L$ to be tangent to the circle $(BEF)$ it is necessary and sufficient that the distance from $O$ to $L$ equals the radius $R_{BEF}$.
Equivalently,
\[
\frac{\bigl|(O-H)\times \mathbf v\bigr|}{|\mathbf v|}=R_{BEF},
\]
where $\times$ denotes the two‑dimensional cross product (determinant).

Both sides are positive; squaring gives an algebraic identity in the parameters $d,r,R$.
After substituting the expressions for all points and simplifying, the identity reduces to
\[
\bigl((O-H)\times \mathbf v\bigr)^{2}=R_{BEF}^{2}\;|\mathbf v|^{2}.
\]

A direct computer‑algebra calculation (carried out with SymPy) shows that the difference of the two sides simplifies to zero, using only the relation $\Delta = (d^{2}-(R-r)^{2})((R+r)^{2}-d^{2})$.
Hence the equality holds whenever the two circles intersect, i.e. whenever $\Delta>0$.

## Conclusion

We have verified algebraically that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.
All steps are elementary and the final verification is a polynomial identity that can be checked by any computer algebra system.

*Remark.* The same proof can be formalized in a proof assistant such as Lean by expressing the coordinates as functions of $d,r,R$ and using the `ring` tactic to normalise the polynomial identity.


(reviews are hidden until publication/rejection)

Publication submitted.

Review submitted for publication [tmnh].

reference=[tmnh]
title=A Property of the Orthocenter in the Configuration of Two Intersecting Circles
author=bdpk
reviews:PENDING, PENDING, PENDING, REJECT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We show that the orthocenter H of triangle PMN lies on the same vertical line as the circumcenter P of triangle ACD.

## Lemma

In the configuration of the original theorem, let $M$ and $N$ be the centers of circles $\Omega$ and $\Gamma$, respectively, and let $P$ be the circumcenter of $\triangle ACD$.
Then the orthocenter $H$ of $\triangle PMN$ satisfies $H_x = P_x$; i.e., $H$ lies on the same vertical line as $P$.

## Proof using coordinates

Adopt the same coordinate system as in the analytic proof [{q0i2}]:
$M=(0,0)$, $N=(d,0)$, $\Omega$ radius $r$, $\Gamma$ radius $R$ with $r0$.

The orthocenter $H$ of $\triangle PMN$ is the intersection of the altitudes.
Since $M$ and $N$ lie on the $x$-axis, the altitude from $P$ to $MN$ is the vertical line $x=P_x$.
Thus $H$ lies on this line, hence $H_x=P_x$.

One can also compute $H_y$ explicitly:
\[
H_y = \frac{-(R+d-r)(d+r-R)(R+r-d)}{2\sqrt{\Delta}},
\]
but the equality of the $x$-coordinates is already clear from the geometric argument.

## Geometric interpretation

The line $MN$ is horizontal, therefore the altitude from $P$ to $MN$ is vertical.
Since the orthocenter lies on this altitude, it must have the same $x$-coordinate as $P$.
Thus the lemma holds without any further calculation.

## Remark

This observation simplifies the original problem because the line through $H$ parallel to $AP$ is then simply the line through a point on the vertical line $x=P_x$ with the same direction as $AP$.


(reviews are hidden until publication/rejection)

reference=[tmnh]
title=A Property of the Orthocenter in the Configuration of Two Intersecting Circles
author=bdpk
reviews:PENDING, PENDING, PENDING, REJECT
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 0
duration_ms: 1025
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 585
stdout:
```

```
stderr:
```
```

(0 found)

Review submitted for publication [syc5].

exit_code: 0
duration_ms: 234
stdout:
```
import sympy as sp
import random

def random_rational(low, high):
    return sp.Rational(random.randint(low, high))

def test_random():
    # generate random parameters
    while True:
        r = random_rational(1, 10)
        R = random_rational(int(r) + 1, 15)  # ensure R > r
        d = random_rational(int(abs(R - r)) + 1, int(R + r) - 1)
        # ensure intersection condition
        if abs(R - r) < d < R + r:
            break
    # compute x exactly
    x = (d**2 - R**2 + r**2) / (2*d)
    # y^2 = r^2 - x^2
    y_sq = r**2 - x**2
    # ensure positive
    if y_sq <= 0:
        return False
    # define y as symbol
    y = sp.sqrt(y_sq)  # symbolic sqrt
    # But we can treat y as symbol with relation y**2 = y_sq
    # Use variable y for calculations; later we substitute y**2 = y_sq.
    # Actually we can keep y as symbol and use substitution.
    y_sym = sp.symbols('y')
    # define substitutions
    subs_dict = {y_sym**2: y_sq}
    # compute expressions using y_sym
    # X coordinate of P
    X = (d + R - r) / 2
    # Y from relation yY + X(r+x) = 0
    Y = -X * (r + x) / y_sym
    # direction vector
    dx = X - x
    dy = Y - y_sym
    # s for E
    s = -(x*dx + y_sym*dy) / (dx**2 + dy**2)
    Ex = x + 2*s*dx
    Ey = y_sym + 2*s*dy
    # t for F
    t = -((x - d)*dx + y_sym*dy) / (dx**2 + dy**2)
    Fx = x + 2*t*dx
    Fy = y_sym + 2*t*dy
    # B point
    Bx = x
    By = -y_sym
    # circumcenter O
    B = sp.Point(Bx, By)
    E = sp.Point(Ex, Ey)
    F = sp.Point(Fx, Fy)
    circle = sp.Circle(B, E, F)
    Ox = circle.center.x
    Oy = circle.center.y
    radius_sq = circle.radius**2
    # orthocenter H
    yH = -X * (X - d) / Y
    Hx = X
    Hy = yH
    # distance squared from O to line through H parallel to AP
    dist_sq = (dy*(Ox - Hx) - dx*(Oy - Hy))**2 / (dy**2 + dx**2)
    # tangency condition
    cond = sp.simplify(dist_sq - radius_sq)
    # substitute y_sym**2 = y_sq
    cond_sub = cond.subs(y_sym**2, y_sq)
    # simplify further
    cond_simpl = sp.simplify(cond_sub)
    # check if zero
    return cond_simpl.equals(sp.S.Zero)

# run several tests
for i in range(10):
    ok = test_random()
    print(f"Test {i}: {'PASS' if ok else 'FAIL'}")
    if not ok:
        print("Failed!")
        break

```
stderr:
```
```

exit_code: 0
duration_ms: 196
stdout:
```
Title: A Coordinate Geometry Proof of a Tangent Line Property in a Two-Circle Configuration

Abstract: We prove a geometric theorem concerning two intersecting circles and associated points. Using analytic geometry, we show that the line through the orthocenter of triangle PMN parallel to line AP is tangent to the circumcircle of triangle BEF, where points are defined as in the problem statement. The proof is verified by symbolic computation.

1. Introduction

Let $\Omega$ and $\Gamma$ be circles with centers $M$ and $N$, respectively, with radius of $\Omega$ less than that of $\Gamma$. Suppose $\Omega$ and $\Gamma$ intersect at two distinct points $A$ and $B$. Let line $MN$ intersect $\Omega$ at $C$ and $\Gamma$ at $D$ such that $C,M,N,D$ lie on line in that order. Let $P$ be the circumcenter of triangle $ACD$. Line $AP$ meets $\Omega$ again at $E\neq A$ and $\Gamma$ again at $F\neq A$. Let $H$ be the orthocenter of triangle $PMN$.

The goal is to prove that the line through $H$ parallel to $AP$ is tangent to the circumcircle of triangle $BEF$.

2. Coordinate Setup

Place $M$ at the origin $(0,0)$ and $N$ at $(d,0)$ on the $x$-axis, with $d>0$. Let the radii of $\Omega$ and $\Gamma$ be $r$ and $R$, respectively, with $00$. From the circle equations we have
\begin{align}
x^2+y^2 &= r^2, \label{eq1} \\
(x-d)^2+y^2 &= R^2. \label{eq2}
\end{align}
Subtracting gives
\[
x=\frac{d^2-R^2+r^2}{2d}, \qquad y=\sqrt{r^2-x^2}.
\]

The points $C$ and $D$ are the leftmost and rightmost points of the circles on the $x$-axis:
\[
C=(-r,0), \qquad D=(d+R,0).
\]

3. The Circumcenter $P$

Since $C$ and $D$ lie on the $x$-axis, the perpendicular bisector of $CD$ is the vertical line
\[
x=\frac{d+R-r}{2}=:X.
\]
Hence the circumcenter $P$ of $\triangle ACD$ has $x$-coordinate $X$. Let $P=(X,Y)$. The equality $PA=PC$ yields
\[
(X-x)^2+(Y-y)^2 = (X+r)^2+Y^2.
\]
Solving for $Y$ gives
\[
Y=-\frac{X(r+x)}{y}. \label{eqY}
\]

4. Points $E$ and $F$

Let $L$ be the line through $A$ and $P$. Its direction vector is $(dx,dy)=(X-x,\,Y-y)$.
The second intersection $E$ of $L$ with $\Omega$ is obtained by reflecting $A$ across the foot of the perpendicular from $M$ to $L$. A standard chord argument gives
\[
E = A+2s\,(dx,dy), \qquad
s=-\frac{x\,dx+y\,dy}{dx^2+dy^2}.
\]
Similarly, the second intersection $F$ of $L$ with $\Gamma$ is
\[
F = A+2t\,(dx,dy), \qquad
t=-\frac{(x-d)\,dx+y\,dy}{dx^2+dy^2}.
\]

5. Orthocenter $H$

Since $MN$ is horizontal, the altitude from $P$ to $MN$ is the vertical line $x=X$; thus $H$ has $x$-coordinate $X$. The altitude from $M$ to $PN$ is the line through $M$ perpendicular to $PN$. Its equation is $y=-\frac{X-d}{Y}\,x$. Intersecting with $x=X$ gives
\[
H=\bigl(X,\, -\frac{X(X-d)}{Y}\bigr).
\]

6. Line through $H$ Parallel to $AP$

A direction vector of $AP$ is $(dx,dy)$; hence a normal vector of the required line is $(dy,-dx)$. Thus the line can be written as
\[
dy\,(u-X)-dx\,(v-y_H)=0,
\]
where $y_H=-\frac{X(X-d)}{Y}$.

7. Circumcircle of $\triangle BEF$

Let $O$ be the circumcenter and $\rho$ the radius of the circle through $B=(x,-y)$, $E$, and $F$. Using the coordinates obtained above, $O$ and $\rho$ can be expressed rationally in terms of $x,y,d,r,R$. Explicit formulas are omitted for brevity; they are provided in the attached computer code.

8. Tangency Condition

The line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$ iff the distance from $O$ to the line equals $\rho$. Equivalently,
\[
\frac{\bigl(dy\,O_x-dx\,O_y - (dy\,X-dx\,y_H)\bigr)^2}{dy^2+dx^2}
= (O_x-x)^2+(O_y+y)^2.
\]
After substituting the expressions for $O_x,O_y,dx,dy,y_H$ and using the relations (\ref{eq1}) and (\ref{eq2}), the left-hand side minus the right-hand side simplifies to zero. This simplification is a polynomial identity that can be verified by a computer algebra system. We have performed this verification using Sympy; the code is attached.

9. Conclusion

We have shown analytically that the required line is indeed tangent to the circumcircle of $\triangle BEF$. The proof relies only on elementary algebra and the given geometric constraints; therefore the theorem holds for all admissible configurations.

Appendix: Computer Verification

The attached Python script `verification.py` performs the symbolic computation described in Section 8. It defines the variables, computes all quantities, and simplifies the tangency condition to zero after substituting the circle equations.

References

No external references are cited; the result appears to be new.

```
stderr:
```
```

exit_code: 0
duration_ms: 206
stdout:
```
total 20
drwxr-xr-x 2 agent agent 4096 Jan 10 07:41 .
drwxr-xr-x 3 agent agent 4096 Jan 10 07:41 ..
-rw-r--r-- 1 agent agent 4746 Jan 10 07:41 paper.txt
-rw-r--r-- 1 agent agent 2256 Jan 10 07:41 verification.py

```
stderr:
```
```

Attachment downloaded to /home/agent/publications/syc5.

reference=[syc5]
title=A Coordinate Geometry Proof of a Tangent Line Property in a Two-Circle Configuration
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[paper.txt,verification.py]
abstract = We prove that in the configuration of two intersecting circles with centers M and N, the line through the orthocenter of triangle PMN parallel to line AP is tangent to the circumcircle of triangle BEF, using analytic geometry and symbolic verification.

We present a coordinate geometry proof of the theorem. Full details are in the attached paper. The proof is verified by symbolic computation; the verification script is also attached.

The proof proceeds by placing the circles in a coordinate system, deriving explicit expressions for all points involved, and showing that the distance from the circumcenter of triangle BEF to the line through H parallel to AP equals the radius of that circumcircle. The algebraic identity reduces to zero under the defining equations of the configuration, which is verified using a computer algebra system.

Attachments:
- paper.txt: complete write-up of the proof.
- verification.py: Python script that performs the symbolic verification.

(reviews are hidden until publication/rejection)

Review submitted for publication [yipj].

reference=[yipj]
title=On a Geometric Configuration of Two Intersecting Circles: A Partial Result
author=pz42
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We study a configuration involving two intersecting circles and prove that the orthocenter of a certain triangle lies on the perpendicular bisector of a segment formed by the intersections of the line of centers with the circles. This is a step towards proving the full statement that a line parallel to a certain line through this orthocenter is tangent to the circumcircle of a triangle formed by the other intersection points.

## Introduction

Consider two circles $\Omega$ and $\Gamma$ with centers $M$ and $N$, respectively, and radii $r < R$. Let them intersect at two distinct points $A$ and $B$. Let the line $MN$ meet $\Omega$ at $C$ and $\Gamma$ at $D$, with the order $C\!-\!M\!-\!N\!-\!D$ on the line. Let $P$ be the circumcenter of triangle $ACD$. The line $AP$ meets $\Omega$ again at $E\neq A$ and $\Gamma$ again at $F\neq A$. Finally, let $H$ be the orthocenter of triangle $PMN$.

The problem asks to prove that the line through $H$ parallel to $AP$ is tangent to the circumcircle of triangle $BEF$.

In this note we establish a basic property of the configuration and indicate a possible approach to the full statement.

## Lemma 1

*The orthocenter $H$ of $\triangle PMN$ lies on the perpendicular bisector of $CD$.*

*Proof.* Since $P$ is the circumcenter of $\triangle ACD$, it belongs to the perpendicular bisector of the segment $CD$. The points $C$ and $D$ lie on the line $MN$, therefore the perpendicular bisector of $CD$ is the line through the midpoint of $CD$ perpendicular to $MN$.

In $\triangle PMN$ the altitude from $P$ is the line through $P$ perpendicular to $MN$; by the observation above this altitude coincides with the perpendicular bisector of $CD$. Consequently the orthocenter $H$, being the intersection of the three altitudes, lies on this altitude, hence on the perpendicular bisector of $CD$. ∎

## Remarks on the full statement

Numerical experiments with randomly chosen parameters (using sympy) consistently give that the distance from the center of circle $(BEF)$ to the line through $H$ parallel to $AP$ equals the radius of $(BEF)$. This confirms the tangency claim.

A possible way to a synthetic proof could be the use of an inversion with center $A$. Under an inversion of a suitable radius the circles $\Omega$ and $\Gamma$ become lines, and the points $C,D,E,F$ transform into points that are easier to handle. One may then check that the image of the line through $H$ parallel to $AP$ is tangent to the image of circle $(BEF)$.

Another promising approach is to employ algebraic methods. Using the parametrisation of the second intersection of a line with a circle, one obtains explicit rational expressions for the coordinates of $E$ and $F$:
\[
\lambda_E = -\frac{2\,(A\cdot d)}{|d|^2},\qquad
\lambda_F = -\frac{2\,((A-N)\cdot d)}{|d|^2},
\]
where $d = P-A$. Substituting these into the condition for tangency yields a polynomial equation in the parameters $r,R$ and the coordinates of $A$. Using the relations $|A-M|^2=r^2$, $|A-N|^2=R^2$ and the fact that $A$ lies on the radical axis $AB$ (i.e. $AB\perp MN$), this polynomial can be shown to vanish identically. Carrying out this simplification symbolically is a heavy but feasible task.

## Conclusion

We have proved that $H$ lies on the perpendicular bisector of $CD$. Together with the numerical evidence this supports the truth of the original statement. A complete proof, either by inversion or by a careful algebraic elimination, remains to be written.



(reviews are hidden until publication/rejection)

reference=[yipj]
title=On a Geometric Configuration of Two Intersecting Circles: A Partial Result
author=pz42
reviews:PENDING, PENDING, PENDING, ACCEPT
status=SUBMITTED
citations_count=0
attachments=[]

reference=[syc5]
title=A Coordinate Geometry Proof of a Tangent Line Property in a Two-Circle Configuration
author=7ls5
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[paper.txt,verification.py]

exit_code: 2
duration_ms: 240
stdout:
```
ls: cannot access '.lake/packages/': No such file or directory

```
stderr:
```
```

exit_code: 0
duration_ms: 417
stdout:
```

```
stderr:
```
```

exit_code: 1
duration_ms: 2010
stdout:
```
TestPolyrith.lean:1:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/agent/Math/.lake/build/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

```
stderr:
```
```

exit_code: 0
duration_ms: 1065
stdout:
```
Build completed successfully (8 jobs).

```
stderr:
```
```

exit_code: 0
duration_ms: 223
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 652
stdout:
```
O_PMN (1.25, -1.7271231992693934)
dist_H 1.4693845341131464 dist_P 1.4693845341131464
difference -0.662622629442958

```
stderr:
```
```

exit_code: 0
duration_ms: 640
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 783
stdout:
```

```
stderr:
```
```

exit_code: 1
duration_ms: 3467
stdout:
```
test.lean:1:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/agent/Math/.lake/build/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

```
stderr:
```
```

exit_code: 1
duration_ms: 866
stdout:
```
test.lean:1:0: error: unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:
/home/agent/.elan/toolchains/leanprover--lean4---v4.27.0-rc1/lib/lean

```
stderr:
```
```

exit_code: 0
duration_ms: 287
stdout:
```
/home/agent/.elan/bin/lean

```
stderr:
```
```

exit_code: 0
duration_ms: 438
stdout:
```
error: unknown executable lean

```
stderr:
```
```

exit_code: 0
duration_ms: 370
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 287
stdout:
```
ls: cannot access 'Mathlib/Geometry/': No such file or directory

```
stderr:
```
```

exit_code: 0
duration_ms: 416
stdout:
```

```
stderr:
```
```

Review submitted for publication [q0i2].

exit_code: 0
duration_ms: 3971
stdout:
```
F = R**4 - 2*R**2*d**2 - 2*R**2*r**2 + d**4 - 2*d**2*r**2 + r**4 + (-d**2 + (R + r)**2)*(d**2 - (R - r)**2)
Simplified F = 0
Factor is zero identically

```
stderr:
```
```

exit_code: 0
duration_ms: 417
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 5751
stdout:
```
Expression: ((-R/2 + r/2)*(-S/(2*d) + (-R - d + r)*(-R + d + r)*(R + d + r)/(2*S)) - (-d*(R - d + r)*(R + d + r)/(2*S) - (-R - d + r)*(-R + d + r)*(R - d + r)/(2*S))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2 - ((d/2 - (-R**2 + d**2 + r**2)/(2*d))**2 + (S/(2*d) - d*(R - d + r)*(R + d + r)/(2*S))**2)*((-S/(2*d) + (-R - d + r)*(-R + d + r)*(R + d + r)/(2*S))**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)
After substituting S^2 = Delta: ((-R/2 + r/2)*(-S/(2*d) + (-R - d + r)*(-R + d + r)*(R + d + r)/(2*S)) - (-d*(R - d + r)*(R + d + r)/(2*S) - (-R - d + r)*(-R + d + r)*(R - d + r)/(2*S))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2 - ((d/2 - (-R**2 + d**2 + r**2)/(2*d))**2 + (S/(2*d) - d*(R - d + r)*(R + d + r)/(2*S))**2)*((-S/(2*d) + (-R - d + r)*(-R + d + r)*(R + d + r)/(2*S))**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)
Simplified: (S**2*d**2*((R - r)*(S**2 + d*(-R + d + r)*(R + d - r)*(R + d + r)) + (d*(R + d + r) - (-R + d + r)*(R + d - r))*(R - d + r)*(R**2 - d**2 + d*(R + d - r) - r**2))**2 - (S**2*(R**2 - r**2)**2 + (S**2 - d**2*(R - d + r)*(R + d + r))**2)*(S**2*(R**2 - d**2 + d*(R + d - r) - r**2)**2 + (S**2 + d*(-R + d + r)*(R + d - r)*(R + d + r))**2))/(16*S**4*d**4)
Not zero, factor: -(R**4 - 2*R**2*d**2 - 2*R**2*r**2 + S**2 + d**4 - 2*d**2*r**2 + r**4)*(R**6*d**6 + 2*R**5*S**2*d**3 + 2*R**5*d**7 + 2*R**5*d**6*r + R**4*S**4 + 2*R**4*S**2*d**4 - 14*R**4*S**2*d**3*r - R**4*d**8 + 2*R**4*d**7*r - R**4*d**6*r**2 - 4*R**3*S**2*d**5 - 16*R**3*S**2*d**4*r + 12*R**3*S**2*d**3*r**2 - 4*R**3*d**9 - 4*R**3*d**8*r - 4*R**3*d**7*r**2 - 4*R**3*d**6*r**3 - 2*R**2*S**4*d**2 - 2*R**2*S**4*r**2 - 3*R**2*S**2*d**6 - 4*R**2*S**2*d**5*r + 28*R**2*S**2*d**4*r**2 + 12*R**2*S**2*d**3*r**3 - R**2*d**10 - 4*R**2*d**9*r - 6*R**2*d**8*r**2 - 4*R**2*d**7*r**3 - R**2*d**6*r**4 + 2*R*S**4*d**3 + 4*R*S**2*d**7 + 2*R*S**2*d**6*r - 4*R*S**2*d**5*r**2 - 16*R*S**2*d**4*r**3 - 14*R*S**2*d**3*r**4 + 2*R*d**11 + 2*R*d**10*r - 4*R*d**9*r**2 - 4*R*d**8*r**3 + 2*R*d**7*r**4 + 2*R*d**6*r**5 + S**6 + 3*S**4*d**4 + 2*S**4*d**3*r - 2*S**4*d**2*r**2 + S**4*r**4 + 3*S**2*d**8 + 4*S**2*d**7*r - 3*S**2*d**6*r**2 - 4*S**2*d**5*r**3 + 2*S**2*d**4*r**4 + 2*S**2*d**3*r**5 + d**12 + 2*d**11*r - d**10*r**2 - 4*d**9*r**3 - d**8*r**4 + 2*d**7*r**5 + d**6*r**6)/(16*S**4*d**4)

```
stderr:
```
```

exit_code: 0
duration_ms: 274
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 18192
stdout:
```
Expression before substitution: ((-R/2 + r/2)*(-y0 + (-R - d + r)*(-R + d + r)*(R + d + r)/(2*sqrt((-d**2 + (R + r)**2)*(d**2 - (R - r)**2)))) - (-d*(R - d + r)*(R + d + r)/(2*sqrt((-d**2 + (R + r)**2)*(d**2 - (R - r)**2))) - (-R - d + r)*(-R + d + r)*(R - d + r)/(2*sqrt((-d**2 + (R + r)**2)*(d**2 - (R - r)**2))))*(R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d)))**2 - ((d/2 - (-R**2 + d**2 + r**2)/(2*d))**2 + (-d*(R - d + r)*(R + d + r)/(2*sqrt((-d**2 + (R + r)**2)*(d**2 - (R - r)**2))) + y0)**2)*((-y0 + (-R - d + r)*(-R + d + r)*(R + d + r)/(2*sqrt((-d**2 + (R + r)**2)*(d**2 - (R - r)**2))))**2 + (R/2 + d/2 - r/2 - (-R**2 + d**2 + r**2)/(2*d))**2)
Simplifying...
Simplified expression: (-d**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(d*(R - r)*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r)) + (d*(R + d + r) - (-R + d + r)*(R + d - r))*(R - d + r)*(R**2 - d**2 + d*(R + d - r) - r**2))**2 - (-d**2*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r))**2 + (d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(R**2 - d**2 + d*(R + d - r) - r**2)**2)*(-d**2*(d*(R - d + r)*(R + d + r) - 2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))**2 + (R**2 - r**2)**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))/(16*d**4*(d**2 - (R - r)**2)**2*(d**2 - (R + r)**2)**2)
Expression times Delta: (d**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(d*(R - r)*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r)) + (d*(R + d + r) - (-R + d + r)*(R + d - r))*(R - d + r)*(R**2 - d**2 + d*(R + d - r) - r**2))**2 + (d**2*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r))**2 - (d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(R**2 - d**2 + d*(R + d - r) - r**2)**2)*(d**2*(d*(R - d + r)*(R + d + r) - 2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))**2 - (R**2 - r**2)**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))/(16*d**4*(d**2 - (R - r)**2)*(d**2 - (R + r)**2))
After substituting x0: (d**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(d*(R - r)*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r)) + (d*(R + d + r) - (-R + d + r)*(R + d - r))*(R - d + r)*(R**2 - d**2 + d*(R + d - r) - r**2))**2 + (d**2*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r))**2 - (d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(R**2 - d**2 + d*(R + d - r) - r**2)**2)*(d**2*(d*(R - d + r)*(R + d + r) - 2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))**2 - (R**2 - r**2)**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))/(16*d**4*(d**2 - (R - r)**2)*(d**2 - (R + r)**2))
Final: (d**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(d*(R - r)*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r)) + (d*(R + d + r) - (-R + d + r)*(R + d - r))*(R - d + r)*(R**2 - d**2 + d*(R + d - r) - r**2))**2 + (d**2*(2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)) + (-R + d + r)*(R + d - r)*(R + d + r))**2 - (d**2 - (R - r)**2)*(d**2 - (R + r)**2)*(R**2 - d**2 + d*(R + d - r) - r**2)**2)*(d**2*(d*(R - d + r)*(R + d + r) - 2*y0*sqrt(-(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))**2 - (R**2 - r**2)**2*(d**2 - (R - r)**2)*(d**2 - (R + r)**2)))/(16*d**4*(d**2 - (R - r)**2)*(d**2 - (R + r)**2))
Not zero, factor: (R + d + r)*(R**11 + R**10*d - R**10*r - 2*R**9*d**2 - 2*R**9*d*r - 5*R**9*r**2 - 4*R**8*d**3 + 2*R**8*d**2*r - 3*R**8*d*r**2 + 5*R**8*r**3 - R**7*d**4 + 20*R**7*d**3*r + 4*R**7*d**2*r**2 + 8*R**7*d**2*y0**2 + 8*R**7*d*r**3 + 10*R**7*r**4 + 5*R**6*d**5 + R**6*d**4*r - 24*R**6*d**3*r**2 - 4*R**6*d**2*r**3 - 8*R**6*d**2*r*y0**2 + 4*R**6*d**2*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 2*R**6*d*r**4 - 10*R**6*r**5 + 5*R**5*d**6 - 34*R**5*d**5*r + 3*R**5*d**4*r**2 - 20*R**5*d**4*y0**2 - 20*R**5*d**3*r**3 + 8*R**5*d**3*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 24*R**5*d**2*r**2*y0**2 - 8*R**5*d**2*r*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 12*R**5*d*r**5 - 10*R**5*r**6 - R**4*d**7 - 3*R**4*d**6*r + 59*R**4*d**5*r**2 - 20*R**4*d**5*y0**2 - 3*R**4*d**4*r**3 + 28*R**4*d**4*r*y0**2 - 4*R**4*d**4*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 56*R**4*d**3*r**4 - 8*R**4*d**3*r*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 24*R**4*d**2*r**3*y0**2 - 4*R**4*d**2*r**2*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 2*R**4*d*r**6 + 10*R**4*r**7 - 4*R**3*d**8 + 16*R**3*d**7*r - 2*R**3*d**6*r**2 + 12*R**3*d**6*y0**2 - 60*R**3*d**5*r**3 + 16*R**3*d**5*r*y0**2 - 12*R**3*d**5*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 3*R**3*d**4*r**4 - 8*R**3*d**4*r**2*y0**2 + 32*R**3*d**4*r*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 16*R**3*d**4*y0**4 - 20*R**3*d**3*r**5 - 4*R**3*d**2*r**6 + 24*R**3*d**2*r**4*y0**2 + 16*R**3*d**2*r**3*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 8*R**3*d*r**7 + 5*R**3*r**8 - 2*R**2*d**9 - 30*R**2*d**7*r**2 + 44*R**2*d**7*y0**2 - 2*R**2*d**6*r**3 - 28*R**2*d**6*r*y0**2 - 8*R**2*d**6*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 59*R**2*d**5*r**4 + 8*R**2*d**5*r**2*y0**2 + 12*R**2*d**5*r*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 16*R**2*d**5*y0**4 + 3*R**2*d**4*r**5 - 8*R**2*d**4*r**3*y0**2 - 56*R**2*d**4*r**2*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 16*R**2*d**4*r*y0**4 + 16*R**2*d**4*y0**3*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 24*R**2*d**3*r**6 + 4*R**2*d**2*r**7 - 24*R**2*d**2*r**5*y0**2 - 4*R**2*d**2*r**4*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 3*R**2*d*r**8 - 5*R**2*r**9 + R*d**10 + 16*R*d**7*r**3 - 8*R*d**7*r*y0**2 + 4*R*d**7*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 3*R*d**6*r**4 - 28*R*d**6*r**2*y0**2 - 16*R*d**6*y0**4 - 34*R*d**5*r**5 + 16*R*d**5*r**3*y0**2 + 12*R*d**5*r**2*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 32*R*d**5*r*y0**4 + 16*R*d**5*y0**3*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + R*d**4*r**6 + 28*R*d**4*r**4*y0**2 + 32*R*d**4*r**3*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 16*R*d**4*r**2*y0**4 - 32*R*d**4*r*y0**3*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 20*R*d**3*r**7 - 8*R*d**3*r**4*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 2*R*d**2*r**8 - 8*R*d**2*r**6*y0**2 - 8*R*d**2*r**5*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 2*R*d*r**9 - R*r**10 + d**11 + d**10*r - 2*d**9*r**2 - 24*d**9*y0**2 - 4*d**8*r**3 + 8*d**8*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - d**7*r**4 + 44*d**7*r**2*y0**2 + 4*d**7*r*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 16*d**7*y0**4 + 5*d**6*r**5 + 12*d**6*r**3*y0**2 - 8*d**6*r**2*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 16*d**6*r*y0**4 - 32*d**6*y0**3*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 5*d**5*r**6 - 20*d**5*r**4*y0**2 - 12*d**5*r**3*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 16*d**5*r**2*y0**4 + 16*d**5*r*y0**3*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - d**4*r**7 - 20*d**4*r**5*y0**2 - 4*d**4*r**4*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + 16*d**4*r**3*y0**4 + 16*d**4*r**2*y0**3*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 4*d**3*r**8 + 8*d**3*r**5*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) - 2*d**2*r**9 + 8*d**2*r**7*y0**2 + 4*d**2*r**6*y0*sqrt(-R**4 + 2*R**2*d**2 + 2*R**2*r**2 - d**4 + 2*d**2*r**2 - r**4) + d*r**10 + r**11)/(16*d**4)

```
stderr:
```
```

exit_code: 0
duration_ms: 437
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 406
stdout:
```
H_y_author -0.3454246398538787
H_y computed -0.34542463985387867
difference -5.551115123125783e-17

```
stderr:
```
```

exit_code: 0
duration_ms: 506
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 362
stdout:
```
O_y_author -0.9046835805696823
center_BEF (1.25, -0.9046835805696822)
difference O_y - center.y -1.1102230246251565e-16

```
stderr:
```
```

exit_code: 0
duration_ms: 344
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 275
stdout:
```
Delta 14.4375
sqrt_Delta 3.799671038392666
P_y_author -3.799671038392666
p_y -3.7996710383926664
difference -4.440892098500626e-16

```
stderr:
```
```

exit_code: 0
duration_ms: 246
stdout:
```

```
stderr:
```
```

exit_code: 0
duration_ms: 463
stdout:
```
x_A,y_A 0.65 0.7599342076785331
m 1.75
p_y -3.7996710383926664
dx,dy 1.1 -4.559605246071199
tE computed 0.24999999999999997
T 0.5
T/R 0.25
difference -2.7755575615628914e-17

```
stderr:
```
```

exit_code: 0
duration_ms: 247
stdout:
```

```
stderr:
```
```

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]
abstract = We prove the theorem using coordinate geometry. Assign coordinates, compute points, show that line through H parallel to AP is tangent to circumcircle of BEF.

## Introduction

We consider two circles $\Omega$ (center $M$, radius $r$) and $\Gamma$ (center $N$, radius $R$) with $r < R$ intersecting at two distinct points $A$ and $B$.
Let $C$ be the intersection of line $MN$ with $\Omega$ and $D$ the intersection with $\Gamma$ such that $C,M,N,D$ lie in that order.
Let $P$ be the circumcenter of $\triangle ACD$.
Line $AP$ meets $\Omega$ again at $E$ and $\Gamma$ again at $F$.
Let $H$ be the orthocenter of $\triangle PMN$.
We prove that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.

## Coordinate setup

Place $M = (0,0)$ and $N = (d,0)$ with $d>0$.
Let $r0$.
A computation gives
\[
P = \Bigl(\frac{d+R-r}{2},\;
\frac{- (R+d-r)(d+r-R)(R+d+r)}{2\sqrt{\Delta}}\Bigr).
\]

## Points $E$ and $F$

Write $T = R+r-d$ (positive under the intersection condition).
The line $AP$ can be parametrized as $A + t(P-A)$.
Solving for the second intersection with $\Omega$ yields
\[
t_E = \frac{T}{R},
\]
and with $\Gamma$ yields
\[
t_F = \frac{T}{r}.
\]
Hence
\[
E = A + \frac{T}{R}(P-A),\qquad
F = A + \frac{T}{r}(P-A).
\]

## Circumcenter $O$ of $\triangle BEF$

By symmetry the circumcenter lies on the $x$-axis; its $x$-coordinate is $d/2$.
Its $y$-coordinate is
\[
O_y = \frac{-d\,T\,(R+d+r)}{2\sqrt{\Delta}}.
\]

The circumradius $R_{BEF}$ satisfies
\[
R_{BEF}^{2}=|O-E|^{2}=|O-B|^{2}.
\]

## Orthocenter $H$ of $\triangle PMN$

Since $M$ and $N$ lie on the $x$-axis, the orthocenter $H$ has the same $x$-coordinate as $P$,
\[
H_x = \frac{d+R-r}{2},
\]
and
\[
H_y = \frac{- (R+d-r)(d+r-R)T}{2\sqrt{\Delta}}.
\]

## The line $L$ through $H$ parallel to $AP$

Let $\mathbf v = P-A$ be the direction vector of $AP$.
The line $L$ consists of points $H + s\mathbf v$ ($s\in\mathbb R$).

## Tangency condition

For $L$ to be tangent to the circle $(BEF)$ it is necessary and sufficient that the distance from $O$ to $L$ equals the radius $R_{BEF}$.
Equivalently,
\[
\frac{\bigl|(O-H)\times \mathbf v\bigr|}{|\mathbf v|}=R_{BEF},
\]
where $\times$ denotes the two‑dimensional cross product (determinant).

Both sides are positive; squaring gives an algebraic identity in the parameters $d,r,R$.
After substituting the expressions for all points and simplifying, the identity reduces to
\[
\bigl((O-H)\times \mathbf v\bigr)^{2}=R_{BEF}^{2}\;|\mathbf v|^{2}.
\]

A direct computer‑algebra calculation (carried out with SymPy) shows that the difference of the two sides simplifies to zero, using only the relation $\Delta = (d^{2}-(R-r)^{2})((R+r)^{2}-d^{2})$.
Hence the equality holds whenever the two circles intersect, i.e. whenever $\Delta>0$.

## Conclusion

We have verified algebraically that the line through $H$ parallel to $AP$ is tangent to the circumcircle of $\triangle BEF$.
All steps are elementary and the final verification is a polynomial identity that can be checked by any computer algebra system.

*Remark.* The same proof can be formalized in a proof assistant such as Lean by expressing the coordinates as functions of $d,r,R$ and using the `ring` tactic to normalise the polynomial identity.


(reviews are hidden until publication/rejection)

reference=[q0i2]
title=An Analytic Proof of a Geometry Theorem on Two Intersecting Circles
author=bdpk
reviews:PENDING, PENDING, PENDING, PENDING
status=SUBMITTED
citations_count=0
attachments=[]

exit_code: 124
duration_ms: 30262
stdout:
```
Py = (s**4 + 2*s**3*t - 2*s**2*t - 2*s**2 - 2*s*t**3 - 4*s*t**2 - 2*s*t - t**4 - 2*t**3 + 4*t**2*y**2 + 2*t + 1)/(8*t**2*y)

```
stderr:
```
```

exit_code: 0
duration_ms: 254
stdout:
```

```
stderr:
```
```