Casey's theorem
TheoremCasey's theorem#✓fully proved
In the Euclidean plane, let a circle have center \(O\) and radius \(R > 0\), and let four circles have centers \(c_1, c_2, c_3, c_4\) and radii \(r_1, r_2, r_3, r_4\) with \(0 < r_i < R\) and \(|c_i O| + r_i = R\) for each \(i\), so that each is internally tangent to the outer circle. Assume that the four circles lie outside each other, \(r_i + r_j < |c_i c_j|\) for all \(i \ne j\), and that they appear counterclockwise around \(O\) with every consecutive angular gap less than \(\pi\): writing \(u \times v = u_1 v_2 - u_2 v_1\) for vectors \(u = (u_1, u_2)\) and \(v = (v_1, v_2)\) of the plane, \((c_i - O) \times (c_j - O) > 0\) for \((i, j) = (1, 2), (2, 3), (3, 4), (4, 1)\). For the pairs \(ij = 12, 23, 34, 41, 13, 24\) let \(t_{ij} > 0\) satisfy \(t_{ij}^2 = |c_i c_j|^2 - (r_i - r_j)^2\), the length of an exterior common tangent of the circles \(i\) and \(j\). Then \(t_{12} t_{34} + t_{23} t_{41} = t_{13} t_{24}\).
Configurations with a consecutive angular gap of at least \(\pi\) are not covered here; they are covered by the cyclic-order form of Casey's theorem.
MetaMathlibExt.casey_theorem · 28 lines
theorem casey_theorem {O c1 c2 c3 c4 : EuclideanSpace ℝ (Fin 2)}
{R r1 r2 r3 r4 t12 t23 t34 t41 t13 t24 : ℝ}
(hR : 0 < R)
(hr1 : 0 < r1) (hr2 : 0 < r2) (hr3 : 0 < r3) (hr4 : 0 < r4)
(hlt1 : r1 < R) (hlt2 : r2 < R) (hlt3 : r3 < R) (hlt4 : r4 < R)
(hinner1 : dist c1 O + r1 = R)
(hinner2 : dist c2 O + r2 = R)
(hinner3 : dist c3 O + r3 = R)
(hinner4 : dist c4 O + r4 = R)
(hdisj12 : r1 + r2 < dist c1 c2)
(hdisj23 : r2 + r3 < dist c2 c3)
(hdisj34 : r3 + r4 < dist c3 c4)
(hdisj41 : r4 + r1 < dist c4 c1)
(hdisj13 : r1 + r3 < dist c1 c3)
(hdisj24 : r2 + r4 < dist c2 c4)
(ht12 : t12 ^ 2 = dist c1 c2 ^ 2 - (r1 - r2) ^ 2)
(ht23 : t23 ^ 2 = dist c2 c3 ^ 2 - (r2 - r3) ^ 2)
(ht34 : t34 ^ 2 = dist c3 c4 ^ 2 - (r3 - r4) ^ 2)
(ht41 : t41 ^ 2 = dist c4 c1 ^ 2 - (r4 - r1) ^ 2)
(ht13 : t13 ^ 2 = dist c1 c3 ^ 2 - (r1 - r3) ^ 2)
(ht24 : t24 ^ 2 = dist c2 c4 ^ 2 - (r2 - r4) ^ 2)
(ht12pos : 0 < t12) (ht23pos : 0 < t23) (ht34pos : 0 < t34)
(ht41pos : 0 < t41) (ht13pos : 0 < t13) (ht24pos : 0 < t24)
(hcyc12 : 0 < ((c1 - O).ofLp 0 * (c2 - O).ofLp 1 - (c1 - O).ofLp 1 * (c2 - O).ofLp 0))
(hcyc23 : 0 < ((c2 - O).ofLp 0 * (c3 - O).ofLp 1 - (c2 - O).ofLp 1 * (c3 - O).ofLp 0))
(hcyc34 : 0 < ((c3 - O).ofLp 0 * (c4 - O).ofLp 1 - (c3 - O).ofLp 1 * (c4 - O).ofLp 0))
(hcyc41 : 0 < ((c4 - O).ofLp 0 * (c1 - O).ofLp 1 - (c4 - O).ofLp 1 * (c1 - O).ofLp 0))
: t12 * t34 + t23 * t41 = t13 * t24Sources
- https://en.wikipedia.org/wiki/Casey%27s_theorem.
TheoremCore identity behind Casey's theorem in cyclic order#✓fully proved
In the Euclidean plane, write \(d(p, q)\) for the distance between points \(p\) and \(q\). Let \(O, c_1, c_2, c_3, c_4\) be points and \(R, r_1, r_2, r_3, r_4\) real numbers with \(r_i < R\) and \(d(c_i, O) + r_i = R\) for each \(i\). Suppose \(c_i - O = d(c_i, O)(\cos\theta_i, \sin\theta_i)\) for real numbers \(\theta_1 < \theta_2 < \theta_3 < \theta_4 < \theta_1 + 2\pi\). For each pair \((i, j)\) among \((1, 2), (2, 3), (3, 4), (4, 1), (1, 3), (2, 4)\) let \(t_{ij} > 0\) satisfy \(t_{ij}^2 = d(c_i, c_j)^2 - (r_i - r_j)^2\). Then \(t_{12} t_{34} + t_{23} t_{41} = t_{13} t_{24}\).
Compared with Casey's theorem for four circles in arbitrary cyclic order, neither \(R\) nor the \(r_i\) need be positive and the circles need not be pairwise disjoint.
MetaMathlibExt.casey_theorem_cyclic_order_core · 21 lines
theorem casey_theorem_cyclic_order_core {O c1 c2 c3 c4 : EuclideanSpace ℝ (Fin 2)}
{R r1 r2 r3 r4 t12 t23 t34 t41 t13 t24 θ1 θ2 θ3 θ4 : ℝ}
(hlt1 : r1 < R) (hlt2 : r2 < R) (hlt3 : r3 < R) (hlt4 : r4 < R)
(hinner1 : dist c1 O + r1 = R)
(hinner2 : dist c2 O + r2 = R)
(hinner3 : dist c3 O + r3 = R)
(hinner4 : dist c4 O + r4 = R)
(ht12 : t12 ^ 2 = dist c1 c2 ^ 2 - (r1 - r2) ^ 2)
(ht23 : t23 ^ 2 = dist c2 c3 ^ 2 - (r2 - r3) ^ 2)
(ht34 : t34 ^ 2 = dist c3 c4 ^ 2 - (r3 - r4) ^ 2)
(ht41 : t41 ^ 2 = dist c4 c1 ^ 2 - (r4 - r1) ^ 2)
(ht13 : t13 ^ 2 = dist c1 c3 ^ 2 - (r1 - r3) ^ 2)
(ht24 : t24 ^ 2 = dist c2 c4 ^ 2 - (r2 - r4) ^ 2)
(ht12pos : 0 < t12) (ht23pos : 0 < t23) (ht34pos : 0 < t34)
(ht41pos : 0 < t41) (ht13pos : 0 < t13) (ht24pos : 0 < t24)
(hθ12 : θ1 < θ2) (hθ23 : θ2 < θ3) (hθ34 : θ3 < θ4) (hθ41 : θ4 < θ1 + 2 * Real.pi)
(hc1 : c1 - O = dist c1 O • !₂[Real.cos θ1, Real.sin θ1])
(hc2 : c2 - O = dist c2 O • !₂[Real.cos θ2, Real.sin θ2])
(hc3 : c3 - O = dist c3 O • !₂[Real.cos θ3, Real.sin θ3])
(hc4 : c4 - O = dist c4 O • !₂[Real.cos θ4, Real.sin θ4])
: t12 * t34 + t23 * t41 = t13 * t24Used by 1
TheoremCasey's theorem for four circles in arbitrary cyclic order#✓fully proved
In the Euclidean plane, write \(d(p, q)\) for the distance between points \(p\) and \(q\). Let \(O\) be a point and \(R > 0\), and let \(c_1, c_2, c_3, c_4\) be points and \(r_1, r_2, r_3, r_4\) real numbers with \(0 < r_i < R\) and \(d(c_i, O) + r_i = R\) for each \(i\), so that the circle with center \(c_i\) and radius \(r_i\) is internally tangent to the circle with center \(O\) and radius \(R\). Suppose any two of the four inner circles are disjoint, that is \(r_i + r_j < d(c_i, c_j)\) for \(i \ne j\), and that \(c_i - O = d(c_i, O)(\cos\theta_i, \sin\theta_i)\) for real numbers \(\theta_1 < \theta_2 < \theta_3 < \theta_4 < \theta_1 + 2\pi\). For each pair \((i, j)\) among \((1, 2), (2, 3), (3, 4), (4, 1), (1, 3), (2, 4)\) let \(t_{ij} > 0\) satisfy \(t_{ij}^2 = d(c_i, c_j)^2 - (r_i - r_j)^2\), so that \(t_{ij}\) is the length of an outer common tangent. Then \(t_{12} t_{34} + t_{23} t_{41} = t_{13} t_{24}\).
Unlike the version of Casey's theorem that requires each consecutive pair of centers to make a positive oriented angle at \(O\), a gap between consecutive directions may be at least \(\pi\).
MetaMathlibExt.casey_theorem_cyclic_order · 29 lines
theorem casey_theorem_cyclic_order {O c1 c2 c3 c4 : EuclideanSpace ℝ (Fin 2)}
{R r1 r2 r3 r4 t12 t23 t34 t41 t13 t24 θ1 θ2 θ3 θ4 : ℝ}
(hR : 0 < R)
(hr1 : 0 < r1) (hr2 : 0 < r2) (hr3 : 0 < r3) (hr4 : 0 < r4)
(hlt1 : r1 < R) (hlt2 : r2 < R) (hlt3 : r3 < R) (hlt4 : r4 < R)
(hinner1 : dist c1 O + r1 = R)
(hinner2 : dist c2 O + r2 = R)
(hinner3 : dist c3 O + r3 = R)
(hinner4 : dist c4 O + r4 = R)
(hdisj12 : r1 + r2 < dist c1 c2)
(hdisj23 : r2 + r3 < dist c2 c3)
(hdisj34 : r3 + r4 < dist c3 c4)
(hdisj41 : r4 + r1 < dist c4 c1)
(hdisj13 : r1 + r3 < dist c1 c3)
(hdisj24 : r2 + r4 < dist c2 c4)
(ht12 : t12 ^ 2 = dist c1 c2 ^ 2 - (r1 - r2) ^ 2)
(ht23 : t23 ^ 2 = dist c2 c3 ^ 2 - (r2 - r3) ^ 2)
(ht34 : t34 ^ 2 = dist c3 c4 ^ 2 - (r3 - r4) ^ 2)
(ht41 : t41 ^ 2 = dist c4 c1 ^ 2 - (r4 - r1) ^ 2)
(ht13 : t13 ^ 2 = dist c1 c3 ^ 2 - (r1 - r3) ^ 2)
(ht24 : t24 ^ 2 = dist c2 c4 ^ 2 - (r2 - r4) ^ 2)
(ht12pos : 0 < t12) (ht23pos : 0 < t23) (ht34pos : 0 < t34)
(ht41pos : 0 < t41) (ht13pos : 0 < t13) (ht24pos : 0 < t24)
(hθ12 : θ1 < θ2) (hθ23 : θ2 < θ3) (hθ34 : θ3 < θ4) (hθ41 : θ4 < θ1 + 2 * Real.pi)
(hc1 : c1 - O = dist c1 O • !₂[Real.cos θ1, Real.sin θ1])
(hc2 : c2 - O = dist c2 O • !₂[Real.cos θ2, Real.sin θ2])
(hc3 : c3 - O = dist c3 O • !₂[Real.cos θ3, Real.sin θ3])
(hc4 : c4 - O = dist c4 O • !₂[Real.cos θ4, Real.sin θ4])
: t12 * t34 + t23 * t41 = t13 * t24Sources
- https://en.wikipedia.org/wiki/Casey%27s_theorem
Uses 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.