package rocq-spatial-algebra

A tiny, dependency-free Rocq library of spatial-relation algebra, extracted from the NetTopologySuite.Proofs corpus.

Two independent modules, both Qed-closed with NO axioms ("Closed under the global context") and depending only on Rocq's Stdlib:

• DE9IM: the DE-9IM (Dimensionally Extended 9-Intersection Model) algebra used by OGC/SQL-MM spatial predicates -- dimension values, intersection matrices, named relation patterns (disjoint, intersects, contains, within, covers, ...), pattern matching, and the transpose laws relating a relation to its converse.

• RelateIntDetBound: the 2D orientation determinant over integer coordinates together with proven magnitude/overflow bounds, used to certify the safe-coordinate regime for robust orientation predicates.

Both modules are foundational and self-contained: zero intra-corpus dependencies, no Flocq, no classical reals. Useful to any project doing formal GIS / spatial-relation reasoning or robust-predicate overflow analysis.

Provenance: github.com/grootstebozewolf/NetTopologySuite.Proofs (assembled via the package MANIFEST).