LEC point-site candidate completeness (NTS.Proofs 474)

[grootstebozewolf]

Implement the first honest slice of LEC candidate completeness for point sites off feature/sfa-curve-rgr (PR #7 @ 210f1b1). Inspect of merged grootstebozewolf/NetTopologySuite.Proofs#474 (main @ 69119abc) is in. Not stacked on OV-P2 drafts #16–#20. Does not merge to locationtech master.

Why

grootstebozewolf/NetTopologySuite.Proofs#474 (feat/lec-candidate-complete @ 3cfce602 / merge 69119abc) is the general candidate-completeness theorem for arbitrary finite point-site sets.

Headlines in theories/LECCandidateComplete.v (negation-form corollaries of improvement_kernel on dist²):

• lec_candidate_completeness_interior — an interior maximiser cannot have its nearest sites covered by two points. It is a Voronoi vertex with ≥ 3 nearest sites.
• lec_candidate_completeness_boundary_edge — a maximiser strictly inside a domain edge cannot have a unique nearest site. It is a bisector × boundary crossing.
• Domain vertices are the only boundary points left. The three classes are exhaustive.

Witness-scoped list in LECCandidateVertex.v (tri_candidates): vertex (2, 5/6), crossings (2,0), (1, 3/2), (3, 3/2), and the three sites. Ledger F2 / F3 / F8 in docs/lec-optimal-path.md.

What this PR does

Teaches existing LargestEmptyCircle.compute() only. After the certified-disc short-circuit, if every flattened obstacle is a point and the domain is a 2-D polygonal region, a private three-class walk runs and returns null to fall through to the current grid. No new public type. ObstacleDistance is unchanged; it is only used to score candidates.

The walk reuses VoronoiDiagramBuilder / QuadEdgeSubdivision:

1. Delaunay circumcentres (Voronoi vertices)
2. Neighbour-bisector × domain-edge crossings (and clipped Voronoi cell edges)
3. Domain-ring vertices

Public signatures (getCenter / getRadiusLine / hasCertifiedClosedForm) are unchanged. hasCertifiedClosedForm stays disc-only.

Non-point obstacles (lines, polygons, arcs, discs, mixed) keep the grid. Lipschitz slack is untouched (F2).

F8 (load-bearing)

Dropping the interiority premise is false (f8_interiority_load_bearing). Sites (0,0) and (2,0), domain = the connecting segment, midpoint (1,0) radius 1, exactly two nearest sites. Degenerate empty-interior domains use the edge theorem — this walk does not filter “not ≥ 3”. JTS boundary must be Polygonal; the two-point hull is a LineString and is not treated as a domain. F8 is pinned with an explicit thin rectangle containing the segment so the maximiser is forced onto the bisector × edge class.

Not this PR

• Weighted / Apollonius disc-site candidates. Later rung.
• Rocq oracle_bin / JNI in production LEC.
• Densify-as-laser. Laser = exact candidate (or the existing disc closed form). Else the grid.
• Loosening the 15% perf gate.

Tests

• Family I: sites (0,0),(4,0),(2,3) on the hull — unique maximiser (2, 5/6) radius 13/6; candidates include that vertex, (2,0), (1, 3/2), (3, 3/2), and the three sites. Exact vs the grid at a tight tolerance.
• Two sites in a rectangular domain: bisector × boundary crossing, not a Voronoi vertex.
• F8 thin polygonal domain containing the segment.
• Domain-vertex win; coincident sites keep the grid; collinear sites do not crash.
• Non-point stays on the grid; disc closed form still fires.
• Existing core / curve LEC tests and the 15% perf gate.

Verification

LargestEmptyCircleTest          30 run, 0 fail
LargestEmptyCircleCurveTest     12 run, 0 fail
LargestEmptyCirclePerfGateTest   8 run, 0 fail
bash dev/check-no-curved.sh     OK
checkstyle / pmd                BUILD SUCCESS