Chip 2: peel two allowlist-clean files from audit-exceptions

TRIAGE_NTS_JTS_ISSUES.md

@@ -90,7 +90,7 @@ proven, soundness or coordinates open) · **⬜ planned** (not yet started) ·
 | **F-CP / F-MC / F-MS** | Structural `CurvePolygon` / `MultiCurve` / `MultiSurface` (preserve ring/member curves) | #64 · #509 | `CurveGeometry.v` (SQL/MM types, `CurveRing`, validity, chord bridge); `CurvePolygon{Valid,Simple,Orientation,Disjoint,Offset}.v`; oracle-backed exterior ring (`oracle/curve_polygon.py`, `CP_BOUNDARY_SIMPLIFY`) | 🟡 structural model + validity/simplicity witness-sound; true-region (Jordan) deferred |
 | **B-CP / B-MS** | Boundary of curve composites | #65 · #515 | oracle `CP_BOUNDARY_SIMPLIFY` (densify → extracted `greedy_simplify_perp_b64` → per-corner `b64_orient_sign_filtered`); `CurveBufferArea.v` boundary | 🟡 densified-boundary oracle exists (INTSAFE corners certified by `_sound_small_int`); composite-boundary point-set spec deferred |
 | **M-LEN-CS / M-LEN-CC** | Arc / compound-curve length (`r·θ`) | #64 · **#508** | `ArcLength.v`, `Atan2.v`, `AngleBetween.v`, `ArcRectifiable.v`, `CurveLength.v`; oracle `ARC_LENGTH_INVARIANTS_EXACT` / `ARC_SHORTER` | ✅ exact invariants; **`r·θ` meets the spec** (`ArcRectifiable.v : arc_r_theta_is_curve_length`); additivity is `CurveLength.v : curve_length_additive` (zoo wrap-up #566). Engine agreement remains differential; float length is interface-boundary |
