grootstebozewolf · grootstebozewolf · Aug 5, 2026 · Aug 5, 2026
diff --git a/docs/ffi-rungs-2026-08.md b/docs/ffi-rungs-2026-08.md
@@ -20,9 +20,9 @@ process — not new ABI symbols.
 | **1** | Re-extract `Validate_binary64_extract.v` → freshen `oracle/extracted.ml` | **GREEN** (local WSL; extract is gitignored) |
 | **2** | `make -C oracle ffi` → full `libntsrocq.so` + `ffi_probe` | **GREEN** after rung 1 |
 | **3** | `make -C oracle ffi-parity` | **YELLOW** — 3 ORIENT_EXACT* cases segfault on extreme coords (see §3) |
-| **4** | Orientation differential scout for [jts#1093](https://github.com/locationtech/jts/pull/1093) | **Harness landed** (`oracle/gen_jts1093_orient_scout.py`) |
+| **4** | Orientation differential scout for [jts#1093](https://github.com/locationtech/jts/pull/1093) | **GREEN** — 45 vectors; see [`jts-1093-orient-lane-2026-08.md`](jts-1093-orient-lane-2026-08.md) |
 | **5** | Retire / demote `scout_incircle_*` once full FFI is the default path | Pending CI green on parity |
-| **6** | Optional: post numbers on jts#1093 / keep #1197 green | Later |
+| **6** | Optional: post numbers on jts#1093 / keep #1197 green | Draft: `tests/Discussion839Mre/jts-1093-comment.md` |
 
 ---
 
@@ -102,7 +102,7 @@ allocation under the shared-lib runtime), not the abstract algorithm.
 
 ---
 
-## §4 — Orientation lane (rung 4)
+## §4 — Orientation lane (rung 4) — GREEN
 
 Upstream: [jts#1093](https://github.com/locationtech/jts/pull/1093) replaces
 JTS `orientationIndexFilter` Shewchuk-ish / `DP_SAFE_EPSILON=1e-15` path with
@@ -122,10 +122,13 @@ Corpus counterpart:
 |---|---|
 | `b64_orient_sign_filtered` | Shewchuk Stage A (corpus / FFI) |
 | `b64_orient2d_exact` / `ORIENT_EXACT` | Full-plane sign GT |
-| `oracle/gen_jts1093_orient_scout.py` | Ozaki mirror vs Shewchuk filter vs exact |
+| `oracle/gen_jts1093_orient_scout.py` | Three-way: master / Ozaki / Shewchuk vs exact |
+| [`jts-1093-orient-lane-2026-08.md`](jts-1093-orient-lane-2026-08.md) | Session write-up |
 
-Gate intent: **Ozaki CERTAIN never disagrees with exact**; report how often
-Ozaki is CERTAIN when Shewchuk is UNCERTAIN (tighter filter claim).
+**Gate (2026-08-05, 45 vectors):** Ozaki / Shewchuk / master CERTAIN vs exact
+conflicts all **0**. Ozaki CERTAIN while master UNCERTAIN: **4** (same-sign
+\(h \in \{10^{-15}, 2\cdot10^{-15}\}\) band). Ozaki ↔ corpus Shewchuk certainty
+splits: **0**. Details and PR comment draft in the lane doc.
 
 ---
 
@@ -142,8 +145,8 @@ Ozaki is CERTAIN when Shewchuk is UNCERTAIN (tighter filter claim).
 ## §6 — Next actions
 
 1. Track ORIENT_EXACT FFI segfault (rung 3 close-out) — isolated repro above.
-2. Run `python3 oracle/gen_jts1093_orient_scout.py` in CI-ish local loop; comment
-   on jts#1093 only with numbers.
+2. ~~Run `python3 oracle/gen_jts1093_orient_scout.py`~~ **done** (rung 4 GREEN);
+   optional: post `tests/Discussion839Mre/jts-1093-comment.md` on jts#1093.
 3. Wire `make -C oracle ffi` into developer docs / optional CI once parity is
    green or exact is skipped under a named env flag.
 

diff --git a/docs/jts-1093-orient-lane-2026-08.md b/docs/jts-1093-orient-lane-2026-08.md
@@ -0,0 +1,206 @@
+# Orientation lane — JTS #1093 Ozaki filter differential (session)
+
+**Date**: 2026-08-05.  
+**topic:** `precision` · epic **#66** (orient substrate; also #64 consumers)  
+**Upstream**: [locationtech/jts#1093](https://github.com/locationtech/jts/pull/1093)
+  *Change Shewchuk Orientation filter to Ozaki et al.* (tinko92) — single-file
+  change to `CGAlgorithmsDD.orientationIndexFilter`.  
+**Sibling**: [jts#1197](https://github.com/locationtech/jts/pull/1197) (ours —
+  DD orientation characterization / `RocqRefRunner`); keep green in parallel.  
+**Scope**: Pure-double mirrors of **three** Stage A shapes vs corpus
+  `ORIENT_EXACT`; optional FFI `ORIENT_FILTERED` for corpus Stage A. No new
+  Rocq theorems; no Ozaki entry in `libntsrocq` (ADR-0004 cold).
+
+**Verdict**: **GREEN** — on a 45-vector table, **no CERTAIN wrong signs** for
+Ozaki, corpus Shewchuk Stage A, or JTS-master (`DP_SAFE_EPSILON = 1e-15`).
+Ozaki is **strictly tighter than master** on this table (4 CERTAIN where master
+UNCERTAIN; 0 reverse). Ozaki certainty matches the corpus Shewchuk constant
+shape (0/0 tightness divergences). Product call: **safe to merge from a
+soundness-filter perspective**, with the usual DD/exact fallback remaining
+mandatory near collinearity.
+
+---
+
+## §1 — What #1093 changes
+
+`CGAlgorithmsDD.orientationIndexFilter` only (production orientation fast path
+before DD escalation):
+
+### Before (master)
+
+Shewchuk-**style** detsum construction + opposite-sign early return, but with
+a **loose** relative constant:
+
+```text
+DP_SAFE_EPSILON = 1e-15
+errbound = DP_SAFE_EPSILON * detsum
+certain  iff |det| >= errbound   (or early CERTAIN on opposite-sign products)
+```
+
+PR author note: this is *not* Shewchuk’s published constant (which is
+≈ \(3.33 \times 10^{-16}\)).
+
+### After (#1093 / Ozaki et al.)
+
+```text
+detleft  = (pax - pcx) * (pby - pcy)
+detright = (pay - pcy) * (pbx - pcx)
+det      = detleft - detright
+errbound = |detleft + detright| * 3.3306690621773724e-16
+certain  iff |det| >= errbound
+```
+
+Claims (PR body): tighter ⇒ fewer DD misses; fewer/more predictable branches;
+theoretically and practically faster. **No new tests** — behaviour should match
+existing predicate tests except speed.
+
+Reference: Ozaki, Ogita, Rump, Oishi (2011/2016),
+[doi:10.1007/s10543-015-0574-9](https://doi.org/10.1007/s10543-015-0574-9).
+
+---
+
+## §2 — Corpus ground truth
+
+| Asset | Role |
+|---|---|
+| `b64_orient2d_exact` / `ORIENT_EXACT` | Full-plane exact sign (`oracle_bin`) |
+| `b64_orient_sign_filtered` / `ORIENT_FILTERED` | Corpus Shewchuk Stage A (FFI optional) |
+| `Orient_b64_exact*` / `Orient_b64_exact_full.v` | Qed soundness of exact orient |
+| `Orientation_b64.v` Stage A | Qed filter discipline (commit only when bound clears) |
+| `docs/orient-stratified-apf.md` | Stratified APF narrative |
+
+Sign convention (JTS `orientationIndex` / corpus):
+
+> `POS` ⇔ left of directed line \(a \to b\) when standing at \(a\) looking toward \(b\)  
+> (equivalently CCW triangle \((a,b,q)\)).
+
+**Policy (FFI rungs):** use **`oracle_bin` ORIENT_EXACT** as GT; in-process
+exact FFI still has a rare segfault class on extreme coords
+([ffi-rungs-2026-08.md](ffi-rungs-2026-08.md)). Filtered FFI is fine for
+corroboration.
+
+---
+
+## §3 — Three filters under test
+
+| Filter | Constant | Structure | Source |
+|---|---|---|---|
+| **JTS-master** | \(1 \times 10^{-15}\) | detsum + opposite-sign early CERTAIN | `CGAlgorithmsDD` master |
+| **Ozaki (#1093)** | \(3.3306690621773724 \times 10^{-16}\) | \(\lvert\mathrm{detleft}+\mathrm{detright}\rvert \cdot K\) | PR tip |
+| **Corpus Shewchuk** | \(\mathrm{ccwerrboundA}=(3+16\varepsilon)\varepsilon \approx 3.3306690738754716 \times 10^{-16}\) | detsum + early CERTAIN | `Orientation_b64` / `predicates.c` |
+
+Ozaki’s published double is **slightly smaller** than \(\mathrm{ccwerrboundA}\)
+(tighter by ~\(1.17 \times 10^{-26}\)); on this table they never split certainty.
+
+---
+
+## §4 — Deliverables
+
+| Path | Purpose |
+|---|---|
+| `oracle/gen_jts1093_orient_scout.py` | Three-way Stage A mirror + oracle gate |
+| `oracle/jts1093_orient_vectors.txt` | 45-vector table (regenerated by the script) |
+| `oracle/Makefile` target `jts1093-orient-scout` | Convenience wrapper |
+| `docs/ffi-rungs-2026-08.md` | Rungs 0–3 (extract / full FFI / parity) |
+
+```text
+python oracle/gen_jts1093_orient_scout.py \
+  --wsl-oracle /home/user/nettopologysuite.proofs/oracle/oracle_bin \
+  --wsl-ffi-probe /home/user/nettopologysuite.proofs/oracle/ffi_probe
+# or on Linux:  --oracle oracle/oracle_bin --ffi-probe oracle/ffi_probe
+```
+
+---
+
+## §5 — Gate results (2026-08-05)
+
+| Metric | Value |
+|---|---|
+| Vectors | **45** |
+| Oracle pin (unit CCW) | **POS** ✓ |
+| EXPECTED pin failures | **0** |
+| Ozaki CERTAIN vs exact conflicts | **0** |
+| Corpus Shewchuk CERTAIN vs exact conflicts | **0** |
+| JTS-master CERTAIN vs exact conflicts | **0** |
+| Ozaki UNCERTAIN | **10** |
+| Corpus Shewchuk UNCERTAIN | **10** |
+| JTS-master UNCERTAIN | **14** |
+| Ozaki CERTAIN while JTS-master UNCERTAIN | **4** |
+| JTS-master CERTAIN while Ozaki UNCERTAIN | **0** |
+| Ozaki ↔ corpus Shewchuk certainty splits | **0** |
+
+### Load-bearing band (same-sign products)
+
+Construction (forces detsum path; det ≈ \(h\)):
+
+```text
+a = (0, 0),  b = (1, 0.5),  q = (2, 1 + h)
+```
+
+| \(h\) | Exact | JTS-master | Ozaki | Shewchuk |
+|---|---|---|---|---|
+| \(10^{-12}\), \(10^{-14}\) | ± | CERTAIN | CERTAIN | CERTAIN |
+| **\(10^{-15}\), \(2\cdot10^{-15}\)** | ± | **UNCERTAIN** | **CERTAIN** | **CERTAIN** |
+| \(5\cdot10^{-16}\), \(3.3\cdot10^{-16}\) | ± | UNCERTAIN | UNCERTAIN | UNCERTAIN |
+| \(10^{-16}\) | ZERO / NEG | UNCERTAIN | UNCERTAIN | UNCERTAIN |
+
+This is the PR’s **“fewer misses”** claim in miniature: master escalates at
+relative \(10^{-15}\) while Ozaki (and true Shewchuk) still commit correctly.
+
+### Pins that correctly force escalation
+
+Diagonal collinear, decimal `.1` almost-collinear, zero-length edge, and the
+deep same-sign band (\(|h| \lesssim 5\cdot10^{-16}\)): filters return **UNCERTAIN**
+(or CERTAIN ZERO only when the double det is exactly 0 and the filter allows
+it). DD / exact path must remain.
+
+### FFI note
+
+Optional `ORIENT_FILTERED` agreed with pure-Python Shewchuk on clear pins.
+Near the \(10^{-15}\) same-sign band, FFI sometimes reports **UNCERTAIN** while
+the pure-Python \(\mathrm{ccwerrboundA}\) mirror with non-strict `>=` reports
+CERTAIN — consistent with a **stricter “strictly clears bound”** discipline in
+the extracted filter (`docs/orient-stratified-apf.md`). Not a #1093 product
+issue; Ozaki/JTS use non-strict `>=` as in the Java sources.
+
+---
+
+## §6 — Implications for JTS / NTS
+
+1. **#1093 filter is sound on this table** relative to independent exact orient:
+   CERTAIN commits never disagreed with `ORIENT_EXACT`.
+2. **Master’s `1e-15` is the loose outlier**, not Ozaki. Moving to Ozaki moves
+   JTS closer to the corpus / Shewchuk Stage A constant class.
+3. **Do not** treat double Stage A alone as ground truth near collinearity —
+   keep DD (current JTS) or exact / Rocq `ORIENT_EXACT` for the uncertain band.
+4. **Do not** add Ozaki as a Rocq FFI symbol unless/until the corpus proves an
+   Ozaki filter under a named claimId (product decision). Differential scouts
+   stay in Python.
+5. **NTS port:** when NTS copies `CGAlgorithmsDD`, re-run this script against
+   the same table; expect the 4-vector tightness win vs pre-port `1e-15`.
+6. **#1197** remains the characterization / RocqRefRunner track — complementary,
+   not competing.
+
+---
+
+## §7 — What this session does *not* claim
+
+- Bit-identity of JTS DD fallback with `ORIENT_EXACT`.
+- A full formal proof of the Ozaki error bound (paper is the reference).
+- Exhaustive adversarial search over all binary64 triples.
+- Merge politics / review of Java style beyond the filter math.
+
+---
+
+## §8 — Next
+
+| Item | Status |
+|---|---|
+| Expand vector bank + three-way gate | **This session GREEN** |
+| Draft PR comment with numbers | `tests/Discussion839Mre/jts-1093-comment.md` |
+| Post comment on jts#1093 | Human / optional |
+| Keep #1197 green | Ongoing |
+| ORIENT_EXACT FFI segfault class | Separate (ffi rungs §3) |
+
+**AI assistance**: Grok (grok-4.5), human-directed.  
+**License**: project documentation (BSD-3-Clause).
diff --git a/docs/jts-1212-incircle-lane-2026-08.md b/docs/jts-1212-incircle-lane-2026-08.md
@@ -127,7 +127,7 @@ exactly the fix shape.
 | 1b | Add `jts1212_incircle_vectors.txt` to CI smoke (`make -C oracle` optional target) | small |
 | 1c | Comment on jts#1212 with GEOS955 StageA=0 / oracle=POS table (numbers only) | 15 min |
 | 1d | Extract more quads from full circle expected MULTILINESTRING if needed | medium |
-| 2 | Orientation lane (#1093 Ozaki) — separate session | — |
+| 2 | Orientation lane (#1093 Ozaki) — separate session | **GREEN** ([jts-1093-orient-lane-2026-08.md](jts-1093-orient-lane-2026-08.md)) |
 
 ---
 

diff --git a/docs/jts-open-prs-scout-2026-08.md b/docs/jts-open-prs-scout-2026-08.md
@@ -37,7 +37,7 @@ Ordered by **risk÷cost** for the proofs corpus (not JTS merge politics).
 | **1** | [#1212](https://github.com/locationtech/jts/pull/1212) | Improve triangulation robustness | **#68** `mesh` | H | L–M | H | `TrianglePredicate.isInCircleRobust` Shewchuk-style filter + `Vertex.isCCW` → `Orientation.index`. Corpus has `b64_inCircle` / `DelaunayLocallyDelaunay` / empty-circle pins — can **diff-test** the new filter against `INCIRCLE_SIGN` / `nts_rocq_in_circle`. Direct NTS port path. |
 | **2** | [#1094](https://github.com/locationtech/jts/pull/1094) | Make isInCircleRobust robust | **#68** `mesh` | H | L | H | Older sibling of #1212 on the same class. Same gate; prefer whichever is current tip — treat as **one lane**. |
 | **3** | [#311](https://github.com/locationtech/jts/pull/311) | isInCircleAdapt sketch Java port | **#68** `mesh` | H | L | H | Shewchuk adaptive sketch; updated 2026-05. Superseded in spirit by #1094/#1212 but useful as **design history**. Corpus Stage D expansion work is the formal counterpart. |
-| **4** | [#1093](https://github.com/locationtech/jts/pull/1093) | Change Shewchuk Orientation filter to Ozaki et al. | **#66/#64** `precision`/`core` | H | M | H | Changes production `CGAlgorithmsDD` orientation filter. Corpus ground truth: `Orient_b64_exact*` / `nts_rocq_orient_sign_exact`. **Must** differential-test before blessing; Ozaki vs Shewchuk Stage A is a real soundness product decision. |
+| **4** | [#1093](https://github.com/locationtech/jts/pull/1093) | Change Shewchuk Orientation filter to Ozaki et al. | **#66/#64** `precision`/`core` | H | M | H | Production `CGAlgorithmsDD` filter. **Lane GREEN 2026-08-05:** 45-vector three-way gate (master `1e-15` / Ozaki / corpus Shewchuk) vs `ORIENT_EXACT` — 0 CERTAIN conflicts; Ozaki tighter than master on 4 same-sign band cases. See [`jts-1093-orient-lane-2026-08.md`](jts-1093-orient-lane-2026-08.md). |
 | **5** | [#1197](https://github.com/locationtech/jts/pull/1197) | Characterize DD orientation soundness (#1106) | **#66** `precision` | H | L | M | **Ours.** Test-only characterization + `RocqRefRunner`. Aligns with `docs/verified-claims.md` orient rows and oracle vectors. **Push merge / keep green** — low cost, high signalling. |
 | **6** | [#90](https://github.com/locationtech/jts/pull/90) | Fix ScaledNoder behaviour (draft) | **#66** `precision` | H | M | H | Scale=0 vs scale=1 noding inconsistency. Corpus: snap / noding / `GeometryPrecisionReducer` lane. Draft but high risk if scaled noding is wrong. |
 | **7** | [#1145](https://github.com/locationtech/jts/pull/1145) | YStripesPointInAreaLocator | **#67** `relate` (+ JCT) | H | L–M | M | New PIP implementation. Corpus `point_in_ring` + gallery (`nts-oracle-gallery.md`) is the **regression oracle** — run hat/Spectre/vertex-graze/horizontal-edge vectors. |
@@ -65,13 +65,18 @@ Ordered by **risk÷cost** for the proofs corpus (not JTS merge politics).
      + [`docs/jts-311-incircle-lane-2026-08.md`](jts-311-incircle-lane-2026-08.md).  
      Stage A sketch + DDFast lineage; **ε = `ulp(1.0)` = \(2^{-52}\)** (looser than
      Shewchuk \(2^{-53}\)); name is not full `incircleadapt` (#1094). Product tip stays **#1212**.  
-2. **Orientation lane (P0)** — **STARTED 2026-08-05 (FFI rungs):**  
-   Full `libntsrocq` rebuild path after re-extract (`docs/ffi-rungs-2026-08.md`,
-   `scripts/rebuild_oracle_ffi.sh`).  
-   Differential scout: `oracle/gen_jts1093_orient_scout.py` (Ozaki mirror vs
-   Shewchuk Stage A vs `ORIENT_EXACT`).  
-   Note: `ORIENT_EXACT` **FFI** still has a segfault class on extreme coords
-   (parity YELLOW); use `oracle_bin` for exact GT. Keep #1197 green.  
+2. **Orientation lane (P0)** — **LANDED 2026-08-05 (session GREEN):**  
+   - Full `libntsrocq` rebuild path after re-extract (`docs/ffi-rungs-2026-08.md`,
+     `scripts/rebuild_oracle_ffi.sh`).  
+   - Differential scout: `oracle/gen_jts1093_orient_scout.py` — **three-way**
+     mirror (JTS-master `1e-15` vs Ozaki #1093 vs corpus Shewchuk Stage A) vs
+     `ORIENT_EXACT`.  
+   - Table + write-up: `oracle/jts1093_orient_vectors.txt` (45 vectors) +
+     [`docs/jts-1093-orient-lane-2026-08.md`](jts-1093-orient-lane-2026-08.md).  
+   - Gate: 0 CERTAIN conflicts; Ozaki CERTAIN while master UNCERTAIN on **4**
+     same-sign band vectors; Ozaki ↔ corpus Shewchuk certainty splits **0**.  
+   - Note: `ORIENT_EXACT` **FFI** still has a segfault class on extreme coords
+     (parity YELLOW); use `oracle_bin` for exact GT. Keep #1197 green.  
 3. **PIP gallery on #1145 (P0/P1)** — Reuse `docs/nts-oracle-gallery.md` WKT as Java tests / differential.  
 4. **ScaledNoder #90 (P1)** — Scope whether scale=0/1 bug maps to a named snap claim.  
 5. **Coverage #1084 (P1)** — Spec sketch only until #425 cleaner is stable.
@@ -176,7 +181,7 @@ Columns: **Pri** = P0/P1/P2 · **Rel/Cost/Risk** · **Epic**.
 | Cluster | Members | Action |
 |---|---|---|
 | **In-circle robustness** | #311 → #1094 → **#1212** | Treat **#1212 as tip**; archive others as predecessors once merged. History: [`jts-311-incircle-lane-2026-08.md`](jts-311-incircle-lane-2026-08.md). FFI scout + review: [`jts-1094-incircle-lane-2026-08.md`](jts-1094-incircle-lane-2026-08.md). Tip differential: [`jts-1212-incircle-lane-2026-08.md`](jts-1212-incircle-lane-2026-08.md) |
-| **Orientation filters** | #1093 (Ozaki production), #1197 (DD limits tests), #1189 (isCCW test INVALID) | Gate #1093 against corpus exact; keep #1197; mine #1189 for vectors only |
+| **Orientation filters** | #1093 (Ozaki production), #1197 (DD limits tests), #1189 (isCCW test INVALID) | **#1093 lane GREEN** ([jts-1093-orient-lane-2026-08.md](jts-1093-orient-lane-2026-08.md)); keep #1197; mine #1189 for vectors only |
 | **DistanceOp / LineSegment** | #926, #930 | One review pass if either moves; low proof cost |
 | **CI matrix** | #638, #646 | Ignore unless JTS maintainers revive |
 
@@ -230,7 +235,7 @@ Do **not** open multi-session theory work for P2 PRs.
 ## §9 — Suggested one-liner picks for Joost / BDFL
 
 1. **Bet the mesh lane on #1212** (with #1094/#311 as history) — highest corpus leverage per hour.  
-2. **Gate any orientation filter change (#1093) on exact orient** — never merge on vibes.  
+2. **Orientation filter change (#1093) gated on exact orient** — session GREEN; re-run table if the PR is revised.  
 3. **Use the PIP gallery as free CI for #1145**.  
 4. **Ignore ~55% of the open queue** (CI/IO/docs/API) for proof planning.  
 5. **Keep our four PRs** green; only #1197 and #1216 need corpus-adjacent attention.