A Rocq-Based Formalization of Hilbert’s Geometry: Building a Reusable Foundation for 3D Perpendicularity Theory and Verification

Hilbert’s axiom system for geometry is a landmark in formal methods. This paper presents a complete formalization of spatial perpendicularity—a theory not fully developed in Hilbert’s original work—using the Rocq proof assistant. We systematically defined the relations of perpendicularity between lines and planes based solely on Hilbert’s primitive notions and axioms. Within this framework, we mechanized the proof of a significant spatial congruence theorem that Hilbert stated without proof—a theorem that fundamentally reveals the relationship between congruence and motion. The formal proof of this theorem demonstrates the intrinsic completeness of Hilbert’s system for three-dimensional (3D) space. Crucially, no additional spatial congruence axioms are needed, as all properties are derived rigorously from the original planar axioms. All proofs are mechanically verified by Rocq, ensuring logical correctness. This work completes Hilbert’s geometry system. It also delivers a reusable Rocq library that offers a rigorous foundation for verifying geometric reasoning in safety-critical software systems.