package rocq-robust-geometric-predicates

A small, self-contained Rocq library of formally verified robust geometric predicates for binary64 (IEEE-754 double) coordinates, extracted from the NetTopologySuite.Proofs corpus.

It provides, with Qed-closed soundness proofs against exact arithmetic:

• exact sign of the 2D orientation determinant (orient2d) via an error-free expansion (TwoSum / Dekker / fast-expansion-sum), proven to match the sign of the real determinant cross_R_BP;
• a Stage-D adaptive decoder (fast floating-point filter with an exact expansion fallback) and its soundness theorem;
• robust segment-intersection predicates;
• integer-coordinate determinant overflow bounds (0 axioms) for the int-safe regime.

The library sits on top of Flocq (the IEEE-754 substrate) and complements, rather than competes with, the geometry libraries in the ecosystem: GeoCoq is synthetic/axiomatic (no coordinates or floats), while this package is the analytic + floating-point-robustness layer. It also ships machine-checked counterexamples showing where the textbook strong-nonoverlap postcondition of Shewchuk's Theorem 13 is FALSE as stated under a half-ulp predicate, so the top-level orientation soundness is stated honestly (the strong-nonoverlap headline appears as an explicit, type-visible hypothesis where it is needed).

Provenance: github.com/grootstebozewolf/NetTopologySuite.Proofs (assembled via the package MANIFEST). Every theorem ends in Qed; the only axioms are the standard classical-reals + functional-extensionality used throughout the corpus (see make's Print Assumptions output).