SSX v5 hardening: theorem-first overlap certification, unified budgets/status, singular-case completeness (L41–L61)

docs/superpowers/specs/2026-07-12-theorem-first-overlap-methodology.md

@@ -0,0 +1,139 @@
+# Theorem-first overlap certification — methodology (USER DECISION 2026-07-12)
+
+**Status:** adopted; implemented for CSX in `_bez_csx4._tolerance_csx_overlap_certificate`
+(ledger L59/L60); CCX's L47 tier is the ancestor. This document is the methodology of
+record for all coincidence handling in mmcore's intersection engines, and the template
+for the future quadric/rational tier (L58).
+
+## 1. The principle (the user's rationale, on record)
+
+Two polynomial/rational Bézier arcs that coincide on **any open sub-arc** lie on the
+same irreducible algebraic curve — coincidence is all-or-nothing, never local.
+Therefore a maximal overlap can only **terminate at a domain boundary** of one of the
+operands: nothing interior to both domains can end it.
+
+The methodological consequence: **do not fight floating point for the interior.**
+Numerics is used only to establish *which structure* we are in:
+
+1. verify the span's ends are **domain-pinned** (see §3),
+2. verify **interior witnesses** are within tolerance,
+3. verify **no interior crossing structure** (see §5),
+
+and then the *theorem*, not the arithmetic, carries the interior of the span. A
+deliberately incomplete numerical proof of a mathematically complete property. This
+replaces two failed regimes:
+
+- **tiny's valley rule** (pre-`5d05ddc`): permissive pairing with no certificate —
+  fast and often right, but provably unsound (merges sub-tolerance-distinct sets;
+  fails every exactness contract).
+- **the 5d05ddc hardening**: exact-affine-only certification with no tier for genuine
+  non-affine overlaps — sound but incomplete; real coincidences (curve on a
+  non-parallelogram planar quad, curve on an extrusion) fell into a subdivision grind
+  and shipped truncated or empty (the "what got overlooked" of this branch).
+
+## 2. Tolerance semantics (resolves the L47 band-bar residual)
+
+**Tolerance-coincidence IS coincidence.** A span whose ends are domain-pinned, whose
+witnesses sit within `atol`, and which carries no interior crossing structure is ONE
+overlap. The `certification` field says which grade:
+
+- `'exact'` — witnesses at roundoff level (the `tiny = 4096·ε·max(1, diag)` floor);
+  algebraic identity in the source-envelope sense.
+- `'tolerance'` — witnesses within `atol`; sets that are distinct-but-within-tolerance
+  are *reported as* coincident-within-tolerance. The exactness property survives in
+  sharpened form: **sub-tolerance-separated sets must never certify `'exact'`**
+  (measured: even a 5e-324 offset stays `'tolerance'`).
+
+Consequences already pinned in tests: parallel offsets at 0.5·atol, sub-atol humps,
+and translated variants all promote as `'tolerance'` with translation-invariant
+residuals (`test_csx4_exactness_contract.py`, `test_ccx4_exactness_contract.py`).
+
+## 3. Domain pinning (with the real-data amendments)
+
+A span end is pinned when any of:
+- it is the **curve's t-domain end** (t=0/1),
+- the projection onto the surface sits on a **uv-domain edge**,
+- **(amendment, measured)** the projection *one grid step outward* clamps to a uv
+  edge — because on real data the tolerance boundary and the domain exit COINCIDE
+  (measured: d crosses atol at almost the same t where the path leaves through u=1,
+  so the projection at the refined boundary is still interior), and
+- **(amendment, measured)** a span end may have **no exact 3-D root at all**: the
+  curve can leave the patch through an edge *region* at sub-atol clearance
+  (measured 6.7e-4 from the edge line). Pins are verified by inversion + residual,
+  never by requiring a boundary zero to exist.
+
+A span with **both ends interior-fading** (distance rising through atol with the
+projection interior) is the **offset-twin signature and is never promoted** — the
+CCX L47 rule, kept verbatim.
+
+## 4. Structural amendments (from the algebraic geometry)
+
+- **Multiplicity of spans:** improper/folded reparameterizations (a degree-6 double
+  traversal) and domain clipping legitimately produce **multiple** pinned spans —
+  the certificate returns a set, never assumes one.
+- **Nodes ride along:** arcs of the same nodal curve can also meet at isolated
+  self-intersection points outside the spans; those stay isolated roots.
+- **Corner contact is not band evidence:** a single-grid-sample in-band run (a graze
+  at one node whose bisection fringe can exceed 4·ptol) is refused; a genuine span
+  must be in-band across ≥ 2 consecutive grid samples (caught live: a 4·atol stub
+  branch at a shared corner).
+
+## 5. The crossing guard (what protects the blood-bought invariants)
+
+The **never-merge-tolerance-touches invariant** (near-tangent loop topology) is
+protected by the *flip guard*, not by refusing overlaps: a transverse (normal-side)
+**sign flip between consecutive interior gap samples** is crossing structure and
+refuses promotion of that span.
+
+- Root-like samples (residual ≤ `tiny`) are bridged (the root is the coincidence).
+- **(amendment, measured)** END-adjacent flips are exempt: a genuine touch AT a
+  pinned span end on real-world-inexact data sits above the roundoff floor (1.6e-9
+  in the fixture) so bridging cannot cover it — it is the span's own endpoint root;
+  the theorem terminates the overlap there anyway. Interior flips still refuse.
+- Sub-atol **valley chains** between strict-distinct zeros never merge: the strict
+  gap-midpoint certificate fails on valley floors (slice-10 lattice-cluster rule,
+  pinned by the 3-root valley-chain negative control).
+
+**Open (user decision pending):** CCX's woven near-coincident twins (crossings at
+fitting-noise amplitude) still refuse per the pinned L47 contract test. If the
+tolerance semantics of §2 should bridge sub-band weaving in CCX too, the candidate
+rule is a *relative* bar (flip flanks ≤ K× the span's median in-band residual =
+noise), which discriminates the pinned ±1.2e-4-crossings-in-band fixture (120,000×
+median → refuse) from fit-noise weaving (~1× median → bridge). Not implemented.
+
+## 6. Cost discipline (the §11.5 lesson, twice)
+
+- **Arming is evidence-gated and cheap:** a curve-end zero on-surface, a valley
+  pair, or a zero-boundary-zero pair (coincident stretches entering AND exiting
+  through patch edges produce NO exact boundary roots — measured; transversal
+  nested calls always carry zeros and never pay the scan).
+- **Split pricing:** the 17-projection arming scan bills 17 cells; the dense pass
+  (65 witnesses + refines) bills 145 **only on a hit**. A flat combined price
+  tripped the work-drift gate on nested cut-face calls (case 15 ×3.61) and a
+  constrained-budget test — the gate caught it live, twice, on the day it was built.
+- Certified spans are **t-excluded from Phase 2**: no subdivision grind inside a
+  certified span. Baselines in `examples/ssx/bez_ssx5_work_baseline.json` refresh
+  only deliberately (`--update-baseline`).
+
+## 7. Measured record (why this methodology is trusted)
+
+| Case | tiny (valley rule) | 5d05ddc..pre-L59 | theorem-first |
+|---|---|---|---|
+| script-3 call 2 (extrusion) | 2.7 s, 1 overlap, unsound rule | 57 s, 0 overlaps, lost geometry | 4.2 s, 1 overlap **(5.9230, 20.1120)** vs tiny's (5.9238, 20.1131) — sub-ptol agreement |
+| L42 parabola-on-bilinear | 1,679 lattice roots "complete" | bounded typed-partial | 1 `'exact'` overlap, 204 cells |
+| bilinear L-junction (fixtures A/B) | — | branch truncated to 37%/11% | both branches full, linked to the tangent point |
+| exactness contracts | FAIL (merges distinct sets) | pass | pass (re-pinned, sharpened never-'exact') |
+
+**The remaining fundamental cost:** inputs whose answer is genuinely delicate
+(clearance ≈ atol, fast-rotating normals, real near-tangencies) must be resolved at
+tolerance scale by any *honest* method. tiny was faster there only by answering wrong.
+
+## 8. Known incompleteness (merge-blocking, ledger L61)
+
+The user reports the bilinear non-affine family **still loses part of the second
+branch** in their environment. At HEAD `f6d0015` every constructible variant passes
+(A/B/C plus both order-swapped forms D/E: full 9.763-length branches, linked tangent
+point, complete). The failing configuration is therefore not yet captured: it may be
+the NURBS-level driver (non-unit knots), a geometry variant, or a stale checkout.
+**Repro-first is mandatory**: no fix without the user's exact failing script and
+geometry. The branch does not merge to `tiny` until this is closed.

