Scope. This is the proof / oracle reference, not a
JTS/NTS test runner. The cross-project differential harness lives downstream in
NetTopologySuite.Curve; here we report what is formally proven and
which extracted oracle vectors back it, and link out to the upstream projects.
Proven / conditional / oracle distinctions are kept explicit — there is no
flattened “all green” health score.Macro · Meso · Micro
How the corpus is navigated for humans, auditors, and agents.
~thousands of statements are not maintained as a flat list — they are a
three-scale stack tied to board epics (#64–#69), modules, and
machine tags. Full write-up:
docs/macro-meso-micro.md.
Macro
Domains & epics
Human-scale navigation. One board epic / topic owns a geometry family.
topic: mesh·relate·arc·koc· …- Issues #64–#69 (plus teaching ladder)
- Blast cone starts at domain epicenter
Meso
Modules (.v files)
Audit atoms — not 5k+ free-floating theorems. ~hundreds of modules with Require edges.
- Layer law: core → predicates → overlay → Jordan → arcs → mesh
- ADR-0001: Jordan needs Overlay; rocq makefile
- Self-contained smoke / tripwire files when Overlay blocks
Micro
Claims & witnesses
RGR unit of work: one claim, one witness, one Eval→Qed.
claimId: 68-a(board) or micro seedeven-squarewitness: empty-circle·(* WITNESS {…} *)- Red → Green → Refactor; mutation checks vacuity
topic: mesh
claimId: 68-a
witness: empty-circle
Machine header for PRs. topic: = macro · claimId: = micro board key ·
witness: = falsifier for eval/mutation. Use claimId: none /
witness: none only when intentionally off-board.
Dynamic micro-kernel claims register from board sync / WITNESS payloads.
1019
Cited theorems
in docs/verified-claims.md
910
Proven (unconditional)
[exact] · [full-b64] · [int-b64]
22
Conditional headlines
[cond] — named hypotheses
1287
Oracle vectors
across 52 differential modes
exact (exact reals) 832full-b64 (all finite binary64) 33int-b64 (int-coord binary64) 17int-b64-arc (int-coord binary64 (arc)) 12int (exact integer (0 axioms)) 16cond (conditional (named hyps)) 22oracle (extracted / differential) 0
Issue tracker (#64–#69) — macro epics
| Issue | Area | Priority | Verdict (from TRIAGE) |
|---|---|---|---|
| #64 | Circular-arc primitives (length, sweep, in-arc, in-circle) | Immediate | Keep Immediate — D-PT fully closed (arc point-distance Qed); arc-arc quartic coords remain |
| #65 | Buffer / offset curve correctness | Urgent | Keep Urgent — clothoid buffer-ring soundness chain (validity → adjacent contact → whole-ring assembly → clearance simplicity) landed; Minkowski + unconditional simplicity deferred |
| #66 | Precision / snap-rounding / OverlayNG soundness | Urgent | Keep Urgent — largely delivered, closing gaps |
| #67 | RelateNG / 9IM matrix & boundary handling | Immediate | Keep Immediate — 67-c exterior-row pin + JCT/Jordan landed; S15l+ pipeline leftovers remain. Ticket 523 grilled 2026-08-30 (`docs/scout/map-523.md`); still open, not accepted (`RelateCurveMatrix.v : cell_none_iff_empty`) |
| #68 | Delaunay triangulation / Voronoi correctness | Non-urgent | Predicate + flip algebra + edge ↔ empty-circle (weak skeleton) + **local Delaunay / flip-refutes-both banked**; active residue is global/covering DT existence + geometric insert correctness + Voronoi dual |
| #69 | Umbrella / epic tracker | Expectant | Owner review retires the tracker — this row is not "SQL/MM is done" |
Feature × geometry-type coverage
Which NTS operations have mechanically-verified proofs for
each curve geometry type. Column headers:
CS = CircularString, CC = CompoundCurve,
CP = CurvePolygon,
Multi = MultiCurve / MultiSurface — the
abbreviations used by the grootstebozewolf/jts fork, so a row
reads the same in both trackers. Arc = CircularArc is this
corpus's single-arc primitive, not a geometry type: an Arc theorem
is not a CS theorem until something concatenates it.
Hover a cell for the source-of-record lemma or the reason it is empty.
Read the icons with care: they are driven by theorem and
oracle-tag counts, and every red_*_unified_tests.py
file carries one blanket geom:arc,cs,cc,cp,multi tag, so a
single unified file credits itself to all five columns at once. The hover
note is the honest per-column reading.
| Feature \ Geometry | Arc | CS | CC | CP | Multi |
|---|---|---|---|---|---|
| Distance | ✅ | ⚠️ | ⚠️ | ⚠️ | ⚠️ |
| Arc / chord length | ✅ | ✅ | ✅ | ✅ | ✅ |
| Area / perimeter | ✅ | ✅ | ✅ | ✅ | ⚠️ |
| Relate (DE-9IM) | ⚠️ | ⚠️ | ⚠️ | ⚠️ | ⚠️ |
| Intersection / Overlay | ⚠️ | ⚠️ | ⚠️ | ⚠️ | ⚠️ |
| Buffer | ✅ | ✅ | ✅ | ⚠️ | ⚠️ |
| Join continuity (C¹ / C²) | ✅ | ✅ | ✅ | ❌ | ❌ |
| LEC / MIC | ✅ | ✅ | ✅ | ✅ | ✅ |
✅ Qed (unconditional) ⚠️ partial / conditional ❌ no corpus coverage — hover a cell for theorem counts + source note.
Laser ratchet — exact curves vs densified
The laser is the curve-preserving path; the
chainsaw is densify-then-compute. These are engine-side measurements
from the JTS fork, vendored into
docs/laser-ratchet.json so this page keeps reporting only on
data that lives in this repo. They are timings, not proofs — no
theorem below depends on them.
Contract: t_laser ≤ 1.15 × t_chainsaw · measured per curve type (EXACT_CURVE_BIBLE §6, §7)
JTS Year-1 is ExactCircularArc (measured). The Year-2 zoo types are library work, not JTS PR 7 — not missing lasers that PR still owes.
ExactCircularArc ✅ measuredExactEllipticalArc library work, not JTS PR 7ExactCubicBezier library work, not JTS PR 7ExactClothoid library work, not JTS PR 7ExactNurbsSegment library work, not JTS PR 7
Per-curve-type ratchet — ExactCircularArc
| Gate | Operation | Laser | Chainsaw | Ratio | Conditions |
|---|---|---|---|---|---|
P1-A | static length vs densified polyline | 20.4 ms | 168.3 ms | ✅ 0.121× | total over 50,000 calls · seed 0xa7ea0001, N=1000000, box [-100,100]², nChord=64 |
P1-B | arc orientationIndex vs densified | 16.6 ms | 141.1 ms | ✅ 0.118× | p50 over 50,000 calls · straight parity 100%; arc-vs-densify agreement A1=0.996151, A2=0.999996 |
Operation gates — red baseline vs current
Each pair is laser / chainsaw. Red is the state that opened the gate; current is after the laser landed. The red column is kept deliberately — the interesting number is that overlay started 30× slower than densifying, not that it now wins.
| Case | Red laser / chainsaw | Red ratio | Current laser / chainsaw | Current ratio | |
|---|---|---|---|---|---|
| OverlayNGCurvePerfGateTest · operation/overlayng/curve · chainsaw leg: chord overlay (~1570-vertex densified) — current column is the R1.5 two-arc lens, not the chord overlay | |||||
| disjoint CAP | 4.169 / 0.139 ms | ❌ 30.000× | 0.001 / 0.092 ms | ✅ 0.016× | |
| nested CAP | 7.894 / 0.646 ms | ❌ 12.200× | 0.211 / 0.599 ms | ✅ 0.350× | |
| nested CUP | 7.914 / 0.563 ms | ❌ 14.100× | 0.165 / 0.319 ms | ✅ 0.520× | |
| crossing CAP | 3.712 / 0.339 ms | ❌ 11.000× | 0.017 / 0.681 ms | ✅ 0.025× | |
| CurveOpsDistConPerfGateTest · geom/curve · chainsaw leg: CurveOps.linearise(g) then the core algorithm | |||||
| distance far discs | 4.735 / 4.000 ms | ❌ 1.180× | 0.009 / 4.797 ms | ✅ 0.002× | |
| distance arc-point | 0.071 / 0.069 ms | ✅ 1.020× | 0.001 / 0.097 ms | ✅ 0.015× | |
| convexHull disc | 1.031 / 1.064 ms | ✅ 0.970× | 0.003 / 1.141 ms | ✅ 0.003× | |
| convexHull half-arc | 0.369 / 0.356 ms | ✅ 1.040× | 0.002 / 0.533 ms | ✅ 0.004× | |
| buffer disc +1 | 0.802 / 0.342 ms | ❌ 2.350× | 0.001 / 0.807 ms | ✅ 0.002× | |
| DistanceConstructionPerfGateTest · app (jtstest.function) · chainsaw leg: densified geometry then the core algorithm | |||||
| Hausdorff two discs | 29.215 / 29.212 ms | ✅ 1.000× | 0.007 / 15.500 ms | ✅ 0.000× | |
| Hausdorff arc-baseline | 0.049 / 0.049 ms | ✅ 1.000× | 0.009 / 0.063 ms | ✅ 0.140× | |
| nearest arc-point | 0.016 / 0.012 ms | ❌ 1.290× | 0.001 / 0.105 ms | ✅ 0.010× | |
| MIC disc | 0.738 / 0.386 ms | ❌ 1.910× | 0.001 / 0.971 ms | ✅ 0.001× | |
| ReverseDispatchPerfGateTest · geom/curve · chainsaw leg: densified receiver, reversed dispatch — single recorded table — no red baseline was transcribed | |||||
| rev intersects far | not transcribed | 0.000 / 0.241 ms | ✅ 0.001× | ||
| rev intersects crossing | not transcribed | 0.072 / 0.399 ms | ✅ 0.181× | ||
| rev contains far | not transcribed | 0.000 / 0.124 ms | ✅ 0.003× | ||
| rev covers nested | not transcribed | 0.001 / 0.071 ms | ✅ 0.019× | ||
| rev distance point-arc | not transcribed | 0.003 / 0.192 ms | ✅ 0.015× | ||
| rev isWithinDistance far | not transcribed | 0.000 / 0.154 ms | ✅ 0.002× | ||
| rev disjoint CAP | not transcribed | 0.111 / 0.175 ms | ✅ 0.635× | ||
| rev nested CAP | not transcribed | 0.069 / 0.606 ms | ✅ 0.114× | ||
| rev nested CUP | not transcribed | 0.057 / 0.342 ms | ✅ 0.167× | ||
| rev crossing CAP | not transcribed | 0.235 / 1.073 ms | ✅ 0.219× | ||
Gates live but unmeasured
A 1.15× assertion is armed in each of these, but no numbers have been transcribed: CurveWKBPerfGateTest, DirectedHausdorffDistancePerfGateTest, DiscreteHausdorffDistancePerfGateTest, DiscreteFrechetDistancePerfGateTest, LargestEmptyCirclePerfGateTest.
Provenance
Imported 2026-08-22 from grootstebozewolf/jts PR #7, branch feature/sfa-curve-rgr, tip c956b50d. Method: nanoTime, median of 31 samples after 15 warmups (WARMUP=15, SAMPLES=31, NOISE=1.15), OpenJDK 21, single machine.
- Hand-transcribed from javadoc and markdown tables in the fork. There is no JMH and no BenchmarkDotNet anywhere in the tree, and no captured run artifacts — every surefire report directory was searched and holds no perf output. Timings are printed to stdout at runtime and discarded.
- One measurement run, replicated byte-identically across all 13 jts-* worktrees (verified by md5) — not 13 independent runs. Treat as n=1.
- The chainsaw baseline is not stable between harness runs (Hausdorff two discs reads 29.212 ms in the red table and 15.5 ms in the current one; far discs 4.000 then 4.797). Ratios are comparable within a table, not across tables.
- A holding-gate count is not the ratchet. doc/LASER_RATCHET.md reports 'measured 11 (11 hold)' with no backing timing table; only the rows below have numbers.
Cited theorems by area — 1019 total
Each bar shows the regime mix of that section's claims (colours match the legend above).
| Section | Claims | Regime mix |
|---|---|---|
| Phase 0 — Robust orientation (CCW / `Orientation.Index`) | 21 | |
| Issue #67 — RelateNG / DE-9IM (all sessions) | 260 | |
| Phase 1 — Robust segment intersection (`RobustLineIntersector`) | 8 | |
| Phase 2 — Snap rounding (Hobby / Halperin–Packer noder) | 37 | |
| Phase 3 — Planar overlay (OverlayNG) | 142 | |
| Phase 4 — Native curves (linearization, chord-approx arcs) | 84 | |
| Koc compound curves — satellite-survey railway alignment (`CompoundCurveKoc.v`) | 27 | |
| Curve ring contact, boundary meet and the inscribed reduction (`RingContactSound.v`, `RelateCurveArcSegment.v`, `RelateCurveBoundaryMeet.v`, `RelateCurveInscribedGeometry.v`, `OverlayContactSound.v`) | 17 | |
| Foundational — squared distance / degenerate cases (`Distance.v`) | 53 | |
| Discrete → Sh(ℝ²) bridge — spatial-topos foundations (`HeytingOpens.v`, `PlaneConnected.v`, `DiscreteShBridge.v`) | 15 | |
| MIC — maximum inscribed circle of the unit square (`MaximumInscribedCircle.v`, board #9004 / epic #813) | 3 | |
| LEC — largest empty circle over the side midpoints (`LargestEmptyCircle.v`, board card pending / epic #813) | 3 | |
| Cell pruning bound — Polycenter / JTS Cell.getMaxDistance soundness (`CellRadiusBound.v`, board #9004 / 9004-d, epic #813) | 4 | |
| OverlayNGCurve Phase 0 — the exact-cell kernel of the four ops (`OverlayNGCurve.v`) | 5 | |
| Circular noding rung 1 — arc split at an N-AA node (`ArcSplitAtNode.v`) | 5 | |
| LEC chord-path hypothesis — disproved on the circle cell (`LECChordGap.v`) | 5 | |
| LEC typed obstacle distance — the laser's metric, proven exact (`LECObstacleDistance.v`) | 8 | |
| LEC arc row — the CircularString window priced total and gated right (`LECArcRow.v`) | 6 | |
| LEC flatten row — the collection min-fold priced exact, n-ary (`LECFlattenRow.v`) | 7 | |
| LEC segment row — the LineString facet metric priced exact (`LECSegmentRow.v`) | 6 | |
| OverlayNGCurve case matrix — candidate completeness refuted, repaired with TOUCH (`OverlayTouchRow.v`) | 11 | |
| G1 does not forbid self-kiss — one-body anti-collapse (`OverlaySelfKiss.v`) | 7 | |
| Curved-polygon CAP after exact noding — named obligation, disc slice Qed (`CurvedCapObligation.v`) | 7 | |
| Curved-polygon CUP / SUB / XOR after exact noding — parameterized obligation, disc slice Qed (`CurvedOpObligation.v`) | 8 | |
| Two-body kiss on curved polygons — named obligation, disc/TOUCH slice Qed (`CurvedKissObligation.v`) | 12 | |
| The TOUCH pair's DE-9IM — FF2F01212, every cell point-set-backed (`RelateTouchDiscs.v`) | 4 | |
| LEC candidate completeness, witness-scoped — the enumeration contains every maximiser (`LECCandidateVertex.v`) | 6 | |
| LEC candidate completeness, general — the theorem a trusted O(n log n) LEC needs (`LECCandidateComplete.v`) | 6 | |
| LEC candidate completeness, WEIGHTED — the Apollonius summit (`LECCandidateWeighted.v`) | 5 | |
| MIC chord-necessity — refuted: the cell certificate is chord-free, and chords are inexact (`MICChordNecessity.v`) | 4 | |
| V-CS — even CircularString controls are valid only as the closed 4-point annulus (`CircularStringValid.v`) | 4 | |
| EX-CS-4 — four-item CIRCULARSTRING(A,B,C,A) is not a PostGIS control count (`CircularStringOddCount.v`) | 4 | |
| Issue #508 — the canonical metric-length spec (`CurveLength.v`) | 4 | |
| Issue #508 — arc rectifiability: r·θ meets the spec (`ArcRectifiable.v`) | 3 | |
| Issue #508 — the 3-point arc meets the parameterized circle (`ArcParamBridge.v`) | 2 | |
| Issue #508 — the mid-disambiguated traversal meets the spec (`ArcTraversalBridge.v`) | 2 | |
| Issue #508 — ellipse rung 1: two tiers against the spec (`EllipseLength.v`) | 3 | |
| Issue #508 — ellipse rung 2: shift invariance + the rx = ry circular bridge | 3 | |
| Issue #508 — ellipse rung 3: the Rmin lower sandwich | 4 | |
| Issue #508 — Bézier rung 1: degree-elevation exactness + the control-net Lipschitz bound (`Bezier3Length.v`) | 3 | |
| Issue #508 — clothoid rung 1: arc-length parameterization + the generic primitive engine (`ClothoidLength.v`) | 3 | |
| Issue #508 — NURBS rung 1: the rational quadratic (`NurbsQuadraticLength.v`) | 3 | |
| Issue #508 — Bézier P0: tight control-polygon bound (`Bezier3Polygon.v`) | 2 | |
| Issue #508 — ellipse P1: elliptic-E Technique-park discharge (`EllipseLength_E.v`) | 2 | |
| Issue #508 — clothoid P1: windowed unit-speed discharge (`ClothoidLength_unit.v`) | 2 | |
| Issue #508 — NURBS P1: general degree, knot spans, exact primitive (`NurbsGeneralLength.v`) | 2 | |
| Issue #508 — arc P2: through-mid point-set + valid_arc sweep pin (`ArcMidSweep.v`) | 2 | |
| Issue #508 — spec rung: monotone reparameterization invariance (`CurveLength.v`) | 2 | |
| Issue #508 — spec rung: orientation-reversing reparameterization (`CurveLength.v`) | 3 | |
| Issue #508 — NURBS conic exact tier: golden quarter = π/2 (`NurbsConicExact.v`) | 2 | |
| Issue #508 — integral machinery: speed-integral premises (`SpeedIntegral.v`) | 3 | |
| Issue #508 — elliptic-E pack instance (`EllipseSpeedIntegral.v`) | 3 | |
| Issue #508 — Bernstein / rational framework (`BernsteinBasis.v`) | 4 | |
| Issue #508 — QED ∨ QEX stop (`ExactCurveEpic508.v`) | 3 | |
| Issue #508 — Fresnel pack + inhabitant (`ClothoidFresnel.v`, `ClothoidFresnelInhab.v`) | 5 | |
| Issue #508 — multi-span NURBS: knot-vector additivity (`NurbsKnotSpans.v`) | 3 | |
| Issue #508 — wrap-up: M-LEN-ZOO + Bible §4.2 satisfaction (`508-h`) | 6 | |
| ADR-0007 — sheet / hen / cook noding constructor (Accepted) | 151 |
Oracle coverage — 52 modes, 1287 vectors
Extracted differential-test vectors (with reference expected
outputs) the C# port is checked against. Run via
oracle/driver.ml (RocqRefRunner).
| Mode | Kind | Vectors | Source |
|---|---|---|---|
ARC_DISTANCE | tests | 128 | oracle/arc_distance_tests.txt |
OBSTACLE_DISTANCE | tests | 95 | oracle/obstacle_distance_tests.txt |
DE9IM_TRIANGLE | vectors | 59 | oracle/de9im_triangle_vectors.txt |
ARC_SEGMENT_DISTANCE | tests | 54 | oracle/arc_segment_distance_tests.txt |
ARC_OFFSET | tests | 50 | oracle/arc_offset_tests.txt |
ARC_SEGMENT | tests | 50 | oracle/arc_segment_tests.txt |
JTS1093_ORIENT | vectors | 45 | oracle/jts1093_orient_vectors.txt |
DE9IM_AREA_AREA | vectors | 42 | oracle/de9im_area_area_vectors.txt |
DE9IM_LINE_LINE | vectors | 36 | oracle/de9im_line_line_vectors.txt |
ADVERSARIAL | tests | 35 | oracle/adversarial_tests.txt |
ARC_BUFFER_SIMPLE | tests | 34 | oracle/arc_buffer_simple_tests.txt |
ARC_CENTROID | tests | 34 | oracle/arc_centroid_tests.txt |
IEEE_ORACLE_BRIDGE | tests | 34 | oracle/ieee_oracle_bridge_tests.txt |
ARC_AREA_CENTROID | tests | 33 | oracle/arc_area_centroid_tests.txt |
CURVE_RELATE_MATRIX | tests | 33 | oracle/curve_relate_matrix_tests.txt |
JTS1212_INCIRCLE | vectors | 29 | oracle/jts1212_incircle_vectors.txt |
WINDING_NUMBER | tests | 28 | oracle/winding_number_tests.txt |
JTS1094_INCIRCLE | vectors | 27 | oracle/jts1094_incircle_vectors.txt |
ARC_ARC_DISTANCE | tests | 26 | oracle/arc_arc_distance_tests.txt |
CP_BOUNDARY_SIMPLIFY | tests | 24 | oracle/cp_boundary_simplify_tests.txt |
DE9IM_ARC_CHORD | vectors | 24 | oracle/de9im_arc_chord_vectors.txt |
DE9IM_AREA_LINE | vectors | 24 | oracle/de9im_area_line_vectors.txt |
DISC_OVERLAY | tests | 23 | oracle/disc_overlay_tests.txt |
ARC_ARC | tests | 21 | oracle/arc_arc_tests.txt |
ARC_SIMPLIFY_DECISION | tests | 18 | oracle/arc_simplify_decision_tests.txt |
BUFFER_REGION | tests | 18 | oracle/buffer_region_tests.txt |
DE9IM_BEZIER3 | vectors | 18 | oracle/de9im_bezier3_vectors.txt |
DE9IM_CLOTHOID | vectors | 18 | oracle/de9im_clothoid_vectors.txt |
DE9IM_ELLIPTIC | vectors | 18 | oracle/de9im_elliptic_vectors.txt |
ARC_OFFSET_FILTERED | tests | 15 | oracle/arc_offset_filtered_tests.txt |
DE9IM_CURVE_AREA_POINT | vectors | 14 | oracle/de9im_curve_area_point_vectors.txt |
JTS1145_PIP_GALLERY | vectors | 14 | oracle/jts1145_pip_gallery_vectors.txt |
LEC_CIRCLE | tests | 14 | oracle/lec_circle_tests.txt |
POINT_IN_CURVE_RING | tests | 14 | oracle/point_in_curve_ring_tests.txt |
I_CIRCULAR | tests | 13 | oracle/i_circular_tests.txt |
RED_LENGTH_UNIFIED_ZOO | red-tests | 13 | oracle/red_length_unified_zoo_tests.py |
RING_SIMPLE | tests | 13 | oracle/ring_simple_tests.txt |
ARC_AREA | tests | 12 | oracle/arc_area_tests.txt |
ORIENTATION_PROOF | vectors | 9 | oracle/orientation_proof_vectors.txt |
HOLES_DISJOINT | tests | 8 | oracle/holes_disjoint_tests.txt |
RED_CURVE_LINEAL_RELATE | red-tests | 8 | oracle/red_curve_lineal_relate_tests.py |
RED_DISTANCE_UNIFIED | red-tests | 8 | oracle/red_distance_unified_tests.py |
RED_OVERLAY_UNIFIED | red-tests | 8 | oracle/red_overlay_unified_tests.py |
CP_RING_SIMPLE | tests | 7 | oracle/cp_ring_simple_tests.txt |
RED_BUFFER_UNIFIED | red-tests | 7 | oracle/red_buffer_unified_tests.py |
RING_ORIENTATION | tests | 7 | oracle/ring_orientation_tests.txt |
DE9IM_ARC_ANALYTIC | vectors | 6 | oracle/de9im_arc_analytic_vectors.txt |
PASSES_THROUGH_PROOF | vectors | 6 | oracle/passes_through_proof_vectors.txt |
RED_LENGTH_UNIFIED | red-tests | 5 | oracle/red_length_unified_tests.py |
RED_AREA_UNIFIED | red-tests | 4 | oracle/red_area_unified_tests.py |
RED_RELATE_UNIFIED | red-tests | 4 | oracle/red_relate_unified_tests.py |
RED_WINDING | red-tests | 0 | oracle/red_winding_tests.py |
Trust footprint & audit
Qed-closure is enforced corpus-wide by
scripts/check_admitted.sh; claim citations by
scripts/validate-claims.sh. Every Admitted is
registered as either a verified counterexample or a structured deferral.
| Item | Count | Source of record |
|---|---|---|
| Classical-reals axioms (theories/) | 3 | sig_not_dec · sig_forall_dec · functional_extensionality_dep |
| Flocq binary64 adds | 1 | Classical_Prop.classic |
| Admitted — verified counterexamples | 0 | docs/admitted-counterexamples.txt (provably-strongest) |
| Admitted — deferred (proof structured) | 0 | docs/admitted-deferred-proofs.txt |
| Hand-rolled interface-boundary kernels | 32 | docs/oracle-handrolled-allowlist.txt (frozen ratchet) |