Commit 2026-03-11 03:16 0f1d0fb1

feat(Geometry.Euclidean.Sphere): inner product of chord with radius vector is negative (#36241) For distinct points A and B on a sphere, the inner product ⟪B -ᵥ A, A -ᵥ s.center⟫ is negative. This is a natural companion to the existing inner_pos_of_dist_lt_radius and inner_nonneg_of_dist_le_radius.