examples/ccx/multiple_int_3d.py

@@ -216,13 +216,13 @@
         viewer.add(curve, color=color)
     for pt in isolated['point']:
 
-        viewer.add(pt, color=(0.0, 1.0, 0.5,1.0),size_px=13)
+        viewer.add(pt, color=(0.0, 1.0, 0.5,1.0),size_px=6)
     if overlaps is not None:
 
 
         for start,end in overlaps['point']:
-            viewer.add(start, color=(0.0, 1.0, 0.5, 1.0), size_px=13)
-            viewer.add(end, color=(0.0, 1.0, 0.5, 1.0), size_px=13)
+            viewer.add(start, color=(0.0, 1.0, 0.5, 1.0), size_px=6)
+            viewer.add(end, color=(0.0, 1.0, 0.5, 1.0), size_px=6)
 
 
 

examples/ccx/multiple_int_new_2d.py

@@ -62,7 +62,7 @@
 from mmcore.numeric.intersection.ccx._nccx4 import nurbs_ccx,nurbs_ccx_multiple
 from mmcore.extras.renderer.renderer3d import Viewer,OrbitCamera
 
-isolated,overlaps=nurbs_ccx_multiple(val,rational=True)
+isolated,overlaps,_status=nurbs_ccx_multiple(val,rational=True)
 print('isolated:')
 print(isolated)
 print('overlaps:')

