GEOMETOR Codes

A Comparative Study of Formal Languages, Visual Pseudocodes, Symbolic Architectures, Syntax, and Canon (“Opus”) Across Geometric Logic — and How They Inform GEOMETOR.

Every formalization of geometry makes a foundational wager about what a geometric entity is, how existence and degeneracy are certified, and how human intuition meets symbolic proof. Across two millennia—from Euclid of Alexandria’s lettered diagrams and Oliver Byrne’s 1847 four-color visual pseudocode to modern interactive theorem provers, neuro-symbolic Olympiad engines, Clifford multivector calculi, and complex projective Riemann-surface tracers—each language illuminates certain truths effortlessly while rendering other truths verbose, unexpressible, or silently broken.

geometor-codes sits at Layer 2 of the 33-repository GEOMETOR ecosystem. It conducts a source-level forensic audit of 11 formal, visual, and symbolic geometric architectures, decodes 60 unfamiliar syntactic symbols and combinators, compares 7 canonical Rosetta Stone constructions side-by-side, maps 69 canonical topics across 8 domains (759 audited coverage cells), and distills 11 concrete engineering blueprints for geometor.model, geometor.elements 2.0 (Principles of Geometry), geometor.wildberger, geometor.pappus, geometor.etc, geometor.divine, and geometor.seer.

< A B F > ( A B ) (Q = 4) ( B A ) (Q = 4) [ A B ] / A F / (Q = 4) / B F / (Q = 4) A = [0, 0] B = [2, 0] F = [1, sqrt(3)] System E: F = intersect_same_side Tarski: Cong A B A F /\ Cong B A B F Mathlib4: dist F A = dist A B 2DCGA: C = P1 ^ P2 ^ P3 CP^2: conic through I, J GEOMETOR: Q(A,F)=Q(B,F)=4, s=3/4 AA BB FF + − ⟲ Lbl Gde

One Figure, Eleven Languages — Euclid’s opening vesica piscis (A, B, circles AB and BA, equidistant poles F and E on line AB) viewed simultaneously through diagrammatic Formal System E, Tarski’s point-only ontology, mathlib4 affine torsor spaces, DD+AR clauses, 2D Conformal Geometric Algebra null-cone blades, \(\mathbb{CP}^2\) homogeneous matrices, Oliver Byrne’s chromatic value-token glyphs, and geometor.model’s exact \(\mathbb{Q}(\sqrt{3})\) DAG. Hover any :g: badge or diagram locus to illuminate its corresponding element.

Headline Forensic Discoveries

  1. Unverified Trust Oracle & Six Missing Lemmas in LeanEuclid: LeanEuclid (Murphy2024) faithfully separates constructive steps (euclid_apply) from diagrammatic topology, and its 7 rules in Intersections.lean correspond 1-to-1 with geometor.model.intersect’s selectors (side_of, between, beyond). Yet source inspection of SystemE/Meta/Smt/Solver.lean:44-55 reveals that euclid_finish closes goals via private axiom SMT_VERIF (P : Prop) : P without reconstructing proof terms in the Lean 4 kernel, while Book/Prop47.lean:25-60 isolates six topological square-orientation lemmas missed by Euclid in the Bride’s Chair proof.

  2. Metatheoretic Gold & Classical Gaps in GeoCoq: Across 481 Coq files and 4,671 kernel-checked lemmas (Boutry2019), GeoCoq proves bidirectional equivalences between Tarski, Hilbert, and Euclid, 34 equivalent parallel postulates, neutral-geometry midpoint existence without circles, and an explicit proof of False when non-collinearity is omitted from cut-and-paste area axioms—yet omits the Nine-Point Circle X(5), Steiner circle power, radical axes, circle inversion, pole–polar reciprocity, conics, and the golden ratio.

  3. Dimension-Polymorphic Elegance vs. Noncomputable Projective Gaps in Mathlib4: Mathlib/Geometry/Euclidean/ (Mathlib2020) generalizes the orthocenter (mongePoint), the \(3(n+1)\)-point Feuerbach sphere, Sphere.power, inversion, and 1-line La Hire pole–polar reciprocity to arbitrary dimension \(n\)—yet is pervasively noncomputable, lacks a constructive Euclid I.1 theorem, documents a 20-line cyclic-order TODO in Sphere/Ptolemy.lean:22-41, and contains zero radicalAxis, crossRatio, Menelaus, Pappus, or Desargues.

  4. Log-Ratio Bug & Expressiveness Walls in AlphaGeometry / Newclid: Source audit of alphageometry/ar.py:425-431, 570-574 (Trinh2024) uncovers a live bug where RatioTable.add_const_ratio encodes \(m \log|s_1| - n \log|s_2| = 0\) (\(|s_1|^m = |s_2|^n\) instead of \(|s_1|/|s_2| = m/n\)), alongside silent drops of unprefixed post-; clauses in 12 defs.txt stanzas. Architecturally, pure DD+AR cannot state \(a^2 + b^2 = c^2\) or disjoint radical axes (fixed in C++ Yuclid’s squared-length AR) and cannot prove Pappus or Desargues without auxiliary parallel lines (forcing Newclid to hardcode R44_PAPPUS_THEOREM and R70_PROJECTIVE_HARMONIC_CONJUGATE as axioms).

  5. The Unfinished Area Method in JGEX: Shang-Ching Chou, Xiao-Shan Gao, and Jing-Zhong Zhang’s coordinate-free Area Method (ChouGaoZhang1994) proves Pythagoras in 0 steps (P_BAC = 0 by definition), Orthocenter in 0 steps (Jacobi identity), and Pappus/La Hire/Cross-Ratio with zero auxiliary points—yet in Java-Geometry-Expert’s Java codebase, Area.java (213 lines) is an unfinished port whose GUI tab is commented out in PanelProve.java:112-116 (TODO: Implement the area method).

  6. Clifford Dual Traps in GAlgebra vs. Conformal Triumphs in Kingdon: galgebra crashes with AttributeError on .dual() for every degenerate Projective Geometric Algebra (\(I^2 = 0\)), omits the regressive join &, and overloads >> as a commutator rather than a sandwich product. By contrast, kingdon compiles exact SymPy polynomial blades where 2D CGA circle power is -2*(kappa | P), radical axis is kappa1 - kappa2, circumcenter is C * ni * ~C, and circle inversion is C >> P.

  7. Live Symbolic Bugs in SymPy Geometry (`1.14.0`): Source inspection of sympy/geometry/ reveals (a) a double live bug in ``Triangle.excenters`` (polygon.py:2714-2726: missing numerator parentheses -a*x[0] + b*x[1] + c*x[2]/(-a+b+c) plus wrong side-vertex pairing) and (b) a 2-digit float zero-test bug in ``Point.affine_rank`` (point.py:331-335: abs(x.n(2)) < 1e-12) causing exact rational non-collinear points to falsely test collinear, alongside solve() bottlenecks and missing Hyperbola, inversion, radical_axis, polar, and cross_ratio.

  8. Byrne’s Pointer-Free Visual Pseudocode & The Universal Golden Blind Spot: Across LeanEuclid, GeoCoq, mathlib4 Geometry, AlphaGeometry, and Newclid, the Golden Ratio (:math:`phi`) and Book XIII Platonic Solids have zero geometric coverage. Remarkably, Oliver Byrne’s 1847 Coloured Euclid (Byrne1847; revived interactively by Nicholas Rougeux, Rougeux2018) not only pioneered pointer-free visual pseudocode (Given / To Prove / Construction / Proof with inline chromatic value-tokens), it also formalized Book II gnomons, Book III circle power, Book IV pentagons, and Book VI golden-ratio cuts—directly inspiring GEOMETOR’s synthesis of exact symbolic identifiers with interactive visual tokens.

Guided Navigation

  • Hierarchy — The 8 mathematical paradigms of geometric formalization and the 7-layer, 33-repository GEOMETOR architecture with 11 prioritized upgrades.

  • Syntax Field Guide & Symbol Decoder — Beginner-to-expert decoder for 60 formal symbols, dependent binders, Tarski predicates, Clifford blades, clause stanzas, and Byrne chromatic value-tokens.

  • Systems — Ten deep architectural and forensic dossiers covering all 11 surveyed systems.

  • Rosetta Stone Benchmarks — Seven canonical constructions and theorems implemented side-by-side across all 11 systems with interactive .euclid-graphic SVGs.

  • Opus Coverage Matrix (69 Topics x 11 Systems) — The complete 69-topic \(\times\) 11-system Opus Coverage Matrix across 8 geometric domains.