Constructive Demonstrations¶
Exact Symbolic geometor.model Constructions & Algebraic Proofs for Casey’s Sequel
In accordance with GEOMETOR’s strict separation of historical text and executable code, all Python constructions and SymPy symbolic proofs reside in src/geometor/casey/ and demos/. Every coordinate below is an exact SymPy Integer, Rational, or closed-form radical over the canonical Heronian reference triangle $\triangle ABC$ with sides $(a, b, c) = (15, 13, 14)$ and vertices $A = (0, 0), B = (14, 0), C = (5, 12)$ (or integer projective lattices)—zero ``float`` or ``sp.Float`` approximations enter any Model.
1. Casey’s Generalized Ptolemy Theorem & Feuerbach’s Nine-Point Tangency¶
Executes demos/casey_feuerbach.py (geometor.casey.feuerbach), proving Casey’s bitangent relation symbolically and constructing both the Euler Line & Nine-Points Circle (Unit 1, Book IV Prop. 5) and Casey’s Orthogonal Inversion Proof of Feuerbach’s Theorem at $F_e = X(11) = (6, 8)$ (Unit 4, Book VI Sec. IV Props. 9–10 & Cor. 2):
Exact Centres & Radii on $(15, 13, 14)$: $\Delta = 84$, $r = 4$, $R = \frac{65}{8}$, $R_9 = \frac{65}{16}$, $O = \left(7, \frac{33}{8}\right)$, $G = \left(\frac{19}{3}, 4\right)$, $N = \left(6, \frac{63}{16}\right)$, $H = \left(5, \frac{15}{4}\right)$, $I = (6, 4)$.
Exact Feuerbach Tangency: $|NI| = \frac{1}{16} = \frac{65}{16} - 4 = R_9 - r$, touching internally at $F_e = X(11) = (6, 8)$, and touching the three excircles externally at $\left(\frac{2709}{289}, \frac{1792}{289}\right)$, $\left(\frac{553}{233}, \frac{1344}{233}\right)$, and $\left(\frac{1672}{257}, -\frac{24}{257}\right)$.
Casey’s 1861 Inversion Circle: Circle $(M_a, T_a)$ centered at $M_a = \left(\frac{19}{2}, 6\right)$ of radius $\frac{1}{2} = \frac{|b - c|}{2}$ cuts both the incircle $(I, 4)$ and $A$-excircle $(I_a, 14)$ orthogonally and inverts $T_s = \left(\frac{614}{65}, \frac{392}{65}\right)$ on the fourth common tangent directly onto $F_e = (6, 8)$.
"""Demo 1: Casey's Generalized Ptolemy Theorem & Feuerbach's Nine-Point Tangency (Units 1 & 4).
Verifies:
1. Universal polynomial proof of Casey's bitangent relation ``t_12*t_34 + t_14*t_23 = t_13*t_24``
under circular inversion (Book VI, Sec. IV, Props. 9–10, pp. 102–104).
2. Universal ``(a, b, c)`` bitangent identities for both the incircle and the excircles
(Prop. 10, Cor. 2, pp. 104–105).
3. Exact compass-and-straightedge construction on the Heronian ``(15, 13, 14)`` triangle,
confirming Casey's 1861 orthogonal inversion circle ``(Ma, 1/2)`` and tangency at the
Feuerbach point ``Fe = X(11) = (6, 8)``.
"""
from __future__ import annotations
import sys
from pathlib import Path
_REPO_ROOT = Path(__file__).resolve().parents[1]
for _extra in (_REPO_ROOT / "src", _REPO_ROOT.parent / "model" / "src"):
if _extra.exists() and str(_extra) not in sys.path:
sys.path.insert(0, str(_extra))
from rich.console import Console # noqa: E402
from rich.table import Table # noqa: E402
from geometor.casey import ( # noqa: E402
construct_casey_feuerbach,
construct_euler_nine_point,
export_svg,
prove_casey_feuerbach_heronian,
prove_casey_theorem_symbolic,
)
def run_demo(*, write_svgs: bool = True) -> None:
"""Execute the Casey–Feuerbach symbolic demonstration and optionally export interactive SVGs."""
console = Console()
sym_proof = prove_casey_theorem_symbolic()
heron = prove_casey_feuerbach_heronian()
unit1_res = construct_euler_nine_point()
unit4_res = construct_casey_feuerbach()
tbl_sym = Table(title="Casey's Generalized Ptolemy Theorem — Symbolic Verification (VI.IV.9–10)")
tbl_sym.add_column("Algebraic Identity", style="cyan bold")
tbl_sym.add_column("Residual", style="green")
tbl_sym.add_row("Inversion invariance of t_12^2 / (r_1 r_2) (Prop. 9)", str(sym_proof.inversion_invariance_residual))
tbl_sym.add_row("Collinear contact Euler identity (Prop. 10)", str(sym_proof.tangent_line_euler_residual))
tbl_sym.add_row("Incircle bitangent sum a(c-b)+b(a-c)-c(a-b) (Cor. 2)", str(sym_proof.incircle_casey_residual))
tbl_sym.add_row("Casey Cor. 2 squared difference sum", str(sym_proof.incircle_cor2_squares_residual))
tbl_sym.add_row("A-Excircle bitangent sum a(c-b)+c(a+b)-b(a+c)", str(sym_proof.excircle_a_casey_residual))
console.print(tbl_sym)
tbl_heron = Table(title="Heronian (15, 13, 14) Exact Feuerbach & Bitangent Ledger")
tbl_heron.add_column("Quantity", style="cyan bold")
tbl_heron.add_column("Exact Symbolic Value", style="green")
tbl_heron.add_row("Sides (a, b, c) & Area Δ", f"{heron.sides}, Δ = {heron.area}")
tbl_heron.add_row("Radii (r, R, R_9)", f"r = {heron.inradius}, R = {heron.circumradius}, R_9 = {heron.nine_point_radius}")
tbl_heron.add_row("Exradii (r_a, r_b, r_c)", str(heron.exradii))
tbl_heron.add_row("Midpoint chords (t_23, t_31, t_12)", str(heron.midpoint_chords))
tbl_heron.add_row("Midpoint-to-incircle bitangents (|MaTa|, |MbTb|, |McTc|)", str(heron.incircle_midpoint_tangents))
tbl_heron.add_row("Casey bitangent relation t_23*t_14 + t_31*t_24 - t_12*t_34", str(heron.casey_signed_sum))
tbl_heron.add_row("Centre distance |N I| = R_9 - r", str(heron.ni_distance))
tbl_heron.add_row("Feuerbach Point Fe = X(11)", f"{unit4_res.feuerbach_point} (steps={len(unit4_res.model.steps)})")
tbl_heron.add_row("Excircle Feuerbach Touch Points", str(heron.excircle_feuerbach_points))
tbl_heron.add_row(
"Casey 1861 Circle (Ma, 1/2) Orthogonal to I & I_a",
f"{heron.inversion_circle_orthogonal_to_incircle} & {heron.inversion_circle_orthogonal_to_excircle_a}",
)
console.print(tbl_heron)
if write_svgs:
u1_focus = [
*unit1_res.vertices,
*unit1_res.midpoints,
unit1_res.circumcenter,
unit1_res.orthocenter,
]
for out_u1 in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-1" / "0083.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit1_euler_nine_point.svg",
):
export_svg(
unit1_res.model,
out_u1,
graphic_id="0083.g1",
title="Casey Book IV Prop. 5 — Euler Line & Nine-Points Circle",
bbox=(-2.5, 16.5, -4.6, 13.4),
focus_points=u1_focus,
highlight_point_ids=("O", "G", "N", "H"),
)
for out_u4 in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-4" / "0130.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit4_casey_feuerbach.svg",
):
export_svg(
unit4_res.model,
out_u4,
graphic_id="0130.g1",
title="Casey Book VI Sec. IV Prop. 10 Cor. 2 — Casey's Inversion & Feuerbach Tangency at X(11)",
bbox=(-2.5, 16.5, -4.6, 13.4),
highlight_point_ids=("Fe", "Ma", "I", "N"),
)
if __name__ == "__main__":
run_demo()
2. Radical Axis, Radical Centre & Coaxal Pencil with Poncelet Limiting Points¶
Executes demos/coaxial_pencil_and_limiting_points.py (geometor.casey.coaxial), constructing the radical axis of two non-intersecting circles via an auxiliary secant circle (Casey Book III, Prop. 21, p. 43), verifying Casey’s Fundamental Difference-of-Powers Theorem (Prop. 24), and constructing Poncelet’s Limiting Points $L_1 = (-8, 0), L_2 = (8, 0)$ and the orthogonal circle centered at the Radical Centre $R_c = (0, -6)$ (Book VI, Sec. V, Props. 1–6):
"""Demo 2: Radical Axis, Coaxal System & Poncelet Limiting Points (Unit 2).
Constructs the radical axis of two disjoint circles ``C1=((-10,0), 6)`` and ``C2=((17,0), 15)``
via an auxiliary secant circle ``C_aux=((2,8), 10)`` (Casey Book III, Prop. 28), locates the
Radical Centre ``Rc=(0,-6)``, constructs Poncelet's Limiting Points ``L1=(-8,0), L2=(8,0)``,
and verifies Casey's Fundamental Theorem of Coaxal Circles (Book III, Prop. 24).
"""
from __future__ import annotations
import sys
from pathlib import Path
_REPO_ROOT = Path(__file__).resolve().parents[1]
for _extra in (_REPO_ROOT / "src", _REPO_ROOT.parent / "model" / "src"):
if _extra.exists() and str(_extra) not in sys.path:
sys.path.insert(0, str(_extra))
from rich.console import Console # noqa: E402
from rich.table import Table # noqa: E402
from geometor.casey import ( # noqa: E402
circle_power,
construct_radical_axis_and_coaxial_pencil,
export_svg,
)
def run_demo(*, write_svgs: bool = True) -> None:
"""Execute the Coaxal Pencil & Limiting Points demo and optionally export SVGs."""
console = Console()
res = construct_radical_axis_and_coaxial_pencil()
table = Table(title="Casey Book III Props. 22–28 & VI.V — Coaxal System & Limiting Points")
table.add_column("Element / Invariant", style="cyan bold")
table.add_column("Exact Symbolic Value", style="green")
table.add_row("Primary Disjoint Circles C1, C2", f"C1=({res.c1.center}, r={res.c1.radius}), C2=({res.c2.center}, r={res.c2.radius})")
table.add_row("Third Coaxal Circle C3", f"C3=({res.c3_coaxial.center}, r={res.c3_coaxial.radius})")
table.add_row("Radical Centre Rc (via C_aux)", f"{res.radical_center}, pow(Rc, C1)={circle_power(res.radical_center, res.c1)}")
table.add_row("Radical Axis [Rc D]", f"{res.radical_axis.equation()} = 0, foot D={res.radical_foot}")
table.add_row("C1 Tangent Contact T1 from D", str(res.tangent_contact_c1))
table.add_row("Poncelet Limiting Points (L1, L2)", f"{res.limiting_points[0]}, {res.limiting_points[1]}")
table.add_row(
"Orthogonal Circle (Rc, L1) Cuts C1, C2, C3",
f"{res.report.orthogonal_to_c1}, {res.report.orthogonal_to_c2}, {res.report.orthogonal_to_c3}",
)
table.add_row("Book III Prop. 24 Symbolic Residual", str(res.report.symbolic_prop24_residual))
console.print(table)
if write_svgs:
for out_path in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-2" / "0069.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit2_coaxial_limiting_points.svg",
):
export_svg(
res.model,
out_path,
graphic_id="0069.g1",
title="Casey Book III Props. 23–28 — Disjoint Radical Axis, Orthogonal Pencil & Poncelet Limiting Points",
bbox=(-18.0, 34.0, -17.5, 19.5),
highlight_point_ids=("Rc", "L1", "L2"),
)
if __name__ == "__main__":
run_demo()
3. Complete Quadrilateral Harmonic Ranges, Poles & Polars, and La Hire Reciprocity¶
Executes demos/poles_polars_lahire.py (geometor.casey.poles_polars), demonstrating pure-straightedge projective harmonic division on the Complete Quadrilateral (Book VI, Sec. III, Prop. 7, p. 91) and inscribed-quadrangle polar construction, Self-Conjugate Triangle $\triangle DUV$, harmonic secant division $(G_i, H_i; J_i, D) = -1$, and La Hire’s Reciprocity $Q \in \operatorname{polar}(D) \iff D \in \operatorname{polar}(Q)$ (Book III, Props. 25, 27 & Book VI, Sec. VII):
"""Demo 3: Complete Quadrilateral Harmonic Section, Poles & Polars, and La Hire Reciprocity (Units 3 & 4).
Constructs:
1. Casey Book VI, Sec. III, Prop. 7 (p. 91): Complete Quadrilateral harmonic diagonal ranges.
2. Casey Book III, Props. 25, 27 & Book VI, Sec. VII, Prop. 2: Pure-straightedge inscribed
quadrangle polar construction, Self-Conjugate Triangle ``D U V``, harmonic secant section
``(G, H; J, D) = -1``, and La Hire's Reciprocity ``Q in polar(D) <=> D in polar(Q)``.
"""
from __future__ import annotations
import sys
from pathlib import Path
_REPO_ROOT = Path(__file__).resolve().parents[1]
for _extra in (_REPO_ROOT / "src", _REPO_ROOT.parent / "model" / "src"):
if _extra.exists() and str(_extra) not in sys.path:
sys.path.insert(0, str(_extra))
from rich.console import Console # noqa: E402
from rich.table import Table # noqa: E402
from geometor.casey import ( # noqa: E402
construct_complete_quadrilateral_harmonic,
construct_pole_and_polar,
export_svg,
verify_lahire_reciprocity_symbolic,
)
def run_demo(*, write_svgs: bool = True) -> None:
"""Execute the Complete Quadrilateral & Pole–Polar Reciprocity demo and export SVGs."""
console = Console()
quad = construct_complete_quadrilateral_harmonic()
sym_lh = verify_lahire_reciprocity_symbolic()
pol = construct_pole_and_polar()
tbl_q = Table(title="Casey Book VI Sec. III Prop. 7 — Complete Quadrilateral Harmonic Ranges")
tbl_q.add_column("Element / Cross-Ratio", style="cyan bold")
tbl_q.add_column("Exact Symbolic Value", style="green")
tbl_q.add_row("Opposite Side Meets (E, F)", f"E={quad.opposite_meets[0]}, F={quad.opposite_meets[1]}")
tbl_q.add_row("Internal Diagonal Meet P", str(quad.diagonal_center))
tbl_q.add_row("Third Diagonal Meets (Qa, Qb)", f"Qa={quad.third_diagonal_meets[0]}, Qb={quad.third_diagonal_meets[1]}")
tbl_q.add_row("Cross-Ratios (A,C;P,Qa) & (B,D;P,Qb)", f"{quad.cross_ratio_ac} & {quad.cross_ratio_bd}")
console.print(tbl_q)
tbl_p = Table(title="Casey Book III Prop. 25 & VI.VII — Poles, Polars & La Hire Reciprocity")
tbl_p.add_column("Element / Invariant", style="cyan bold")
tbl_p.add_column("Exact Symbolic Value", style="green")
tbl_p.add_row("Symbolic Bilinear Reciprocity Residual", str(sym_lh.reciprocity_bilinear_diff))
tbl_p.add_row("Pole D & Polar [U V]", f"D={pol.pole_d}, {pol.polar_d.equation()} = 0")
tbl_p.add_row("Self-Conjugate Triangle (D, U, V)", f"{pol.self_conjugate_triangle}")
tbl_p.add_row("Harmonic Secant Cross-Ratios", f"(G1,H1;J1,D)={pol.cross_ratio_secant_1}, (G2,H2;J2,D)={pol.cross_ratio_secant_2}")
tbl_p.add_row("Reciprocal Pole Q on polar(D)", f"Q={pol.reciprocal_pole_q}, polar(Q): {pol.polar_q.equation()} = 0")
tbl_p.add_row("La Hire Reciprocity D in polar(Q)", str(pol.lahire_verified))
console.print(tbl_p)
if write_svgs:
for out_u3 in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-3" / "0117.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit3_complete_quadrilateral_harmonic.svg",
):
export_svg(
quad.model,
out_u3,
graphic_id="0117.g1",
title="Casey Book VI Sec. III Prop. 7 — Complete Quadrilateral Harmonic Section",
bbox=(-7.2, 9.2, -1.2, 10.2),
highlight_point_ids=("P", "Qa", "Qb"),
)
for out_u4 in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-4" / "0071.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit4_poles_polars_lahire.svg",
):
export_svg(
pol.model,
out_u4,
graphic_id="0071.g1",
title="Casey Book III Prop. 25 & VI.VII — Pole, Polar, Self-Conjugate Triangle & La Hire Reciprocity",
bbox=(-6.5, 9.5, -6.5, 11.5),
highlight_point_ids=("D", "Q", "U", "V"),
)
if __name__ == "__main__":
run_demo()
4. Symmedian Point, Lemoine Circles, Brocard Circle & Associated Triangle Points¶
Executes demos/brocard_and_lemoine_circles.py (geometor.casey.brocard), constructing on $\triangle ABC$ $(15, 13, 14)$:
Lemoine’s Symmedian Point $K = X(6) = \left(\frac{1673}{295}, \frac{1176}{295}\right)$ minimizing $\sum d_i^2 = \frac{14112}{295}$, First Lemoine Circle (6 concyclic parallel intercepts, chords proportional to $(a^3 : b^3 : c^3)$), and Cosine (Second Lemoine) Circle (6 concyclic antiparallel intercepts of diameter $2 R \tan\omega$).
Brocard Angle $\cot\omega = \cot A + \cot B + \cot C = \frac{a^2+b^2+c^2}{4\Delta} = \frac{295}{168}$ ($\sin^2\omega = \frac{28224}{115249}$), First & Second Brocard Points $\Omega = \left(\frac{697970}{115249}, \frac{397488}{115249}\right)$ and $\Omega' = \left(\frac{684236}{115249}, \frac{529200}{115249}\right)$, Brocard’s First Triangle $\triangle A_1 B_1 C_1$, and the 7-Point Brocard Circle on diameter $OK$ centered at $M_L = X(182) = \left(\frac{1869}{295}, \frac{19143}{4720}\right)$.
Associated Points: Steiner Point $S_t = X(99) = \left(\frac{17253}{2353}, -\frac{9396}{2353}\right)$, Tarry Point $T_r = X(98) = \left(\frac{15689}{2353}, \frac{115233}{9412}\right)$, and de Longchamps Point $X(20) = \left(9, \frac{9}{2}\right)$.
"""Demo 4: Symmedians, Lemoine Circles, Brocard Points, Brocard Circle & Associated Points (Units 5 & 6).
Constructs on the Heronian ``(15, 13, 14)`` triangle ``A=(0,0), B=(14,0), C=(5,12)``:
1. Lemoine's Symmedian Point ``K = X(6) = (1673/295, 1176/295)`` via circumcircle tangents.
2. First Lemoine Circle (6 side-parallel intersections centered at ``Ml = midpoint(O, K)``)
and Cosine Circle (6 antiparallel intersections centered at ``K``).
3. First & Second Brocard Points ``Ω, Ω'``, Brocard Angle ``cot(ω) = 295/168``, Brocard's First
Triangle ``A1 B1 C1``, and the seven-point **Brocard Circle** on diameter ``OK``.
4. Steiner's Point ``X(99)``, Tarry's Point ``X(98)``, and de Longchamps' Point ``X(20)``.
"""
from __future__ import annotations
import sys
from pathlib import Path
_REPO_ROOT = Path(__file__).resolve().parents[1]
for _extra in (_REPO_ROOT / "src", _REPO_ROOT.parent / "model" / "src"):
if _extra.exists() and str(_extra) not in sys.path:
sys.path.insert(0, str(_extra))
from rich.console import Console # noqa: E402
from rich.table import Table # noqa: E402
from geometor.casey import ( # noqa: E402
construct_brocard_and_lemoine_circles,
construct_symmedian_and_lemoine_circles,
export_svg,
)
def run_demo(*, write_svgs: bool = True) -> None:
"""Execute the Symmedian, Lemoine & Brocard geometry demo and export SVGs."""
console = Console()
lem = construct_symmedian_and_lemoine_circles()
bro = construct_brocard_and_lemoine_circles()
rep = bro.report
table = Table(title="Casey Supplementary Chapter — Exact Rational Lemoine & Brocard Ledger")
table.add_column("Center / Invariant", style="cyan bold")
table.add_column("Exact Rational Expression on (15, 13, 14)", style="green")
table.add_row("Circumcentre O = X(3)", str(bro.circumcenter))
table.add_row("Symmedian Point K = X(6)", str(rep.symmedian_point))
table.add_row("Brocard / First Lemoine Centre Ml = X(182)", str(rep.brocard_center))
table.add_row("Brocard Angle cot(ω) & sin²(ω)", f"cot(ω) = {rep.cot_omega}, sin²(ω) = {rep.sin_sq_omega}")
table.add_row("First Brocard Point Ω (c²a² : a²b² : b²c²)", str(rep.brocard_1))
table.add_row("Second Brocard Point Ω′ (a²b² : b²c² : c²a²)", str(rep.brocard_2))
table.add_row("Brocard's First Triangle (A1, B1, C1)", str(rep.brocard_first_triangle))
table.add_row("Lemoine Intercept Cube Ratios (a³/b³, a³/c³)", str(rep.lemoine_intercept_ratios))
table.add_row("Lagrange Minimum Σ dist² at K (Supp. I.7)", str(rep.min_perp_squares_sum))
table.add_row("Steiner Point X(99) on Circumcircle", str(rep.steiner_point))
table.add_row("Tarry Point X(98) (Antipode of X(99))", str(rep.tarry_point))
table.add_row("de Longchamps Point X(20) = 2O - H", str(rep.longchamps_point))
console.print(table)
if write_svgs:
for out_u5 in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-5" / "0205.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit5_symmedian_lemoine_circle.svg",
):
export_svg(
lem.model,
out_u5,
graphic_id="0205.g1",
title="Casey Supp. Ch. Secs. I & III — Symmedian Point K, First Lemoine Circle & Cosine Circle",
bbox=(-2.2, 16.2, -4.4, 13.2),
highlight_point_ids=("K", "O", "Ml"),
)
for out_u6 in (
_REPO_ROOT / "docsrc" / "sequel_to_euclid" / "unit-6" / "0220.g1.svg",
_REPO_ROOT / "docsrc" / "_static" / "figures" / "unit6_brocard_circle.svg",
):
export_svg(
bro.model,
out_u6,
graphic_id="0220.g1",
title="Casey Supp. Ch. Secs. II, V & VII — Brocard Points Ω, Ω′, Brocard Circle, Steiner X(99) & Tarry X(98)",
bbox=(-2.2, 16.2, -4.5, 13.2),
highlight_point_ids=("K", "Om1", "Om2", "St", "Tr"),
)
if __name__ == "__main__":
run_demo()