examples/ccx/multiple_int_new_3d.py

@@ -202,7 +202,7 @@
 args=parser.parse_args()
 
 
-isolated,overlaps=nurbs_ccx_multiple(val,tol=0.001,rational=True)
+isolated,overlaps,_status=nurbs_ccx_multiple(val,tol=0.001,rational=True)
 print('\n\nOUT\n')
 print(len(isolated) if isolated is not None else 0,len(overlaps) if overlaps is not None else 0)
 print(isolated,overlaps)
@@ -217,13 +217,13 @@
         viewer.add(curve, color=color)
     for pt in isolated['point']:
 
-        viewer.add(pt, color=(0.0, 1.0, 0.5,1.0),size_px=13)
+        viewer.add(pt, color=(0.0, 1.0, 0.5,1.0),size_px=6)
     if overlaps is not None:
 
 
         for start,end in overlaps['point']:
-            viewer.add(start, color=(0.0, 1.0, 0.5, 1.0), size_px=13)
-            viewer.add(end, color=(0.0, 1.0, 0.5, 1.0), size_px=13)
+            viewer.add(start, color=(0.0, 1.0, 0.5, 1.0), size_px=6)
+            viewer.add(end, color=(0.0, 1.0, 0.5, 1.0), size_px=6)
 
 
 

examples/ccx/tangential_int_2d.py

@@ -37,10 +37,10 @@
 
 curve3=curve2._replace(control_points=curve2.control_points-(translate_vec[np.newaxis,:]))
 
-isolated1,overs1=nurbs_ccx(curve1,curve2,tol)
+isolated1,overs1,_status1=nurbs_ccx(curve1,curve2,tol)
 
 # curve1 x curve3 is not overlap!
-isolated2,overs2=nurbs_ccx(curve1,curve3,tol)
+isolated2,overs2,_status2=nurbs_ccx(curve1,curve3,tol)
 viewer=Viewer(camera=OrbitCamera(target=(-0.5 , 1.2,0.,),up=(0,1.,0.), ortho_half_height=1,distance=1,yaw= -3*np.pi/2,pitch= -np.pi/2))
 viewer.cam.lock_orbit(True)
 
@@ -52,8 +52,8 @@
 for pt in isolated1['point']:
 
     viewer.add(pt
-                    , color=(0.7, 0.9, 0.0, 1.0),size_px=13)
+                    , color=(0.7, 0.9, 0.0, 1.0),size_px=6)
 
 for pt in isolated2['point']:
-    viewer.add(pt, color=(0.0, 0.6, 1.0, 1.0),size_px=13)
+    viewer.add(pt, color=(0.0, 0.6, 1.0, 1.0),size_px=6)
 viewer.run()

examples/csx/nurbs_nurbs_intersection_1_new.py

