Java Geometry Expert (JGEX) & Chou–Gao–Zhang’s Area Method

  • Repository: _refs/Java-Geometry-Expert (https://github.com/yezheng1981/Java-Geometry-Expert, GPL-3.0-only, ChouGaoZhang1994, YeChouGao2011)

  • Scale Audited: src/main/java/gprover/ (GDD, Full, Area, Elim, CharSet Wu, PanelGB Gröbner) + hundreds of .gex theorems (exs-book/, 3_JAR/, 4_PYTH/)

  • Mathematical Foundation: Multi-engine synthesis uniting Deductive Databases, Full-Angles, Coordinate-Free Area/Pythagoras Elimination, Ritt–Wu Characteristic Sets, and Gröbner Bases

1. Historical Mother-Ship of Automated Geometry

Java-Geometry-Expert (JGEX), created by Zheng Ye, Shang-Ching Chou, and Xiao-Shan Gao, is the direct ancestor from which AlphaGeometry and Newclid inherited both their clause DSL and their 43 GDD Horn rules. Crucially, however, JGEX was designed around five complementary reasoning engines so that when forward Horn saturation (GDD) stalls, coordinate-free invariant elimination (Area / Full-Angle) or algebraic triangulation (Wu / Gröbner) takes over.

2. Mathematical Jewel: The Coordinate-Free Area Method

Formulated by Chou, Gao, and Jing-Zhong Zhang (ChouGaoZhang1994), the Area Method proves theorems without introducing Cartesian coordinates and without guessing auxiliary points, using three coordinate-free geometric quantities:

  1. Signed Parallel Ratio \(r = \overline{AB} / \overline{CD}\) for parallel directed segments \(AB \parallel CD\).

  2. Signed Polygon Area \(S_{ABC}\) (and quadrilateral \(S_{ABCD} = S_{ABC} + S_{ACD}\)), vanishing iff \(A, B, C\) are collinear and satisfying the Co-Side Theorem: if \(M = AB \cap PQ\), then \(\overline{PM}/\overline{QM} = S_{PAB}/S_{QAB}\).

  3. Pythagoras Difference (Pythagoras difference):

    \[P_{ABC} = |AB|^2 + |BC|^2 - |AC|^2, \qquad P_{ABCD} = |AB|^2 + |CD|^2 - |BC|^2 - |DA|^2 = 2\,\overrightarrow{AC}\cdot\overrightarrow{BD}\]

Look at what happens immediately in this basis:

  • Pythagoras (`Euclid I.47`) is 0 steps: \(AB \perp BC \iff P_{ABC} = 0\) by definition!

  • Orthocenter Concurrency is 0 steps: For any four points \(A, B, C, H\), expanding squares gives the Jacobi-like identity \(P_{ACHB} + P_{BAHC} + P_{CBAH} \equiv 0\). If \(AH \perp BC\) (\(P_{BAHC} = 0\)) and \(BH \perp AC\) (\(P_{CBAH} = 0\)), then \(P_{ACHB} = 0\) (\(CH \perp AB\)) instantaneously!

  • Pappus, Ceva, Menelaus, Cross-Ratio & La Hire Inversion: Given a constructive sequence of points (INTERSECTION_LL, FOOT, PRATIO, TRATIO, INVERSION), each constructed point \(Y\) appears linearly in \(S\) and \(P\) (Elim.java) and is eliminated backward in one rational substitution step—proving Pappus (exs-book/ch2:40) and La Hire pole–polar (exs-book/ch3:49) with zero auxiliary points while automatically extracting exact Non-Degeneracy Conditions (`NDGs`)!

3. Forensic Surprise: Area.java Left Unfinished in JGEX!

Inspecting the actual Java source tree in _refs/Java-Geometry-Expert/src/main/java/ revealed a major surprise: while the elimination kernel helpers live in gprover/Elim.java, gprover/Area.java (213 lines) is an incomplete port from C, and in wprover/PanelProve.java:112-116 the GUI Area-Method tab is literally commented out:

// wprover/PanelProve.java:112-116
        // TODO: Implement the area method
        // panelMethod.addTab("A", ...);

In the shipping Java GUI, users only have interactive access to GDD, Full-Angle, Wu (CharSet.java), and Gröbner (PanelGB.java using Rabinowitsch saturation \(1 - u_k g_k = 0\)).

4. Takeaway for GEOMETOR

geometor.model already has exact signed_area2 and quadrance! Adding pythagoras_diff and completing Chou–Gao–Zhang’s backward point eliminator in clean Python 3.13 / SymPy (Blueprint 6) finishes the exact readable-proof engine that JGEX left unfinished in Java.