English
The distance along a chord relates to the sphere radius via the center-centered angle and the sine or cosine of the base angles.
Русский
Расстояние между двумя точками на окружности связано с радиусом сферы через угол в центре и синус/косинус базовых углов.
LaTeX
$$$\\text{dist}(p_1,p_2) = 2\\,\\text{radius}\\, \\sin(\\angle p_1 p_2 s.center)$$$
Lean4
/-- Given two points on a circle, the center of that circle may be expressed explicitly as a
multiple (by half the tangent of the angle between the chord and the radius at one of those
points) of a `π / 2` rotation of the vector between those points, plus the midpoint of those
points. -/
theorem tan_div_two_smul_rotation_pi_div_two_vadd_midpoint_eq_center {s : Sphere P} {p₁ p₂ : P} (hp₁ : p₁ ∈ s)
(hp₂ : p₂ ∈ s) (h : p₁ ≠ p₂) :
(Real.Angle.tan (∡ p₂ p₁ s.center) / 2) • «o».rotation (π / 2 : ℝ) (p₂ -ᵥ p₁) +ᵥ midpoint ℝ p₁ p₂ = s.center :=
by
obtain ⟨r, hr⟩ :=
(dist_eq_iff_eq_smul_rotation_pi_div_two_vadd_midpoint h).1 (dist_center_eq_dist_center_of_mem_sphere hp₁ hp₂)
rw [← hr, ← oangle_midpoint_rev_left, oangle, vadd_vsub_assoc]
nth_rw 1 [show p₂ -ᵥ p₁ = (2 : ℝ) • (midpoint ℝ p₁ p₂ -ᵥ p₁) by simp]
rw [map_smul, smul_smul, add_comm, «o».tan_oangle_add_right_smul_rotation_pi_div_two,
mul_div_cancel_right₀ _ (two_ne_zero' ℝ)]
simpa using h.symm
