English
The square of the distance from the second intersection point to the center equals the square of the distance from the original point to the center: dist(s.secondInter(p,t), center)^2 = dist(p,center)^2.
Русский
Квадрат расстояния между второй точкой пересечения и центром равен квадрату расстояния между исходной точкой и центром: dist(вторая_пересечение, центр)^2 = dist(исходная_точка, центр)^2.
LaTeX
$$$\\operatorname{dist}(s.\\mathrm{secondInter}(p,t), s.center)^2 = \\operatorname{dist}(p, s.center)^2$$$
Lean4
/-- The second intersection of a sphere with a line through a point on that sphere; that point
if it is the only point of intersection of the line with the sphere. The intended use of this
definition is when `p ∈ s`; the definition does not use `s.radius`, so in general it returns
the second intersection with the sphere through `p` and with center `s.center`. -/
def secondInter (s : Sphere P) (p : P) (v : V) : P :=
(-2 * ⟪v, p -ᵥ s.center⟫ / ⟪v, v⟫) • v +ᵥ p
