INCIRCLE_SIGN: stale deferral note, wrong bound, and an unproven window above 2^11

[grootstebozewolf]

Found verifying #68 (wayfinder map docs/scout/map-epic-block-64-69.md). Three small things that compound into one real exposure.

1. The in-file note is stale

oracle/driver.ml:964-966 says the soundness of the b64_inCircle sign against inCircle_R''s sign is "deferred — docs/oracle-handroll-migration.md item 2".

docs/oracle-handroll-migration.md:95-109 marks item 2 ✅ DONE, discharged by theories-flocq/InCircle_b64_exact.v:264 b64_inCircle_exact_sound (Qed, full plane, all_finite8 only) plus the integer-regime sibling b64_inCircle_exact_for_small_int:592.

2. The bound in that note is wrong, in the optimistic direction

The driver comment quotes |coord| <= 2^12. The proven integer regime is 2^11 (InCircle_b64_exact.v:592, and the migration doc agrees). So the comment overstates the certified window by a factor of two — the same defect shape as verified-claims.md''s 2²³-for-2²² in #503.

3. The exposure

INCIRCLE_SIGN (driver.ml:974, dispatch :4432) prints a confident POS / NEG / ZERO from the naive float determinant. Inside 2^11 that is Qed-backed. Outside it, the label is confident and the sign is unproven — an integer determinant at larger magnitudes can exceed the exactly-representable range and the float sign can flip.

INCIRCLE_EXACT (:435-456, dispatch :4433) computes the same determinant in bignum dyadic arithmetic and is Qed-backed for all finite binary64. So the fix is availability, not mathematics: a consumer that picks the cheap mode for large coordinates gets an unproven answer with no signal.

Note this is not the empty-branch fabrication seen in #511 / #513 — degeneracy is handled loudly here. incircle_sign_string:968 tests v <> v first and emits NAN; exact zero emits ZERO rather than guessing a side, which is why the JTS#1039 cocircular knife-edge is reported honestly and matches cocircular_tie_no_flip_witness.

Ask

1. Correct the driver comment: item 2 is done, and the integer regime is 2^11, not 2^12.
2. Guard or route. Either have INCIRCLE_SIGN decline (or flag) above the proven window, or document that Delaunay consumers must use INCIRCLE_EXACT — and say which in the mode header, since the pins in DelaunayDegeneratePins.v:32-34 are aimed at these modes.
3. While in there: DELAUNAY_WITNESS, named in that same source comment as the mode the degeneracy pins should feed, does not exist — the string appears nowhere else in the repo. Tracked in Global Delaunay: real triangulation predicate, DT existence, insert correctness, then the Voronoi dual #525.

topics: mesh, precision
claimId: none