Initial Comparative Study Across 11 Formal, Visual & Symbolic Geometry Systems

Launched geometor.codes v0.1.0 at Layer 2 of the GEOMETOR ecosystem, conducting a forensic source-level comparison across 11 formal, visual, and symbolic geometry architectures: LeanEuclid (Murphy2024), GeoCoq (Boutry2019), mathlib4 (Mathlib2020), AlphaGeometry (Trinh2024), Newclid/Yuclid (Sicca2024), Java-Geometry-Expert (YeChouGao2011), kingdon/galgebra PGA & CGA (Gunn2020), CindyJS (RichterGebert2011), sympy.geometry (1.14.0), Oliver Byrne’s 1847 Coloured Euclid / Nicholas Rougeux (Byrne1847, Rougeux2018), and geometor.model.

Highlights

• Canonical Datasets & Typed Query Engine (geometor.codes.registry): Authored systems.json (11 profiles), syntax_lexicon.json (60 symbol decoders), opus_matrix.json (69 topics across 8 domains \(= 759\) cells), rosetta_benchmarks.json (7 benchmarks \(\times 11\) systems \(= 77\) encodings), and geometor_hierarchy.json (7 layers, 33 repositories, 11 prioritized engineering recommendations).

• Exact Float-Free Demonstrations (geometor.codes.figures): Built 9 exact Model(..., auto_intersect=False) interactive .euclid-graphic SVG figures verified symbolically via Rational Trigonometry (quadrance, spread, cross_ratio) with zero sp.Float atoms.

• Forensic Audit Catch: Documented SMT_VERIF and 6 missed Euclid lemmas in LeanEuclid, rconst log-ratio hallucination and ; clause drops in AlphaGeometry, disabled Area.java in JGEX, .dual() / >> traps in galgebra, live double bugs in sympy.geometry’s Triangle.excenters and Point.affine_rank, Byrne’s pointer-free visual pseudocode architecture, and the universal omission of the Golden Ratio (\(\phi\)) and Platonic solids across modern ITPs/ATPs.