-| **M-LEN-ZOO** | Exact metric length across the Zoo (Bible §4.2 `length()`; order: ellipse → cubic Bézier → clothoid → single-span NURBS, `rx=ry` bridge as ellipse rung 1) | **#508** | ADR-0004; CONTEXT.md (*Exact curves*: Zoo, Exact, Oracle-stable, Metric length); Bible amendment A1 (`bible/a1-cubic-bezier` in the jts fork); oracle `LENGTH_UNIFIED` (`C`/`A` today — `E`/`B` extension + `K`/`N` mint owed, ISO 13249-3 projections); wrap-up `docs/scout/508-closing-summary.md` | ✅ #566 / 508-h. **Unconditional:** CircularArc `r·θ` (`ArcRectifiable.v : arc_r_theta_is_curve_length`); additivity (`CurveLength.v : curve_length_additive`); reparam/reflect (`CurveLength.v : is_curve_length_reparam`, `CurveLength.v : is_curve_length_reflect`); golden NURBS quarter (`NurbsConicExact.v : nurbs2_golden_quarter_length`); equal-weight N ⊃ B (`NurbsQuadraticLength.v : nurbs2_equal_weights_cubic`, `NurbsGeneralLength.v : nurbs3_equal_weights_length`); Bézier polygon ceiling (`Bezier3Polygon.v : bezier3_length_le_polygon`); unit straight clothoid window (`ClothoidLength_unit.v : unit_line_discharges_window`); knot-list additivity (`NurbsKnotSpans.v : nurbs_spans_additive`) and glued two-quarter instance (`NurbsKnotSpans.v : golden_half_circle_length`). **Engine-conditional (no inhabitant):** elliptic E (`EllipseSpeedIntegral.v : ellipse_speed_integral_is_curve_length`). **Fresnel clothoid inhabitant:** `ClothoidFresnelInhab.v : fresnel_unit_window_length_inhab` (Stdlib RiemannInt; Category C; board #564). Pack layer remains `ClothoidFresnel.v : fresnel_is_curve_length`. **Out of scope:** Cox-de Boor; Exact* zoo types / CurveSegment growth (year-1 is CSChord or CSArc; QEX `ExactCurveEpic508.v : ticket_508_qed_or_qex` is not owner accept); Bible §2.6 densify ≤1.15×. This flip is not "the zoo is unconditionally exact." Owner review retires #508. |
+| **M-LEN-ZOO** | Exact metric length across the Zoo (Bible §4.2 `length()`; order: ellipse → cubic Bézier → clothoid → single-span NURBS, `rx=ry` bridge as ellipse rung 1) | **#508** | ADR-0004; CONTEXT.md (*Exact curves*: Zoo, Exact, Oracle-stable, Metric length); Bible amendment A1 (`bible/a1-cubic-bezier` in the jts fork); oracle `LENGTH_UNIFIED` (`C`/`A` today — `E`/`B` extension + `K`/`N` mint owed, ISO 13249-3 projections); wrap-up `docs/scout/508-closing-summary.md` | ✅ #566 / 508-h. **Unconditional:** CircularArc `r·θ` (`ArcRectifiable.v : arc_r_theta_is_curve_length`); additivity (`CurveLength.v : curve_length_additive`); reparam/reflect (`CurveLength.v : is_curve_length_reparam`, `CurveLength.v : is_curve_length_reflect`); golden NURBS quarter (`NurbsConicExact.v : nurbs2_golden_quarter_length`); equal-weight N ⊃ B (`NurbsQuadraticLength.v : nurbs2_equal_weights_cubic`, `NurbsGeneralLength.v : nurbs3_equal_weights_length`); Bézier polygon ceiling (`Bezier3Polygon.v : bezier3_length_le_polygon`); unit straight clothoid window (`ClothoidLength_unit.v : unit_line_discharges_window`); knot-list additivity (`NurbsKnotSpans.v : nurbs_spans_additive`) and glued two-quarter instance (`NurbsConicExact.v : golden_half_circle_length`). **Engine-conditional (no inhabitant):** elliptic E (`EllipseSpeedIntegral.v : ellipse_speed_integral_is_curve_length`). **Fresnel clothoid inhabitant:** `ClothoidFresnelInhab.v : fresnel_unit_window_length_inhab` (Stdlib RiemannInt; Category C; board #564). Pack layer remains `ClothoidFresnel.v : fresnel_is_curve_length`. **Out of scope:** Cox-de Boor; Exact* zoo types / CurveSegment growth (year-1 is CSChord or CSArc; QEX `ExactCurveEpic508.v : ticket_508_qed_or_qex` is not owner accept); Bible §2.6 densify ≤1.15×. This flip is not "the zoo is unconditionally exact." Owner review retires #508. |
 | **M-AREA-CP** | `CurvePolygon` area (Green's theorem + circular-segment correction) | #64 | `ArcArea.v` (`segment_area`); oracle `ARC_AREA_INVARIANTS_EXACT` / `ARC_AREA` / `RING_ORIENTATION` (signed area) | ✅ exact rational invariants; float area interface-boundary |
 | **M-DIM** | Dimension of curve geometries | TRIAGE park | — | ⬜ research park (no statement; `docs/scout/69-closing-summary.md`) |
 | **V-CP / V-CS** | Arc-aware validity (arc self-intersection, orientation via sector area, holes-in-shell) | #64 | `CurveRingSimple.v` (`curve_ring_not_simple_of_witness`), `CurvePolygonSimple.v`, `CurvePolygonValid.v`, `CurvePolygonOrientation.v`, `CurvePolygonDisjoint.v`, `InCircle_b64_exact.v`, **`CurveRingOffsetSimple.v`** (`curve_ring_simple_of_clearance`), **`WindingNumber.v`** (`winding_decides_membership`), **`CircularStringValid.v`** (`circularstring_abca_valid` — historical V-CS pin, JTS `2b56b1a4`); **`CircularStringOddCount.v`** (`circularstring_abca_postgis_invalid` — EX-CS-4, JTS `81c2e996`, PostGIS odd ≥ 3, closed-4 rejected); oracle `RING_SIMPLE` / `POINT_IN_CURVE_RING` / `RING_ORIENTATION` / `HOLES_DISJOINT` | 🟡 in-circle sign ✅ (full-plane, 3-ax) + per-ring witness-soundness ✅ + **control-count annulus pin ✅ (2026-08-23, even leftover first≠last invalid, odd ≥ 3 unchanged)**; **offset-ring simplicity now POSITIVELY certified under a clearance hypothesis (2026-06-30), and a Z-valued winding number decides point-in-ring (`Z.odd ∘ winding_number` ⟺ `point_in_ring`)**; completeness + unconditional true-region (Jordan / {-1,0,+1} winding) deferred |

_CoqProject.full

@@ -103,23 +103,24 @@ theories/NurbsQuadraticLength.v
 # golden quarter so later Weierstrass consumers do not copy them.
 # Category C (Stdlib atan / Ratan).  No golden content.
 theories/AtanDoubleAngle.v
+# #508-g / #565: knot-vector carrier + induction over spans.  3-axiom
+# (curve_length_additive).  Golden half-circle instance lives in
+# NurbsConicExact.v (Category C via 508-a atan).  Not a remint of
+# NurbsGeneralLength.nurbs_knot_span_additive.  Not Cox-de Boor.
+theories/NurbsKnotSpans.v
 # #508-a / #559: golden rational quarter circle has metric length π/2.
 # Weierstrass φ(t) = 2·atan(t/(√2+(1-√2)·t)); reparam + ext onto the
 # golden nurbs2_param.  Generic 2·atan lives in AtanDoubleAngle.v;
-# windowed ext lives in CurveLength.v.  Category C (Stdlib atan /
-# Ratan), same lineage as ArcParamBridge.v.  Does not grow
-# CurveSegment or remint ADR-0004.
+# windowed ext lives in CurveLength.v.  Two-golden-quarter half-circle
+# instance (π/2 + π/2 = π) is here so KnotSpans stays 3-axiom.
+# Category C (Stdlib atan / Ratan), same lineage as ArcParamBridge.v.
+# Does not grow CurveSegment or remint ADR-0004.
 theories/NurbsConicExact.v
 # #508 NURBS P1: general degree (equal-weight rational cubic ↔ polynomial
 # cubic), knot-span additivity (curve_length_additive), and the
 # conditional exact primitive through curve_length_of_primitive.
 # Single-span oracle N.  No ExactNurbsSegment.  3-axiom.
 theories/NurbsGeneralLength.v
-# #508-g / #565: knot-vector carrier + induction over spans, and the
-# two-golden-quarter half-circle instance (π/2 + π/2 = π).  Not a remint
-# of NurbsGeneralLength.nurbs_knot_span_additive.  Not Cox-de Boor.
-# Oracle N stays single-span.  Instance is Category C via 508-a atan.
-theories/NurbsKnotSpans.v
 # #508 arc P2 leftovers from #552: valid_arc ⇒ arc_sweep ≠ 0, and
 # arc_mid is a parameterized circumcircle point.  atan2 lane, 4-axiom
 # (docs/audit-exceptions.txt).  Does not start a new 64-a r·θ.
@@ -2698,17 +2699,9 @@ theories/ArcArcCirclesSpan.v
 # plus a same-sign combinator (no iff fed to nra).  4-axiom (atan2 lineage,
 # see docs/audit-exceptions.txt).  No Admitted.
 theories/ArcSpanAtan2.v
-# Issue #64 round-2 items ② and ④ (N-AA quartic certificate + atan2 discharge).
-# §1 Vieta coordinate identities for radical_point_plus/minus: x/y sum and
-# product formulas (ring proofs, no hypotheses) — the degree-2 polynomial
-# certificate certifying the radical-axis intersection is quadratic, not quartic.
-# §2 Four inCircle_R = 0 helpers (radical_points_on_circles +
-# inCircle_R_zero_of_equidistant) place each named point on each circumcircle.
-# §3 arc_arc_intersects_of_atan2_radical_span: headline promotion — atan2 span
-# membership for one radical point w.r.t. both arcs → arc_arc_intersects, via
-# arc_span_contains_atan2_iff_chord_sign + arc_arc_intersects_of_circles_and_radical_signs.
-# 4-axiom (atan2/Classic lineage via ArcSpanAtan2, docs/audit-exceptions.txt).
-# No Admitted.
+# Issue #64 round-2 item ④ — N-AA Vieta coordinate identities
+# (radical_point plus/minus x/y sum and product).  Pure ring, 3-axiom.
+# Item ② atan2 discharge lives in ArcSpanAtan2.v.
 theories/ArcArcQuartic.v
 # Issue #64 ask #5b / N-AA: coordinate certificate (3-axiom).
 # Affine circle–circle resultant (`circle_circle_res_x` / `_y`); constructor

docs/audit-exceptions.txt

@@ -10,13 +10,12 @@
 #     `docs/axiom-allowlist.txt` (verified, not hoped).
 #   - Adding a file requires a comment above it (Category C reason + plan).
 #
-# LIVE: 112 files (75 theories-flocq/ + 36 theories/ + 1 hunt probe).
-# None are allowlist-clean.  Flocq C1 (`Classical_Prop.classic` via
-# Bplus/Bminus/Bmult/Bdiv/round/B2R) cannot leave while Flocq's binary
-# model is in use (`docs/category-c-policy.md`).  R-side files carry
-# classic via atan2/Ratan or RiemannInt.  Five all-C2 arc files already
-# left (2026-08-25): ArcLength / ArcArea / ArcCentroid / ArcAreaCentroid
-# / CurveBufferArea.  Snapshot categorisation:
+# LIVE: 110 files (75 theories-flocq/ + 34 theories/ + 1 hunt probe).
+# Chip 2 peeled NurbsKnotSpans.v + ArcArcQuartic.v (atan/atan2 instances
+# moved into already-excepted siblings).  Remaining R-side files carry
+# classic via atan2/Ratan or RiemannInt.  Flocq C1 (`classic` via
+# Bplus/Bminus/Bmult/round) cannot leave while Flocq's binary model is
+# in use (`docs/category-c-policy.md`).  Snapshot:
 # docs/category-c-distribution.md (2026-08-16; list has grown since).
 #
 # Trio-only siblings deliberately NOT listed: Intersect_b64_exact_refs.v,
@@ -147,9 +146,7 @@ theories/ArcTraversalBridge.v
 theories/ArcMidSweep.v
 theories/AtanDoubleAngle.v
 theories/NurbsConicExact.v
-theories/NurbsKnotSpans.v
 theories/ArcSpanAtan2.v
-theories/ArcArcQuartic.v
 
 # R-side C1 — RiemannInt (#564 Fresnel inhabitant; pack stays 3-axiom)
 theories/ClothoidFresnelInhab.v

docs/scout/508-closing-summary.md

@@ -46,7 +46,7 @@ board #564). Year-1 `CurveSegment` is `CSChord` or `CSArc`. QEX
 | Single-span NURBS (golden) | unit quarter = `π/2` | `NurbsConicExact.v : nurbs2_golden_quarter_length` | Category C (`atan`) |
 | NURBS ⊃ Bézier | equal weights collapse the denominator | `NurbsQuadraticLength.v : nurbs2_equal_weights_cubic`, `NurbsGeneralLength.v : nurbs3_equal_weights_length` | unconditional inclusion |
 | NURBS knot list | span lengths sum | `NurbsKnotSpans.v : nurbs_spans_additive` | unconditional additivity; not Cox-de Boor |
-| NURBS two-quarter instance | `π/2 + π/2 = π` | `NurbsKnotSpans.v : golden_half_circle_length` | two glued 508-a quarters; not a new `π` theorem |
+| NURBS two-quarter instance | `π/2 + π/2 = π` | `NurbsConicExact.v : golden_half_circle_length` | two glued 508-a quarters; not a new `π` theorem |
 
 Speed-integral pack (the method, not a zoo member):
 `SpeedIntegral.v : speed_integral_is_curve_length`. Bernstein plumbing: