docs+oracle: SQL/MM type honesty packet + SQLMM_WKT

.github/workflows/build-oracle.yml

@@ -234,6 +234,7 @@ jobs:
             > oracle/obstacle_distance_tests.txt
           ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_arc_distance_tests.py \
             > oracle/arc_distance_tests.txt
+          ORACLE_BIN=oracle/oracle_bin python3 oracle/red_sqlmm_wkt_tests.py
 
       - name: Upload oracle_bin artifact (90-day retention)
         uses: actions/upload-artifact@v4

.gitignore

@@ -40,6 +40,7 @@ __pycache__/
 
 # Prebuilt oracle binary (from CI artifacts for local harden/vector gen; reproducible via Dockerfile+make)
 oracle/oracle_bin
+oracle/sqlmm_wkt_bin
 oracle/extracted.ml
 
 # Local agent / MCP scratch (not part of the corpus)

TRIAGE_NTS_JTS_ISSUES.md

@@ -103,6 +103,10 @@ proven, soundness or coordinates open) · **⬜ planned** (not yet started) ·
 | **AT-\*** | Affine transforms (non-similarity → detect-and-densify, §7 risk) | TRIAGE park | — | ⬜ research park (no statement; `docs/scout/69-closing-summary.md`) |
 | **LRF-\*** | Linear referencing on curves | TRIAGE park | — | ⬜ research park (no statement; `docs/scout/69-closing-summary.md`) |
 | **DSF** | Densifier (curve → chords internally) | #64, #65 | `ArcChordApprox.v` (sagitta bound), `ArcChord{Density,Subdivision,Length,Sound}.v`, `CurveLinearise.v` (`chord_approx_ring_closed`); oracle `CP_BOUNDARY_SIMPLIFY` densify (`densify_arc`) | ✅ chord-approx faithfulness (closure); sagitta/`ring_simple` open |
+| **CRV-CC** | SQL/MM `COMPOUNDCURVE` stays a compound (ISO/IEC 13249-3; no silent chord Flatten) | board CRV-CC · no Proofs epic | [`docs/scout/map-compoundcurve.md`](docs/scout/map-compoundcurve.md); `CurveGeometry.v : CurveSegment`; `CurveLinearise.v : chord_approx_ring_closed`; `HullExactExtrema.v : h_cc_still_densify` (H-CC stays on #424); `LECFlattenRow.v : empty_disk_flatten_iff` is member-min, not chords | 🟡 type + named linearise + I/O identity landed; GEOS leftover named (`ensureNoCurvedComponents` refuse + `getLinearized`). Ticket 30 closed on GEOS. NTS/JTS overlay still `Coordinate[]`. HOLD merge into JTS #7. HOLD a second CompoundCurve type. Do not remint `424-b` / `615-b` |
+| **CRV-CP** | SQL/MM `CURVEPOLYGON` stays a curve polygon (ISO/IEC 13249-3; no silent POLYGON / LinearRing emit) | TRIAGE park · no Proofs epic · `#509` owns Jordan | [`docs/scout/map-curvepolygon.md`](docs/scout/map-curvepolygon.md); `CurveGeometry.v : valid_curve_polygon` (structural); `CurvePolygonSimple.v : curve_polygon_outer_not_simple_of_witness`; `CurvePolygonValid.v : valid_curve_polygon_cp`; `CurveLinearise.v : to_geometry_outer_ring_closed`; `WindingNumber.v : winding_decides_membership` is linear, not curve Jordan; `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` keeps kit-completeness fog | 🟡 type + named linearise + I/O identity landed; GEOS leftover named (OverlayNG + `createSurface` keep CURVEPOLYGON). Ticket 32 closed on GEOS. HOLD merge into JTS #7. HOLD a second CurvePolygon type. Do not remint `#509`. Do not steal ticket 30. Do not flip F-CP / V-CP |
+| **CRV-MC** | SQL/MM `MULTICURVE` stays a multicurve (ISO/IEC 13249-3 §4.2.25; no silent MULTILINESTRING emit) | TRIAGE park · no Proofs epic | [`docs/scout/map-multicurve.md`](docs/scout/map-multicurve.md); `CurveGeometry.v : CurveSegment` is the member alphabet, not the collection; `CurveGeometry.v : valid_curve_geometry` is `list CurvePolygon` (F-MS-shaped), not MultiCurve; `CurveLinearise.v : chord_approx_ring_closed` is named linearise; `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` has `GTMultiLineString` only; `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` keeps kit-completeness fog | 🟡 JTS type + NTS enum + I/O type 11 landed; Coq has no MultiCurve carrier; GEOS leftover named (OverlayNG keeps MULTICURVE). Ticket 34 closed on GEOS. HOLD merge into JTS #7. HOLD a second MultiCurve type. Do not steal tickets 30 / 32. Do not remint `#509`. Do not flip F-CP / F-MC / F-MS |
+| **CRV-MS** | SQL/MM `MULTISURFACE` stays a multisurface (ISO/IEC 13249-3 §4.2.27; no silent MULTIPOLYGON emit) | TRIAGE park · no Proofs epic · `#509` owns per-member Jordan | [`docs/scout/map-multisurface.md`](docs/scout/map-multisurface.md); `CurveGeometry.v : valid_curve_geometry` is `list CurvePolygon` (structural F-MS); `CurveGeometry.v : valid_curve_geometry_nil` / `CurveGeometry.v : valid_curve_geometry_cons`; `CurveGeometry.v : to_geometry` is named collection linearise; `CurveLinearise.v : to_geometry_outer_ring_closed`; `WktGeoJsonRoundtrip.v : wkt_geojson_wkt_roundtrip` has `GTMultiPolygon` only; `OverlayTouchRow.v : phase0_relation_complete_hypothesis_refuted` keeps kit-completeness fog | 🟡 Coq structural collection + JTS type + NTS enum + I/O type 12 landed; GEOS leftover named (`restrictToSurfaces` checks `hasCurvedTypes`). Ticket 36 closed on GEOS. HOLD merge into JTS #7. HOLD a second MultiSurface type. Do not steal tickets 30 / 32 / 34. Do not remint `#509`. Do not flip F-CP / F-MC / F-MS |
 | **BUF-1 / BUF-N** | Single-/multi-arc buffer → `CurvePolygon` | #65 | 18× `Buffer*.v` (linear), `ExtractBufferRings.v`; `CurveBufferArea.v`, `CurveRingOffset.v`, `CurveOffsetAssembly{,Total}.v`, `CurveRoundJoin.v`, **`ClothoidBufferBridge.v`, `ClothoidOffsetContact.v`, `ClothoidBufferAssembly.v`, `CurveRingOffsetSimple.v`** (clothoid chain); oracle `BUFFER_REGION` (+ `ARC_BUFFER_SIMPLE/FULL` pins); **oracle pilot for unified segments + NTS sketch (2026-06)** | 🟡 arc buffer-region boundary+area cert ✅ (3-ax) + d=0 + helpers; **clothoid buffer-ring chain ✅ (2026-06-30): validity → adjacent offset contact → whole-ring assembly cleanliness → non-adjacent simplicity under clearance > 2·\|d\| = simple-closed-curve cert**; oracle pilot + dispatcher sketch for Arc/CS/CC/CP; pure-linear regression zero; Minkowski + unconditional simplicity deferred. |
 | **OFF** | Offset curve (arc-preserving) | #65 | `BufferOffset.v`, `ArcOffset.v`, `ArcOffsetThreePoint.v` (`arc_offset_preserves_arc`), `CurvePolygonOffset.v`, `CurveRingOffset.v`, `ClothoidBufferBridge.v` (`clothoid_ring_offset_valid` + sharpness), `ClothoidOffsetContact.v`, `ClothoidBufferAssembly.v`, `CurveRingOffsetSimple.v`; oracle `ARC_OFFSET_XY` | 🟡 arc offset ✅ (valid arc → valid arc, radius r+d); **clothoid ring offset now soundness-complete at the adjacency level + non-adjacent simplicity gated on a clearance hypothesis (2026-06-30)** |
 | **VBF** | Variable-distance buffer | #65 | — | ⬜ |
@@ -117,6 +121,15 @@ proven, soundness or coordinates open) · **⬜ planned** (not yet started) ·
 | **TRI-VR** | Voronoi on curved input | #68 | — | ⬜ |
 | **TB-\* / F-RD** | TestBuilder rendering / `ShapeWriter` hooks | — | — | — not proof-relevant |
 
+**§4.2.1 types that are not optional extras.** `ST_Clothoid`,
+`ST_Circle`, `ST_GeodesicString`, `ST_NURBSCurve`, `ST_SpiralCurve`
+are instantiable ST_Curve subtypes in ISO/IEC 13249-3 §4.2.1. GEOS
+WKT names them and refuses. Oracle mode `SQLMM_WKT` parses type
+identity (including the SPIRALTYPE open-set lexer deviation). NTS
+WKT names them and refuses (ticket 38). Not leftover `Ⅺ`. Do not
+remint `508-*`. Do not grow `CurveSegment`. Do not flip F-CP / F-MC
+/ F-MS / V-CP.
+
 **Reading the table against the EPIC's Definition of Done (§10).** JTS#1195's
 DoD requires curve-preserving output "**where mathematically sound**" — which is
 exactly what the ✅ rows certify and the 🟡 rows bound. The §7 "arc intersection

docs/gated-prose-docs.txt

@@ -16,3 +16,7 @@ docs/scout/spec-interior-side.md
 docs/scout/map-523.md
 docs/scout/spec-523.md
 docs/scout/map-iso-st-relate-qex.md
+docs/scout/map-compoundcurve.md
+docs/scout/map-curvepolygon.md
+docs/scout/map-multicurve.md
+docs/scout/map-multisurface.md

docs/iso13249-3-curve-type-bindings-2026-08.md

@@ -40,21 +40,30 @@ TYPE` definitions in clauses 5–8):
 | ST_Curve | ST_Geometry | **no** (`NOT INSTANTIABLE`) | §4.2.4 / §7.1.1 | `Curve` (abstract), `Geometries/Curve.cs:10` |
 | ST_LineString | ST_Curve | yes | §4.2.5 / §7.2.1 | `LineString` |
 | ST_CircularString | ST_Curve | yes | §4.2.6 / §7.3.1 | `Curves/CircularString.cs:36` |
+| ST_Circle | ST_Curve | yes | §4.2.7 | absent — **not an optional extra** |
+| ST_GeodesicString | ST_Curve | yes | §4.2.8 | absent — **not an optional extra** |
+| ST_EllipticalCurve | ST_Curve | yes | §4.2.9 | absent — **not an optional extra** |
+| ST_NURBSCurve | ST_Curve | yes | §4.2.10 | absent — **not an optional extra** |
+| ST_Clothoid | ST_Curve | yes | §4.2.11 | absent — **not an optional extra** |
+| ST_SpiralCurve | ST_Curve | yes | §4.2.12 | absent — **not an optional extra** |
 | ST_CompoundCurve | ST_Curve | yes | §4.2.13 / §7.10.1 | `Curves/CompoundCurve.cs:36` |
 | ST_Surface | ST_Geometry | **no** | §4.2.14 / §8.1.1 | `Surface<T>` (abstract), `Geometries/Surface.cs:16` |
 | ST_CurvePolygon | ST_Surface | yes | §4.2.15 / §8.2.1 | `Curves/CurvePolygon.cs:38` (`Surface<Curve>`) |
 | ST_Polygon | ST_CurvePolygon | yes | §4.2.16 / §8.3.1 | `Polygon` — **not** a `CurvePolygon` subtype in NTS (pre-existing hierarchy; deliberate divergence) |
 | ST_MultiCurve | ST_GeomCollection | "may be instantiable" | §4.2.25 | `Curves/MultiCurve.cs:19` |
 | ST_MultiSurface | ST_GeomCollection | "may be instantiable" | §4.2.27 | `Curves/MultiSurface.cs:19` |
 
-The spec also defines further instantiable ST_Curve subtypes the branch does not
-model: ST_Circle (§4.2.7), ST_GeodesicString (§4.2.8), ST_EllipticalCurve
-(§4.2.9), ST_NURBSCurve (§4.2.10), ST_Clothoid (§4.2.11), ST_SpiralCurve
-(§4.2.12 — spiral types "initially limited to" clothoid, bloss, biquadratic,
-sine, cosine). These are the CONTEXT.md "expansion backlog", verified present in
-the spec. §4.2.1 also explicitly permits an implementation to add subtypes and
-to interpose types, provided subtype relationships are preserved — this is the
-clause that legitimises `Curve`/`Surface<T>` as interposed abstractions.
+ST_Circle, ST_GeodesicString, ST_EllipticalCurve, ST_NURBSCurve,
+ST_Clothoid, and ST_SpiralCurve (spiral types "initially limited to"
+clothoid, bloss, biquadratic, sine, cosine) are instantiable ST_Curve
+subtypes in the §4.2.1 hierarchy. They are **not optional extras**.
+The NTS curve-foundation branch does not yet carry them. GEOS and
+NTS WKT name them and refuse; calling them "Unknown type" is a lie.
+§4.2.1 also permits an implementation to add subtypes and to interpose
+types, provided subtype relationships are preserved — that clause
+legitimises `Curve`/`Surface<T>` as interposed abstractions, not a
+licence to drop these types from the model. Do not remint `508-*`.
+Do not grow `CurveSegment`.
 
 ST_Curve semantics that bind every curve subtype (§4.2.4):
 
@@ -267,6 +276,25 @@ items that follow it):
   itself admits any count ≥ 1; the odd-count ≥ 3 rule is semantic
   well-formedness (§7.3.1 Desc 7), enforced when the produced point array feeds
   `NEW ST_CircularString` (§5.1.67 item e).
+- `CIRCLE [ <z m> ] <circle text>` — `EMPTY` or exactly three points
+  (§4.2.7). Oracle mode `SQLMM_WKT` parses this as type identity.
+- `GEODESICSTRING [ <z m> ] <geodesicstring text>` — `EMPTY` or a
+  parenthesised point list, count ≥ 2 (§4.2.8). Same oracle mode.
+- `ELLIPTICALCURVE [ <z m> ] <elliptical text>` — `EMPTY` or named
+  fields `AFFINEPLACEMENT`, `UAXISLENGTH`, `VAXISLENGTH` (and the
+  start/end angles when present) (§4.2.9). Instantiable; not UNKNOWN.
+- `NURBSCURVE [ <z m> ] <nurbs text>` — `EMPTY` or `DEGREE`, `KNOTS`,
+  `CONTROLPOINTS` as weighted points (§4.2.10 / §7.7). Structural
+  parse only; the `N` length token stays a projection, not this mode.
+- `CLOTHOID [ <z m> ] <clothoid text>` — `EMPTY` or `AFFINEPLACEMENT`
+  (`LOCATION`, `REFERENCEDIRECTIONS`), `SCALEFACTOR`, `STARTDISTANCE`,
+  `ENDDISTANCE` (§4.2.11 / §7.8). Structural parse only; the `K`
+  length token stays a projection.
+- `SPIRALCURVE [ <z m> ] <spiralcurve text>` — `EMPTY` or `SPIRALTYPE`
+  `<spiraltype text>` plus optional `AFFINEPLACEMENT` / `LENGTH` /
+  `STARTCURVATURE` / `ENDCURVATURE` (§4.2.12 / §7.9 / ST_SpiralType
+  §7.9.7). The text lexer for `<spiraltype text>` is a documented
+  deviation: see §8.
 - `COMPOUNDCURVE [ <z m> ] <compoundcurve text>`, components are `<curve
   text>` ::= **bare** `<linestring text body>` (a parenthesised point list with
   *no* LINESTRING keyword) | tagged `<circularstring text representation>` |
@@ -549,6 +577,19 @@ spec-adjacent statements, checked:
 - **Published-IS wording**: citations are from the DIS ballot text of the 5th
   edition (N 2593). No claim here was found only in ballot-specific front
   matter, but clause-item numbering in the published 2016 IS could differ.
+- **SPIRALTYPE text lexer**: the standard defines `<spiraltype text>` as
+  free-form `<letters>`, and §5.1.68 length-prefixes the value in WKB, so
+  the value set is open — §4.2.12 lists `clothoid`, `bloss`,
+  `biquadratic`, `sine` and `cosine` only as the *initial* set. Text has
+  no length prefix, and `<letters>` admits the characters that would end
+  the value, so oracle `SQLMM_WKT` reads a spiral type up to the comma
+  or parenthesis that terminates it. Interior spaces are preserved:
+  `SPIRALTYPE Wiener Bogen` parses as an open-set extension (LandXML /
+  railway alignment name; not a new SQL/MM type and not Koc compound).
+  A name containing a comma or a parenthesis is the one case this
+  grammar cannot represent — the leftover token after the terminator
+  is `REFUSE`, not a type value. Pinned by `oracle/red_sqlmm_wkt_tests.py`.
+  Do not remint `508-*`. Do not grow `CurveSegment`.
 
 ---