@@ -0,0 +1,149 @@
+import numpy as np
+import rich
+
+from mmcore.geom._nurbs_eval import _nurbs_to_tuple, evaluate_nurbs_curve
+
+from mmcore.numeric.intersection.csx._ncsx4 import nurbs_csx
+
+cpts = np.array(
+    [
+        [-9.1796875, 13.229166666666666, -4.5186767578125],
+        [-9.1796875, 14.739583333333332, -4.49395751953125],
+        [-9.1796875, 16.432291666666664, -4.580108642578125],
+        [-9.1796875, 18.372395833333332, -4.8531036376953125],
+    ]
+)
+spts = np.array(
+    [
+        [
+            [-5.849180481790346, 18.372395833333336, -1.5018374203712104],
+            [-5.858792686592141, 16.432291666666668, -2.719633841323509],
+            [-5.871782152540512, 14.739583333333334, -3.1229032219131403],
+            [-5.8852911971268185, 13.229166666666668, -3.116512598566417],
+        ],
+        [
+            [-6.88688536134276, 18.372395833333336, -1.6832837287863824],
+            [-6.894094514944105, 16.432291666666668, -2.9325012796112815],
+            [-6.9038366144053835, 14.739583333333334, -3.3409109281989706],
+            [-6.913968397845114, 13.229166666666668, -3.3217200441495054],
+        ],
+        [
+            [-7.97766402100707, 18.372395833333336, -2.2658223298287345],
+            [-7.983070886208079, 16.432291666666668, -3.617300740689732],
+            [-7.990377460804037, 14.739583333333334, -4.0455099012702895],
+            [-7.997976298383835, 13.229166666666668, -3.992029157974829],
+        ],
+        [
+            [-9.1863730157553, 18.372395833333336, -2.7409113689805125],
+            [-9.190428164656058, 16.432291666666668, -4.174381706229336],
+            [-9.195908095603027, 14.739583333333334, -4.61538352236864],
+            [-9.201607223787876, 13.229166666666668, -4.527011611303911],
+        ],
+    ]
+)
+
+import argparse
+import time
+
+import rich
+
+from mmcore.geom._nurbs_eval import _tuple_to_nurbs, _curve_interval, evaluate_nurbs_curve
+from mmcore.geom._nurbs_knots import trim_curve
+from mmcore.numeric.intersection.csx._ncsx4 import nurbs_csx
+import logging
+from mmcore.geom.nurbs_iso import extract_surface_boundaries_tuple
+# Creating intersection objects
+import numpy as np
+from mmcore.geom._nurbs_eval import NURBSSurfaceTuple
+def parse_args():
+    parser = argparse.ArgumentParser()
+    ssx_params = parser.add_argument_group(title="CSX Parameters")
+    ssx_params.add_argument("--atol", type=float, default=1e-3)
+
+
+    general_params = parser.add_argument_group(title="General")
+    general_params.add_argument('--viewer', action='store_true')
+
+    return parser.parse_args()
+
+
+args = parse_args()
+
+
+from mmcore.geom.nurbs import NURBSCurve, NURBSSurface
+
+
+surface: NURBSSurfaceTuple =_nurbs_to_tuple( NURBSSurface(np.array(spts), (3, 3)))
+
+curve = _nurbs_to_tuple(NURBSCurve(cpts))
+# ress = new_intersection_candidates(surf, curve, u, v, t, np.array(surf.evaluate_v2(u, v)))
+
+import time
+
+s = time.time()
+
+result = nurbs_csx(curve, surface,tol=args.atol)
+
+print(f"CSX v4 performed at: {time.time()-s} secs.")
+print('isolated:')
+if result[0] is not None:
+    rich.print(result[0])
+print('overlaps:')
+if result[1] is not None:
+    rich.print(result[1])
+isolated,overlaps=result[0],result[1]
+
+if args.viewer:
+
+    try:
+        if args.viewer:
+            from mmcore.extras.renderer.renderer3d import Viewer, OrbitCamera
+
+            viewer = Viewer(camera=OrbitCamera(target=surface.control_points.reshape(-1, 3).mean(axis=0)))
+            srf = viewer.add_nurbs_surface(surface, color=(0.7, 0.7, 0.7, 1.), surface_color=(0.5, 0.5, 0.9, 0.1),
+                                           v_count=4)
+
+
+            def render_result(result, curve, surface=None):
+                if surface is not None:
+                    srf = viewer.add_nurbs_surface(surface, color=(0.3, 0.3, 0.3, 0.05), v_count=4)
+
+                crv = viewer.add(curve, color=(0.9, 0.9, 0.9, 1.0))
+                isolated, overlaps,_ = result
+                if isolated is not None:
+                    uvs = []
+                    for pt in isolated:
+                        viewer.add(pt['point'], color=(0.0, 1.0, 0.5, 1.0), size_px=6)
+
+                if overlaps is not None:
+
+                    for overlap in overlaps:
+                        t0, t1 = overlap['t_range']
+
+                        viewer.add(evaluate_nurbs_curve(curve, t0, d_order=0)['C'], color=(0.0, 1.0, 0.5, 1.0),
+                                   size_px=6)
+                        viewer.add(evaluate_nurbs_curve(curve, t1, d_order=0)['C'], color=(0.0, 1.0, 0.5, 1.0),
+                                   size_px=6)
+
+                    for o in overlaps:
+
+                        t0 = o["t_range"][0]
+                        t1 = o["t_range"][-1]
+
+                        pts = np.linspace(t0, t1, 800)
+                        for t in pts:
+                            evl = evaluate_nurbs_curve(curve, t, d_order=0)
+                            viewer.add_point3d(evl['C'], color=(0.0, 1.0, 0.5, 1.0), size_px=3)
+
+
+            render_result(result, curve)
+
+            viewer.run()
+
+
+    except ModuleNotFoundError as err:
+        print("mmcore.renderer is not installed, skip preview.")
+    except ImportError as err:
+        print("mmcore.renderer is not installed, skip preview.")
+    except Exception as err:
+        raise err