Problem (2ndFNGOp9): For fixed $a>0$, let circles $c_1,c_2,c_3$ be centered at $A,B,C$ with radius $a$. Points $D,E$ lie on the circumcircle of $\triangle ABC$, with $F$ as the midpoint of arc $DE$. Rays $EA,DA$ meet $c_1,c_2$ at $A_1,A_2$ respectively with $FA_1=FA_2$ (similarly define $B_1,B_2,C_1,C_2$). Prove that for any $a$ and $D,E$, the radical axis of the circumcircles of $\triangle A_1B_1C_1$ and $\triangle A_2B_2C_2$ always passes through either the incenter or one excenter of $\triangle ABC$.
AlphaGeometry formalization: a b c = triangle; e = on_circum a b c; f = on_circum a b c; a1 = on_line a e; a2 = reflect a1 a f; b1 = on_line b e, eqdistance b1 b a a1; b2 = reflect b1 b f; c1 = on_line c e, eqdistance c1 c a a1; c2 = reflect c1 c f; x = on_circum a1 b1 c1, on_circum a2 b2 c2; y = on_circum a1 b1 c1, on_circum a2 b2 c2; i = incenter a b c ? coll x y i
HAGeo formalization: A B C = triangle; (ABC) = circle A B C; E = on_circle (ABC); F = on_circle (ABC); AE = line A E; A1 = on_line AE; AF = line A F; A2 = reflect_point_wrt_line A1 AF; BE = line B E; (B) = circle_center_radius B A A1; B1 = intersection BE (B); BF = line B F; B2 = reflect_point_wrt_line B1 BF; CE = line C E; (C) = circle_center_radius C A A1; C1 = intersection CE (C); CF = line C F; C2 = reflect_point_wrt_line C1 CF; (A1B1C1) = circumcircle A1 B1 C1; (A2B2C2) = circumcircle A2 B2 C2; X Y = intersection (A1B1C1) (A2B2C2); I = incenter A B C; Prove: collinear X Y I
Difficulty score: 6.7