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

Host-lane Print Assumptions on all 35 R-side listed files showed 0/35
already allowlist-clean. NurbsKnotSpans and ArcArcQuartic leave after
moving their atan/atan2 instances into already-excepted siblings
(NurbsConicExact, ArcSpanAtan2). Remaining 108 stay C1 (Flocq binary
ops or atan2/Ratan/RiemannInt). Allowlist unchanged.

This PR was drafted with AI assistance.

Co-authored-by: Jeroen Bloemscheer <grootstebozewolf@users.noreply.github.com>

Author: cursoragent

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/508-pstar-rungs.md

@@ -14,7 +14,7 @@ types, ADR-0004 remint) are untouched.  Year-1 engine stays circular-only.
 | P1 | clothoid | `theories/ClothoidLength_unit.v` | `unit_line_discharges_window` — unit-speed straight inhabits the [sd,ed] contract; Euler-spiral integrals stay Route-1 primitives | Qed + Technique park, 3-axiom |
 | P1 | clothoid | `theories/ClothoidFresnel.v` + `ClothoidFresnelInhab.v` | pack `fresnel_is_curve_length` (3-axiom conditional); inhabitant `fresnel_unit_window_length_inhab` via Stdlib RiemannInt of (cos,sin)(t²/2) — `[0,1]` length 1 | Qed + inhabitant, Category C (#564 / 508-e) |
 | P1 | nurbs | `theories/NurbsGeneralLength.v` | equal-weight rational cubic ↔ cubic; two-window `nurbs_knot_span_additive`; conditional primitive | Qed, 3-axiom |
-| P1 | nurbs | `theories/NurbsKnotSpans.v` | `nurbs_spans_additive` — knot-vector induction; instance `golden_half_circle_length` (two 508-a quarters) | Qed, 3-axiom additivity / Category C instance (#565 / 508-g) |
+| P1 | nurbs | `theories/NurbsKnotSpans.v` | `nurbs_spans_additive` — knot-vector induction (3-axiom). Instance `NurbsConicExact.v : golden_half_circle_length` (two 508-a quarters, Category C) | Qed, 3-axiom additivity / Category C instance (#565 / 508-g) |
 | P2 | arc | `theories/ArcMidSweep.v` | `valid_arc_sweep_nonzero`; `arc_mid_on_circle_param` | Qed, Category C (atan2; removal tracks AngleBetween) |
 | — | framework | `theories/BernsteinBasis.v` | `bern_partition`; `bern_elevate_2` (n=2 instance of `elevate_ctrl`); `bezier3_elevation_pointwise` re-proved through it | Qed, 3-axiom (#562 / 508-f) |
 | — | stop | `theories/ExactCurveEpic508.v` | `ticket_508_qed_or_qex` — zoo-on-CurveSegment (QED) or missing constructor (QEX); discharged QEX on the ellipse | Qed, 3-axiom (508-qed-qex) |
@@ -85,7 +85,7 @@ Wrap-up is #566.
 `curve_length_additive`.  It does not remint
 `NurbsGeneralLength.nurbs_knot_span_additive` (two-window special
 case).  Not Cox-de Boor.  Oracle `N` stays single-span.  Instance
-`golden_half_circle_length` glues two 508-a golden quarters
+`NurbsConicExact.v : golden_half_circle_length` glues two 508-a golden quarters
 (`π/2 + π/2 = π`); Category C through `atan` only.  Does not
 retire epic 508.  Wrap-up is #566.  Board #564 inhabitant landed.
 
@@ -105,7 +105,7 @@ Wrap-up letter. TRIAGE `M-LEN-ZOO` flips to ✅ with honest scope
 notes. Bible §4.2 satisfaction is
 [`docs/scout/508-closing-summary.md`](scout/508-closing-summary.md).
 Does not remint `NurbsKnotSpans.v : nurbs_spans_additive` or
-`NurbsKnotSpans.v : golden_half_circle_length`. Does not remint
+`NurbsConicExact.v : golden_half_circle_length`. Does not remint
 `SpeedIntegral.v` / `ClothoidLength_unit.v` / `ClothoidFresnel.v`.
 Fresnel inhabitant is a later #564 letter (`ClothoidFresnelInhab.v`).
 QEX is not owner accept. This letter does

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: 110 files (74 theories-flocq/ + 35 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: 108 files (74 theories-flocq/ + 33 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,
@@ -142,9 +141,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/category-c-distribution.md

@@ -33,6 +33,14 @@ remains the 2026-08-16 snapshot.
 missing from `audit-exceptions.txt` and is now listed (85 files / 74
 `theories-flocq/`). Three PA footers are C1 via `Bminus`/`Bmult` in
 the Ozaki DAG. The TSV still does not include this file.
+**Update 2026-09-11**: Chip 2 peeled `NurbsKnotSpans.v` and
+`ArcArcQuartic.v` off `audit-exceptions.txt` after a host-lane PA
+measurement of all 35 R-side listed files (0 already allowlist-clean).
+The atan half-circle instance moved to `NurbsConicExact.v`; the atan2
+N-AA headline moved to `ArcSpanAtan2.v`. Remaining list: 108 files /
+74 `theories-flocq/` / 33 `theories/` / 1 hunt probe. No Flocq C1 file
+can leave while Flocq's binary model is in use. The TSV remains the
+2026-08-16 snapshot.
 **Update 2026-08-27**: Four HotPixel comparison lemmas
 (`b64_le_R_of_true`, `b64_le_complete`, `b64_lt_R_of_true`,
 `b64_lt_complete`) left `classic` after a payload split on finite

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: