diff --git a/TRIAGE_NTS_JTS_ISSUES.md b/TRIAGE_NTS_JTS_ISSUES.md index 8822acb9..3659ce76 100644 --- a/TRIAGE_NTS_JTS_ISSUES.md +++ b/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 | diff --git a/_CoqProject.full b/_CoqProject.full index 23f5bef2..6cf3ac27 100644 --- a/_CoqProject.full +++ b/_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 diff --git a/docs/audit-exceptions.txt b/docs/audit-exceptions.txt index 0312e07d..4452bfa3 100644 --- a/docs/audit-exceptions.txt +++ b/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 diff --git a/docs/scout/508-closing-summary.md b/docs/scout/508-closing-summary.md index 5d2844ea..f8bb7f91 100644 --- a/docs/scout/508-closing-summary.md +++ b/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: diff --git a/docs/verified-claims.md b/docs/verified-claims.md index 0ab648e0..f567106d 100644 --- a/docs/verified-claims.md +++ b/docs/verified-claims.md @@ -450,7 +450,7 @@ vacuous. See [`docs/jct-vacuity-finding.md`](jct-vacuity-finding.md) and | `ArcArcCircles.v : arc_arc_circles_intersect` (+ `two_circles_radical_point`, `inCircle_R_concyclic`, `inCircle_R_zero_of_equidistant`) | **Arc-arc circles intersect (issue #64 #5b / N-AA), Stage B — the radical-line/sqrt frontier deferred by `ArcArcSound`:** unconditional both-circles existence for properly-intersecting circumcircles. `two_circles_radical_point`: for `\|r1−r2\| < dist O1 O2 < r1+r2` (both radii > 0), the `ARC_ARC_XY` radical-line formula `a=(d²+r1²−r2²)/2d`, `h=√(r1²−a²)`, `P± = O1+a·u ± h·perp(u)` constructs an explicit point with `dist_sq O1 P = r1²` ∧ `dist_sq O2 P = r2²` — discriminant positivity `r1²−a² > 0` from the four-factor identity `(d+r1+r2)(d+r1−r2)(r2+d−r1)(r1+r2−d) = (2dr1)²−(d²+r1²−r2²)²`. `inCircle_R_concyclic`: four points equidistant from a common centre ⇒ Shewchuk determinant `= 0` (proved by translating the centre to the origin via `inCircle_R_translation_invariant`, then `nsatz`). Composed via `arc_center_equidistant`: proper circle intersection ⇒ ∃X on both arcs' circumcircles (`inCircle_R = 0`). Pure real algebra, **3-axiom** (no atan2/sin/Classic, no exemption). Deferred: `arc_span_contains` for these points (angular sector ⇒ atan2), full `arc_arc_intersects` (circles ∧ both spans), b64, sweep≥π `[exact]` | 3 | | `CurveRingSimple.v : curve_ring_not_simple_of_witness` (+ `arc_arc_circle_meet_of_span`, `adjacent_arcs_meet_at_vertex`, `curve_ring_simple`) | **Simple curve rings (issue #64 / JTS #1195 §7 / V-CP), proof companion of the `RING_SIMPLE` oracle mode** — NODE-based ring-edge simplicity, the CurvePolygon shell/hole building block (the OGC point-based `Curve.isSimple` / V-CS is covered separately via the densified `IsSimpleOp` cross-check): adds the simplicity layer on `valid_curve_ring`. `on_curve_segment`/`curve_segments_meet` membership (chord = `between`; arc = on circumcircle ∧ `arc_span_contains`); `curve_ring_simple` = no two NON-adjacent ring positions' segments meet (consecutive/closing pairs may share their connecting vertex). `curve_ring_not_simple_of_witness`: a shared point of two non-adjacent segments refutes `curve_ring_simple` — **certifies every `NOT_SIMPLE` verdict** the oracle reports from a detected crossing. `arc_arc_circle_meet_of_span` ties the merged `ArcArcCircles.arc_arc_circles_intersect` into a self-intersection witness (span bridge as honest hypothesis); `adjacent_arcs_meet_at_vertex` records the permitted shared-vertex meeting. **3-axiom** (no atan2/sin/Classic). Deferred (unconditional span membership resolved below; still open: the completeness direction — SIMPLE ⇒ no crossing = oracle all-pairs computation — and holes-in-shell/disjoint for full V-CP) `[exact]` | 3 | | `CircleCircleResultant.v : radical_points_satisfy_circle_circle_res` (+ `circle_circle_res_vanishes_on_common_zeros`, `circle_circle_res_y_vanishes_on_common_zeros`, `circle_circle_res_{x,y}`, `locked_fixture_res_x`, `locked_fixture_res_y_{plus,minus}`, `locked_fixture_res_on_radical_points`, `circles_properly_intersect`, `coincident_centres_not_proper`) | **N-AA circle–circle resultant identity (issue #64 #5b / `64-naa-res`):** constructor ⇒ resultant root — under `circles_properly_intersect`, `radical_point_plus` / `_minus` coordinates are roots of the affine resultants. Not the converse (resultant vanishing does not identify these radical coordinates), and not a formal degree / Bézout / homogenisation proof. Landscaping coordinate certificate on the existing radical-axis constructor — names coordinates a later cook would write if it existed; does not implement 𝓘, mint hens, or execute ADR-0007. `circle_circle_res_x` / `_y` are the affine Sylvester resultants of the two circle equations. Hypothesis-free supporting lemmas: any common zero is a root of both resultants. Locked-fixture witnesses: `res_x` at `7/2`, `res_y` at `±√(51/4)`, and both resultants on the named radical points. QEX (not the headline): circular γ : [0,1]→S and (ti, tj) are not constructed; spans not minted. `coincident_centres_not_proper` is the Year-1 guard lemma (dist = 0), unused by the headline. **3-axiom** (no atan2/Classic; does not Require `ArcArcQuartic` / `SheetHenCook`) `[exact]` | 3 | -| `ArcArcQuartic.v : arc_arc_intersects_of_atan2_radical_span` (+ `radical_point_x_sum`, `radical_point_y_sum`, `radical_point_x_prod`, `radical_point_y_prod`) | **N-AA quartic certificate + atan2 discharge (issue #64 round-2 items ② and ④):** §1 Vieta coordinate identities — `radical_point_x_sum`/`y_sum` (sum of radical-point x/y coords = `2·(Oi + a·ui)`) and `radical_point_x_prod`/`y_prod` (product = difference of squares `(Oi+a·ui)² − (h·uj)²`) certified by pure `ring` after unfolding point constructors; no geometric hypotheses. These are the Vieta formulas for the degree-2 polynomial whose roots are the radical-line intersection coordinates — the algebraic certificate that reduces the "quartic" circle-circle system to a quadratic after the radical-axis substitution. §2 Four `inCircle_R = 0` helpers (one per {plus, minus} × {a1, a2}) using `radical_points_on_circles` + `inCircle_R_zero_of_equidistant` to place each radical point on each circumcircle. §3 `arc_arc_intersects_of_atan2_radical_span`: atan2 sector membership for one radical point w.r.t. both arcs → `arc_arc_intersects`, via the §2 iff lemmas converting to chord-sign form + `ArcArcCirclesSpan.arc_arc_intersects_of_circles_and_radical_signs`. **4-axiom** (atan2/`Classical_Prop.classic` lineage via `ArcSpanAtan2`, `docs/audit-exceptions.txt`); the Vieta and `inCircle_R` helpers stay 3-axiom `[exact]` | 4 | +| `ArcSpanAtan2.v : arc_arc_intersects_of_atan2_radical_span` (+ `radical_point_x_sum`, `radical_point_y_sum`, `radical_point_x_prod`, `radical_point_y_prod`) | **N-AA quartic certificate + atan2 discharge (issue #64 round-2 items ② and ④):** §1 Vieta coordinate identities — `radical_point_x_sum`/`y_sum` (sum of radical-point x/y coords = `2·(Oi + a·ui)`) and `radical_point_x_prod`/`y_prod` (product = difference of squares `(Oi+a·ui)² − (h·uj)²`) certified by pure `ring` after unfolding point constructors; no geometric hypotheses. These are the Vieta formulas for the degree-2 polynomial whose roots are the radical-line intersection coordinates — the algebraic certificate that reduces the "quartic" circle-circle system to a quadratic after the radical-axis substitution. §2 Four `inCircle_R = 0` helpers (one per {plus, minus} × {a1, a2}) using `radical_points_on_circles` + `inCircle_R_zero_of_equidistant` to place each radical point on each circumcircle. §3 `arc_arc_intersects_of_atan2_radical_span`: atan2 sector membership for one radical point w.r.t. both arcs → `arc_arc_intersects`, via the §2 iff lemmas converting to chord-sign form + `ArcArcCirclesSpan.arc_arc_intersects_of_circles_and_radical_signs`. **4-axiom** (atan2/`Classical_Prop.classic` lineage via `ArcSpanAtan2`, `docs/audit-exceptions.txt`); the Vieta and `inCircle_R` helpers stay 3-axiom `[exact]` | 4 | | `ArcSpanAtan2.v : arc_span_contains_atan2_iff_chord_sign` (+ `cross_on_circle_value`, `sin_sum_to_product`, `two_circles_radical_point_unique`, `arc_arc_intersects_of_circles_and_radical_signs`) | **Arc-span atan2 sector membership = chord-sign membership (issue #64), resolving the "sweep≥π" gap named above:** `arc_span_contains_atan2` is a new atan2-based angular sector test (built on `Atan2.atan2` / `AngleBetween.angle_between`, mirroring `arc_interior_side`'s sign-product shape). The headline proves it **unconditionally** equivalent to the existing chord cross-product test `ArcIntersect.arc_span_contains` for any on-circumcircle point — including reflex arcs (sweep ≥ π), which the chord-sign test was previously (incorrectly) documented as not handling. Proof: `cross_on_circle_value` gives a closed form `cross_R_pt A C P = r²·(sin γ + sin(θ−γ) − sin θ)` for three points on a common circle (via `cross_R_pt_cyclic_sum`, a pure `ring` identity in `ArcOrient.v`, plus the 2-D Lagrange identity `cross_dot_lagrange_2d`); `sin_sum_to_product` rewrites this as `4·sin(γ/2)·sin(θ/2)·sin((θ−γ)/2)` (`nsatz` on double-angle expansions); a `same_sign` combinator (stable under multiplication) matches this sine product's sign to the atan2 test's `θ(θ−γ)·θ_M(θ_M−γ)` sign-product, for every sweep, with no wraparound case split. Also lands `two_circles_radical_point_unique` (any point on both of two properly-intersecting circles equals one of `ArcArcCircles.two_circles_radical_point`'s two named coordinates, 3-axiom) and `arc_arc_intersects_of_circles_and_radical_signs` (replaces `ArcArcCirclesSpan`'s opaque universally-quantified span bridge with a concrete, per-instance-checkable condition on those two named points — still a named hypothesis, since two properly-intersecting circles can host arcs whose spans miss the crossing entirely, so no hypothesis-free version can exist). **4-axiom** (atan2/`Classical_Prop.classic` lineage, `docs/audit-exceptions.txt`); the two circle lemmas stay 3-axiom `[exact]` | 4 | | `CurvePolygonSimple.v : curve_polygon_outer_not_simple_of_witness` (+ `curve_polygon_hole_not_simple_of_witness`, `simple_curve_polygon`, `simple_curve_polygon_{outer,hole}_simple`) | **CurvePolygon ring-simplicity (issue #64 / JTS #1195 §7 / V-CP), first slice:** lifts `CurveRingSimple.curve_ring_simple` over a CurvePolygon's shell + hole rings. `simple_curve_ring` = structurally valid ∧ `curve_ring_simple`; `simple_curve_polygon` = the outer ring and every hole (`Forall`) is `simple_curve_ring`. Projections (`simple_curve_polygon_{outer,hole}_simple`): a simple polygon's every ring is `curve_ring_simple` — the bridge by which the oracle certifies a CurvePolygon by running `RING_SIMPLE` per ring. Soundness (`curve_polygon_{outer,hole}_not_simple_of_witness`): a non-adjacent crossing witness in the outer ring or any hole refutes `simple_curve_polygon` (composes `curve_ring_not_simple_of_witness`). No new oracle (reuses `RING_SIMPLE`). **3-axiom** (no atan2/sin/Classic). Deferred to `CP_VALID`: sector orientation, holes-inside-shell, holes mutually disjoint `[exact]` | 3 | | `CurvePolygonValid.v : valid_curve_polygon_cp_hole_witness` (+ `point_in_inscribed_ring`, `curve_polygon_holes_inside_shell`, `valid_curve_polygon_cp`, `valid_curve_polygon_cp_simple`) | **CurvePolygon holes-inside-shell (issue #64 / JTS #1195 §7 / V-CP / CP_VALID), second slice:** the `POINT_IN_CURVE_RING` oracle decides point-in-TRUE-curved-region by ARC-AWARE ray casting (ray ∩ arcs via circle∩horizontal-line in-sweep + chords) — INTERFACE-BOUNDARY float (sqrt + atan2 sweep, allowlisted as `run_arc_offset_xy`'s neighbour), Jordan soundness deferred and pinned by the adversarial test (oracle vs independent closed-form half-disk/disk membership). This Coq file proves the **sound conservative FLOOR**: the INSCRIBED chord-polygon containment via the merged `CurveGeometry.chord_approx_ring` (the exact rational control polygon, an under-approximation that omits the arc bulges) and Phase-3 `Overlay.point_in_ring` / `hole_inside_outer`. `point_in_inscribed_ring p r n := point_in_ring p (chord_approx_ring r n)` (`inscribed-IN ⇒ truly-IN`); `valid_curve_polygon_cp := simple_curve_polygon ∧ curve_polygon_holes_inside_shell` (composes the ring-simplicity slice); `valid_curve_polygon_cp_hole_witness`: each hole has a vertex inside the inscribed outer ring. **3-axiom** (no atan2/sin/Classic). Deferred: true-region Jordan soundness, n-chord densification, sector orientation, holes mutually disjoint `[exact]` | 3 | @@ -2003,19 +2003,19 @@ Instance: two golden quadratic spans glued at `(0,1)` on knots `[0; 1; 2]`. Span 0 is `NurbsConicExact.v : nurbs2_golden_quarter_length`. Span 1 is the rotate-90 image (isometry of polyline lengths). The piecewise `golden_half` agrees with each span on its window (glue at -the knot). `NurbsKnotSpans.v : golden_half_circle_length` is +the knot). `NurbsConicExact.v : golden_half_circle_length` is `π/2 + π/2 = π` — two 508-a quarters, not a new `π` theorem. Category C (`atan`) through 508-a only; `nurbs_spans_additive` stays 3-axiom. Does not retire epic 508 (that is #566). Does not steal 508-e / 508-h. Fresnel inhabitant is a separate #564 letter. Does not flip TRIAGE M-LEN-ZOO. -**NTS RGR Board catalog (#508 children).** `508-g` = #565 / multi-span NURBS knot-vector additivity (witness `508-g-nurbs-spans`). Headline `NurbsKnotSpans.v : nurbs_spans_additive`. Instance `NurbsKnotSpans.v : golden_half_circle_length`. Board pointer stays #565. `508-a` = #559, `508-b` = #560, `508-c` = #561, `508-d` = #563, `508-e` = #564 (Fresnel pack + inhabitant), and `508-f` = #562 are on `main`. Remaining child is `508-h` only. +**NTS RGR Board catalog (#508 children).** `508-g` = #565 / multi-span NURBS knot-vector additivity (witness `508-g-nurbs-spans`). Headline `NurbsKnotSpans.v : nurbs_spans_additive`. Instance `NurbsConicExact.v : golden_half_circle_length`. Board pointer stays #565. `508-a` = #559, `508-b` = #560, `508-c` = #561, `508-d` = #563, `508-e` = #564 (Fresnel pack + inhabitant), and `508-f` = #562 are on `main`. Remaining child is `508-h` only. | `file : theorem` | Meaning | Ax | |---|---|---| | `NurbsKnotSpans.v : nurbs_spans_additive` (+ `knot_vector`, `span_lengths`, `list_sum`) | **Knot-vector span additivity (#508/#565, claimId: 508-g, witness: 508-g-nurbs-spans):** a weakly increasing knot chain with one `is_curve_length` per consecutive window has total metric length the sum of the span lengths — induction on interior knots over `curve_length_additive`. Not a remint of `nurbs_knot_span_additive`. Not Cox-de Boor. Oracle `N` stays single-span. Does not retire epic 508 `[exact]` | 3 | -| `NurbsKnotSpans.v : golden_half_circle_length` (+ `golden_q2_length`, `golden_half_span0`, `golden_half_span1`, `golden_half_glue`) | **Two golden quarters:** first-quadrant + rotate-90 second-quadrant NURBS on `[0,2]` have metric length `π`. Glue at `(0,1)`. Category C through 508-a `atan`. Not a new `π` theorem `[exact]` | 4 | +| `NurbsConicExact.v : golden_half_circle_length` (+ `golden_q2_length`, `golden_half_span0`, `golden_half_span1`, `golden_half_glue`) | **Two golden quarters:** first-quadrant + rotate-90 second-quadrant NURBS on `[0,2]` have metric length `π`. Glue at `(0,1)`. Category C through 508-a `atan`. Not a new `π` theorem `[exact]` | 4 | ## Issue #508 — wrap-up: M-LEN-ZOO + Bible §4.2 satisfaction (`508-h`) diff --git a/theories/ArcArcQuartic.v b/theories/ArcArcQuartic.v index d35e9cc2..a774962e 100644 --- a/theories/ArcArcQuartic.v +++ b/theories/ArcArcQuartic.v @@ -1,61 +1,37 @@ (* ============================================================================ NetTopologySuite.Proofs.ArcArcQuartic ---------------------------------------------------------------------------- - Issue #64 round-2 open items ② and ④ (N-AA quartic coordinate identity and - atan2 sector-membership discharge). + Issue #64 round-2 item ④ — N-AA quartic coordinate identity (Vieta). - The corpus already has: - · `ArcArcCircles.radical_points_on_circles` — both named radical-line - points lie on both circumcircles (`dist_sq Oi rp± = ri²`). - · `ArcArcCirclesSpan.arc_arc_intersects_of_circles_and_radical_signs` — - promotes proper-circle-intersection to `arc_arc_intersects` when the - chord-sign span predicate holds at one of the two named points. - · `ArcSpanAtan2.arc_span_contains_atan2_iff_chord_sign` — for a valid arc - and any on-circumcircle point, the atan2 sector test is equivalent to - the chord-sign test, unconditionally (every sweep, including reflex arcs). + The two radical-line intersection candidate coordinates satisfy: + px rp+ + px rp- = 2·(px O1 + a·ux) (x Vieta sum) + py rp+ + py rp- = 2·(py O1 + a·uy) (y Vieta sum) + px rp+ · px rp- = (px O1+a·ux)² − (h·uy)² (x Vieta product) + py rp+ · py rp- = (py O1+a·uy)² − (h·ux)² (y Vieta product) + These are the Vieta formulas for the degree-2 polynomial whose roots + are the radical-line intersection x- (resp. y-) coordinates — the + polynomial certificate that makes the "quartic" circle-circle system + reducible to a quadratic after the radical-axis substitution. Pure + `ring` proofs; no geometric hypotheses. 3-axiom. - This file closes the two remaining gaps: + Item ② (atan2 sector-membership discharge) and the headline + `arc_arc_intersects_of_atan2_radical_span` live in ArcSpanAtan2.v + (Category C via atan2). This file does not Require that lane. - §1 Vieta coordinate identities (item ④ — the quartic certificate). - The two intersection candidate coordinates satisfy: - px rp+ + px rp- = 2·(px O1 + a·ux) (x Vieta sum) - py rp+ + py rp- = 2·(py O1 + a·uy) (y Vieta sum) - px rp+ · px rp- = (px O1+a·ux)² − (h·uy)² (x Vieta product) - py rp+ · py rp- = (py O1+a·uy)² − (h·ux)² (y Vieta product) - These are the Vieta formulas for the degree-2 polynomial whose roots - are the radical-line intersection x- (resp. y-) coordinates — the - polynomial certificate that makes the "quartic" system reducible to a - quadratic after the radical-axis substitution. Pure `ring` proofs; no - geometric hypotheses. - - §2 Span atan2 ↔ chord-sign for the explicit radical points (item ②). - Four helper lemmas confirm each radical point lies on the correct - circumcircle (`inCircle_R = 0`), enabling the iff bridge. Each helper - uses `radical_points_on_circles` + `inCircle_R_zero_of_equidistant`. - - §3 atan2-driven promotion to `arc_arc_intersects` (headline). - `arc_arc_intersects_of_atan2_radical_span` — if the atan2 sector test - holds for one of the two named radical points w.r.t. both arcs, then - `arc_arc_intersects a1 a2` follows by converting via the §2 iff lemmas - and applying `arc_arc_intersects_of_circles_and_radical_signs`. - - Proved here (4-AXIOM: inherits `Classical_Prop.classic` transitively via - `ArcSpanAtan2`/`Atan2`/`AngleBetween` — same lineage and exemption as - `ArcSpanAtan2.v`, see `docs/audit-exceptions.txt`). No `Admitted`, no - `Axiom`, no `Parameter`. + No `Admitted`, no `Axiom`, no `Parameter`. Author: NetTopologySuite.Proofs contributors License: BSD-3-Clause (see LICENSE) AI assistance disclosure: AI-drafted, human-reviewed. + Assisted-by: Cursor Grok 4.6 ========================================================================== *) -From Stdlib Require Import Reals Lra. -From NTS.Proofs Require Import Distance CurveGeometry ArcOrient ArcIntersect - ArcChordApprox ArcOffsetThreePoint ArcArcCircles ArcArcCirclesSpan ArcSpanAtan2. +From Stdlib Require Import Reals. +From NTS.Proofs Require Import Distance CurveGeometry ArcArcCircles. Local Open Scope R_scope. (* -------------------------------------------------------------------------- *) -(* §1 Vieta coordinate identities (the quartic certificate). *) +(* Vieta coordinate identities (the quartic certificate). *) (* -------------------------------------------------------------------------- *) (* Sum of x-coordinates of the two radical-line intersection candidates. @@ -109,254 +85,7 @@ Proof. unfold radical_point_plus, radical_point_minus. cbn [py]. ring. Qed. -(* -------------------------------------------------------------------------- *) -(* §2 Each radical point lies on each circumcircle (inCircle_R = 0). *) -(* *) -(* Helper lemmas: four combinations of {plus, minus} × {a1, a2}. *) -(* Proof chain (identical structure for each): *) -(* 1. radical_points_on_circles → dist_sq Oi rp± = ri² *) -(* 2. arc_radius_eq_sqrt + sqrt_sqrt + arc_radius_sq → ri² = dist_sq Oi S *) -(* 3. inCircle_R_zero_of_equidistant closes the goal. *) -(* -------------------------------------------------------------------------- *) - -Lemma radical_plus_on_circle_a1 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - inCircle_R (arc_start a1) (arc_mid a1) (arc_end a1) - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) = 0. -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - destruct (radical_points_on_circles - (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) - (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) - Hdpos Hrabs Hdlt) - as [[HdP1 _] _]. - apply inCircle_R_zero_of_equidistant; [exact Hva1 |]. - assert (Hr1sq : arc_radius a1 * arc_radius a1 - = dist_sq (arc_center a1) (arc_start a1)). - { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. - unfold arc_radius_sq. reflexivity. } - lra. -Qed. - -Lemma radical_plus_on_circle_a2 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - inCircle_R (arc_start a2) (arc_mid a2) (arc_end a2) - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) = 0. -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - destruct (radical_points_on_circles - (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) - (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) - Hdpos Hrabs Hdlt) - as [[_ HdP2] _]. - apply inCircle_R_zero_of_equidistant; [exact Hva2 |]. - assert (Hr2sq : arc_radius a2 * arc_radius a2 - = dist_sq (arc_center a2) (arc_start a2)). - { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. - unfold arc_radius_sq. reflexivity. } - lra. -Qed. - -Lemma radical_minus_on_circle_a1 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - inCircle_R (arc_start a1) (arc_mid a1) (arc_end a1) - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) = 0. -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - destruct (radical_points_on_circles - (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) - (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) - Hdpos Hrabs Hdlt) - as [_ [HdM1 _]]. - apply inCircle_R_zero_of_equidistant; [exact Hva1 |]. - assert (Hr1sq : arc_radius a1 * arc_radius a1 - = dist_sq (arc_center a1) (arc_start a1)). - { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. - unfold arc_radius_sq. reflexivity. } - lra. -Qed. - -Lemma radical_minus_on_circle_a2 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - inCircle_R (arc_start a2) (arc_mid a2) (arc_end a2) - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) = 0. -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - destruct (radical_points_on_circles - (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) - (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) - Hdpos Hrabs Hdlt) - as [_ [_ HdM2]]. - apply inCircle_R_zero_of_equidistant; [exact Hva2 |]. - assert (Hr2sq : arc_radius a2 * arc_radius a2 - = dist_sq (arc_center a2) (arc_start a2)). - { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. - unfold arc_radius_sq. reflexivity. } - lra. -Qed. - -(* -------------------------------------------------------------------------- *) -(* §2b atan2 span ↔ chord-sign span iff for each radical point / arc pair. *) -(* -------------------------------------------------------------------------- *) - -Lemma radical_plus_span_iff_a1 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - (arc_span_contains_atan2 a1 - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) - <-> - arc_span_contains a1 - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2))). -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - apply arc_span_contains_atan2_iff_chord_sign; [exact Hva1 |]. - exact (radical_plus_on_circle_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). -Qed. - -Lemma radical_plus_span_iff_a2 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - (arc_span_contains_atan2 a2 - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) - <-> - arc_span_contains a2 - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2))). -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - apply arc_span_contains_atan2_iff_chord_sign; [exact Hva2 |]. - exact (radical_plus_on_circle_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). -Qed. - -Lemma radical_minus_span_iff_a1 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - (arc_span_contains_atan2 a1 - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) - <-> - arc_span_contains a1 - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2))). -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - apply arc_span_contains_atan2_iff_chord_sign; [exact Hva1 |]. - exact (radical_minus_on_circle_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). -Qed. - -Lemma radical_minus_span_iff_a2 : - forall a1 a2 : CircularArc, - valid_arc a1 -> valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - (arc_span_contains_atan2 a2 - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) - <-> - arc_span_contains a2 - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2))). -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. - apply arc_span_contains_atan2_iff_chord_sign; [exact Hva2 |]. - exact (radical_minus_on_circle_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). -Qed. - -(* -------------------------------------------------------------------------- *) -(* §3 atan2-driven promotion to `arc_arc_intersects` (the N-AA headline). *) -(* *) -(* Converts the atan2 span hypothesis to chord-sign form via the §2 iff *) -(* lemmas, then applies the already-Qed promotion theorem from *) -(* `ArcArcCirclesSpan`. No new geometric content; the circle-intersection *) -(* hypotheses are passed through unchanged. *) -(* *) -(* Why the disjunction is the right hypothesis shape: `arc_arc_intersects` *) -(* is an existential -- it needs ONE point on both circumcircles AND in both *) -(* spans. `two_circles_radical_point_unique` (ArcArcCircles §5) guarantees *) -(* every point on both circles equals `radical_point_plus` or `_minus`. So *) -(* the question reduces to: does `plus` lie in both spans, or does `minus`? *) -(* Checking the two arcs against the SAME root is therefore the minimal *) -(* sufficient condition -- a mixed hypothesis (plus for a1, minus for a2) *) -(* would not witness a single shared point. *) -(* -------------------------------------------------------------------------- *) - -Theorem arc_arc_intersects_of_atan2_radical_span : - forall a1 a2 : CircularArc, - valid_arc a1 -> - valid_arc a2 -> - 0 < dist (arc_center a1) (arc_center a2) -> - Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> - dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> - ((arc_span_contains_atan2 a1 - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) /\ - arc_span_contains_atan2 a2 - (radical_point_plus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2))) - \/ - (arc_span_contains_atan2 a1 - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)) /\ - arc_span_contains_atan2 a2 - (radical_point_minus (arc_center a1) (arc_center a2) - (arc_radius a1) (arc_radius a2)))) -> - arc_arc_intersects a1 a2. -Proof. - intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt Hatan2. - apply (arc_arc_intersects_of_circles_and_radical_signs - a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). - destruct Hatan2 as [[H1 H2] | [H1 H2]]. - - left. split. - + apply (radical_plus_span_iff_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). - exact H1. - + apply (radical_plus_span_iff_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). - exact H2. - - right. split. - + apply (radical_minus_span_iff_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). - exact H1. - + apply (radical_minus_span_iff_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). - exact H2. -Qed. - -(* -------------------------------------------------------------------------- *) -(* §4 Audit footprint. *) -(* -------------------------------------------------------------------------- *) - Print Assumptions radical_point_x_sum. Print Assumptions radical_point_y_sum. Print Assumptions radical_point_x_prod. Print Assumptions radical_point_y_prod. -Print Assumptions arc_arc_intersects_of_atan2_radical_span. diff --git a/theories/ArcSpanAtan2.v b/theories/ArcSpanAtan2.v index 833864f3..f5b4a8b0 100644 --- a/theories/ArcSpanAtan2.v +++ b/theories/ArcSpanAtan2.v @@ -55,6 +55,11 @@ side hypothesis) -- covering the reflex case the corpus previously believed open. + Item ② / N-AA atan2 discharge (moved from ArcArcQuartic so that file + can leave the exceptions list as 3-axiom Vieta): + `arc_arc_intersects_of_atan2_radical_span` plus the four + radical-point on-circle / atan2-iff helpers. + Author: NetTopologySuite.Proofs contributors License: BSD-3-Clause (see LICENSE) AI assistance disclosure: AI-drafted, human-reviewed. @@ -62,7 +67,8 @@ From Stdlib Require Import Reals Lra Nsatz. From NTS.Proofs Require Import Distance CurveGeometry ArcOrient ArcIntersect - ArcOffsetThreePoint ArcArcCircles Atan2 AngleBetween. + ArcOffsetThreePoint ArcChordApprox ArcArcCircles ArcArcCirclesSpan + Atan2 AngleBetween. Local Open Scope R_scope. (* -------------------------------------------------------------------------- *) @@ -463,3 +469,222 @@ Qed. (* -------------------------------------------------------------------------- *) Print Assumptions arc_span_contains_atan2_iff_chord_sign. + +(* -------------------------------------------------------------------------- *) +(* §9 N-AA item ②: radical points on both circumcircles + atan2 discharge. *) +(* Vieta identities stay 3-axiom in ArcArcQuartic.v. *) +(* -------------------------------------------------------------------------- *) + +Lemma radical_plus_on_circle_a1 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + inCircle_R (arc_start a1) (arc_mid a1) (arc_end a1) + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) = 0. +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + destruct (radical_points_on_circles + (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) + (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) + Hdpos Hrabs Hdlt) + as [[HdP1 _] _]. + apply inCircle_R_zero_of_equidistant; [exact Hva1 |]. + assert (Hr1sq : arc_radius a1 * arc_radius a1 + = dist_sq (arc_center a1) (arc_start a1)). + { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. + unfold arc_radius_sq. reflexivity. } + lra. +Qed. + +Lemma radical_plus_on_circle_a2 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + inCircle_R (arc_start a2) (arc_mid a2) (arc_end a2) + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) = 0. +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + destruct (radical_points_on_circles + (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) + (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) + Hdpos Hrabs Hdlt) + as [[_ HdP2] _]. + apply inCircle_R_zero_of_equidistant; [exact Hva2 |]. + assert (Hr2sq : arc_radius a2 * arc_radius a2 + = dist_sq (arc_center a2) (arc_start a2)). + { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. + unfold arc_radius_sq. reflexivity. } + lra. +Qed. + +Lemma radical_minus_on_circle_a1 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + inCircle_R (arc_start a1) (arc_mid a1) (arc_end a1) + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) = 0. +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + destruct (radical_points_on_circles + (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) + (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) + Hdpos Hrabs Hdlt) + as [_ [HdM1 _]]. + apply inCircle_R_zero_of_equidistant; [exact Hva1 |]. + assert (Hr1sq : arc_radius a1 * arc_radius a1 + = dist_sq (arc_center a1) (arc_start a1)). + { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. + unfold arc_radius_sq. reflexivity. } + lra. +Qed. + +Lemma radical_minus_on_circle_a2 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + inCircle_R (arc_start a2) (arc_mid a2) (arc_end a2) + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) = 0. +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + destruct (radical_points_on_circles + (arc_center a1) (arc_center a2) (arc_radius a1) (arc_radius a2) + (arc_radius_pos a1 Hva1) (arc_radius_pos a2 Hva2) + Hdpos Hrabs Hdlt) + as [_ [_ HdM2]]. + apply inCircle_R_zero_of_equidistant; [exact Hva2 |]. + assert (Hr2sq : arc_radius a2 * arc_radius a2 + = dist_sq (arc_center a2) (arc_start a2)). + { rewrite arc_radius_eq_sqrt. rewrite sqrt_sqrt; [| apply arc_radius_sq_nonneg]. + unfold arc_radius_sq. reflexivity. } + lra. +Qed. + +Lemma radical_plus_span_iff_a1 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + (arc_span_contains_atan2 a1 + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) + <-> + arc_span_contains a1 + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2))). +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + apply arc_span_contains_atan2_iff_chord_sign; [exact Hva1 |]. + exact (radical_plus_on_circle_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). +Qed. + +Lemma radical_plus_span_iff_a2 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + (arc_span_contains_atan2 a2 + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) + <-> + arc_span_contains a2 + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2))). +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + apply arc_span_contains_atan2_iff_chord_sign; [exact Hva2 |]. + exact (radical_plus_on_circle_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). +Qed. + +Lemma radical_minus_span_iff_a1 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + (arc_span_contains_atan2 a1 + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) + <-> + arc_span_contains a1 + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2))). +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + apply arc_span_contains_atan2_iff_chord_sign; [exact Hva1 |]. + exact (radical_minus_on_circle_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). +Qed. + +Lemma radical_minus_span_iff_a2 : + forall a1 a2 : CircularArc, + valid_arc a1 -> valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + (arc_span_contains_atan2 a2 + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) + <-> + arc_span_contains a2 + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2))). +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt. + apply arc_span_contains_atan2_iff_chord_sign; [exact Hva2 |]. + exact (radical_minus_on_circle_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). +Qed. + +(* WITNESS {"claimId":"64","topic":"arc","lemma":"arc_arc_intersects_of_atan2_radical_span","title":"N-AA atan2 radical-span discharge: atan2 sector on one named radical point for both arcs implies arc_arc_intersects","file":"theories/ArcSpanAtan2.v"} *) + +Theorem arc_arc_intersects_of_atan2_radical_span : + forall a1 a2 : CircularArc, + valid_arc a1 -> + valid_arc a2 -> + 0 < dist (arc_center a1) (arc_center a2) -> + Rabs (arc_radius a1 - arc_radius a2) < dist (arc_center a1) (arc_center a2) -> + dist (arc_center a1) (arc_center a2) < arc_radius a1 + arc_radius a2 -> + ((arc_span_contains_atan2 a1 + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) /\ + arc_span_contains_atan2 a2 + (radical_point_plus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2))) + \/ + (arc_span_contains_atan2 a1 + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)) /\ + arc_span_contains_atan2 a2 + (radical_point_minus (arc_center a1) (arc_center a2) + (arc_radius a1) (arc_radius a2)))) -> + arc_arc_intersects a1 a2. +Proof. + intros a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt Hatan2. + apply (arc_arc_intersects_of_circles_and_radical_signs + a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). + destruct Hatan2 as [[H1 H2] | [H1 H2]]. + - left. split. + + apply (radical_plus_span_iff_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). + exact H1. + + apply (radical_plus_span_iff_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). + exact H2. + - right. split. + + apply (radical_minus_span_iff_a1 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). + exact H1. + + apply (radical_minus_span_iff_a2 a1 a2 Hva1 Hva2 Hdpos Hrabs Hdlt). + exact H2. +Qed. + +Print Assumptions arc_arc_intersects_of_atan2_radical_span. diff --git a/theories/CircleCircleResultant.v b/theories/CircleCircleResultant.v index 1f2e4228..c45dc499 100644 --- a/theories/CircleCircleResultant.v +++ b/theories/CircleCircleResultant.v @@ -27,8 +27,9 @@ Informal Bézout remark (not proved here): two conics meet in 4 points, 2 at the circular points at infinity; the affine - certificate is degree ≤ 2. `ArcArcQuartic.v` stays the 4-axiom - atan2/Vieta discharge; this file does not Require it. + certificate is degree ≤ 2. `ArcArcQuartic.v` is the 3-axiom Vieta + certificate; atan2 discharge lives in `ArcSpanAtan2.v`. This file + does not Require either. HEADLINE (constructor ⇒ resultant root; one named Year-1 guard): `radical_points_satisfy_circle_circle_res` diff --git a/theories/NurbsConicExact.v b/theories/NurbsConicExact.v index 9e2deafd..97cee3db 100644 --- a/theories/NurbsConicExact.v +++ b/theories/NurbsConicExact.v @@ -28,9 +28,11 @@ Stdlib `atan` is unavoidable for the explicit preimage (the reparam contract forbids IVT). That pulls Classical_Prop.classic; this file is Category C in docs/audit-exceptions.txt, same atan lineage as - ArcParamBridge.v. The CurveLength / ArcRectifiable engines stay - 3-axiom in their own files. No CurveSegment growth, no ADR-0004 - remint, no new 64-a r·θ. + ArcParamBridge.v. The CurveLength / ArcRectifiable / NurbsKnotSpans + engines stay 3-axiom in their own files. The two-golden-quarter + half-circle instance (508-g) is here so NurbsKnotSpans can leave the + exceptions list. No CurveSegment growth, no ADR-0004 remint, no new + 64-a r·θ. WITNESS topic: metric · claimId: 508-a · witness: 508-a-golden-quarter macro: metric @@ -45,9 +47,11 @@ Assisted-by: Cursor Grok 4.6 ========================================================================== *) -From Stdlib Require Import Reals Lra Ratan. +From Stdlib Require Import Reals Lra Ratan List. From NTS.Proofs Require Import - Distance CurveLength ArcRectifiable NurbsQuadraticLength AtanDoubleAngle. + Distance CurveLength ArcRectifiable NurbsQuadraticLength AtanDoubleAngle + NurbsKnotSpans. +Import ListNotations. Local Open Scope R_scope. (* -------------------------------------------------------------------------- *) @@ -444,3 +448,174 @@ Proof. Qed. Print Assumptions nurbs2_golden_quarter_length. + +(* -------------------------------------------------------------------------- *) +(* 508-g instance: rotate-90 second quadrant + two-span half-circle. *) +(* Knot-vector induction stays 3-axiom in NurbsKnotSpans.v. *) +(* -------------------------------------------------------------------------- *) + +Definition rot90 (p : Point) : Point := mkPoint (- py p) (px p). + +Lemma rot90_dist_sq : forall p q, dist_sq (rot90 p) (rot90 q) = dist_sq p q. +Proof. + intros p q. unfold dist_sq, rot90. simpl. ring. +Qed. + +Lemma rot90_dist : forall p q, dist (rot90 p) (rot90 q) = dist p q. +Proof. + intros p q. unfold dist. f_equal. apply rot90_dist_sq. +Qed. + +Lemma polyline_len_isometry : + forall (f : Point -> Point) (g : Curve) ts t, + (forall p q, dist (f p) (f q) = dist p q) -> + polyline_len (fun u => f (g u)) t ts = polyline_len g t ts. +Proof. + intros f g ts; induction ts as [|u tl IH]; intros t Hf; simpl. + - reflexivity. + - rewrite Hf, (IH u Hf). reflexivity. +Qed. + +Lemma is_curve_length_isometry : + forall (f : Point -> Point) (g : Curve) a b L, + (forall p q, dist (f p) (f q) = dist p q) -> + is_curve_length g a b L -> + is_curve_length (fun t => f (g t)) a b L. +Proof. + intros f g a b L Hf [Hub Hlst]. + split. + - intros l (ts & Hch & Hl). subst l. + apply Hub. exists ts. split; [exact Hch |]. + rewrite <- (polyline_len_isometry f g (ts ++ [b]) a Hf). + reflexivity. + - intros M HM. apply Hlst. intros l (ts & Hch & Hl). subst l. + apply HM. exists ts. split; [exact Hch |]. + rewrite (polyline_len_isometry f g (ts ++ [b]) a Hf). + reflexivity. +Qed. + +Lemma rot90_nurbs2_pt : forall p0 p1 p2 w0 w1 w2 t, + nurbs2_pt (rot90 p0) (rot90 p1) (rot90 p2) w0 w1 w2 t + = rot90 (nurbs2_pt p0 p1 p2 w0 w1 w2 t). +Proof. + intros p0 p1 p2 w0 w1 w2 t. + unfold nurbs2_pt, rot90, nurbs2_den. simpl. + apply point_ext; simpl. + - rewrite <- Ropp_div. f_equal. ring. + - reflexivity. +Qed. + +Definition golden_q2_p0 : Point := rot90 golden_p0. +Definition golden_q2_p1 : Point := rot90 golden_p1. +Definition golden_q2_p2 : Point := rot90 golden_p2. + +Definition golden_q2_param : Curve := + nurbs2_param golden_q2_p0 golden_q2_p1 golden_q2_p2 + golden_w0 golden_w1 golden_w2. + +Lemma golden_q2_rot : forall t, + golden_q2_param t = rot90 (golden_param t). +Proof. + intro t. + unfold golden_q2_param, golden_param, nurbs2_param. + unfold golden_q2_p0, golden_q2_p1, golden_q2_p2. + apply rot90_nurbs2_pt. +Qed. + +Theorem golden_q2_length : + is_curve_length golden_q2_param 0 1 (PI / 2). +Proof. + apply (is_curve_length_ext (fun t => rot90 (golden_param t)) + golden_q2_param). + - intro t. symmetry. apply golden_q2_rot. + - apply (is_curve_length_isometry rot90 golden_param). + + apply rot90_dist. + + exact nurbs2_golden_quarter_length. +Qed. + +Definition golden_half (t : R) : Point := + match Rle_dec t 1 with + | left _ => golden_param t + | right _ => golden_q2_param (t - 1) + end. + +Lemma golden_param_at_1 : golden_param 1 = mkPoint 0 1. +Proof. + unfold golden_param, nurbs2_param, nurbs2_pt, nurbs2_den. + unfold golden_p0, golden_p1, golden_p2, golden_w0, golden_w1, golden_w2. + unfold bern2_0, bern2_1, bern2_2. simpl. + apply point_ext; simpl; field. +Qed. + +Lemma golden_q2_param_at_0 : golden_q2_param 0 = mkPoint 0 1. +Proof. + unfold golden_q2_param, nurbs2_param, nurbs2_pt, nurbs2_den. + unfold golden_q2_p0, golden_q2_p1, golden_q2_p2, rot90. + unfold golden_p0, golden_p1, golden_p2, golden_w0, golden_w1, golden_w2. + unfold bern2_0, bern2_1, bern2_2. simpl. + apply point_ext; simpl; field. +Qed. + +Lemma golden_half_glue : golden_param 1 = golden_q2_param 0. +Proof. + rewrite golden_param_at_1, golden_q2_param_at_0. reflexivity. +Qed. + +Lemma golden_half_on_span0 : forall t, t <= 1 -> golden_half t = golden_param t. +Proof. + intros t Ht. unfold golden_half. + destruct (Rle_dec t 1) as [Hle | Hgt]; [reflexivity | lra]. +Qed. + +Lemma golden_half_on_span1 : + forall t, 1 <= t -> golden_half t = golden_q2_param (t - 1). +Proof. + intros t Ht. unfold golden_half. + destruct (Rle_dec t 1) as [Hle | Hgt]. + - assert (Heq : t = 1) by lra. rewrite Heq. + replace (1 - 1) with 0 by ring. + exact golden_half_glue. + - reflexivity. +Qed. + +Lemma golden_half_span0 : is_curve_length golden_half 0 1 (PI / 2). +Proof. + apply (is_curve_length_ext_on golden_param golden_half). + - intros t _ Ht1. symmetry. apply golden_half_on_span0. exact Ht1. + - exact nurbs2_golden_quarter_length. +Qed. + +Lemma golden_half_span1 : is_curve_length golden_half 1 2 (PI / 2). +Proof. + apply (is_curve_length_ext_on + (fun t => golden_q2_param (t - 1)) golden_half). + - intros t Ht1 _. symmetry. apply golden_half_on_span1. exact Ht1. + - apply (is_curve_length_ext + (fun t => golden_q2_param (-1 + t)) + (fun t => golden_q2_param (t - 1))). + + intro t. f_equal. ring. + + pose proof (is_curve_length_shift golden_q2_param (-1) 1 2 (PI / 2)) + as Hshift. + replace (-1 + 1) with 0 in Hshift by ring. + replace (-1 + 2) with 1 in Hshift by ring. + apply Hshift. exact golden_q2_length. +Qed. + +(* WITNESS {"claimId":"508-g","witness":"508-g-nurbs-spans","topic":"metric","lemma":"golden_half_circle_length","title":"Two golden quarter NURBS spans glue to a half-circle of length π","file":"theories/NurbsConicExact.v","board":"#565"} *) + +Theorem golden_half_circle_length : + is_curve_length golden_half 0 2 PI. +Proof. + pose (Ls := [PI / 2; PI / 2]). + assert (H : is_curve_length golden_half 0 2 (list_sum Ls)). + { apply (nurbs_spans_additive golden_half 0 [1] 2 Ls). + - unfold knot_vector. simpl. split; lra. + - unfold Ls. simpl. split. + + exact golden_half_span0. + + exact golden_half_span1. } + unfold Ls, list_sum in H. simpl in H. + replace (PI / 2 + (PI / 2 + 0)) with PI in H by lra. + exact H. +Qed. + +Print Assumptions golden_half_circle_length. diff --git a/theories/NurbsKnotSpans.v b/theories/NurbsKnotSpans.v index 803b3335..8d417d12 100644 --- a/theories/NurbsKnotSpans.v +++ b/theories/NurbsKnotSpans.v @@ -1,8 +1,7 @@ (* ============================================================================ NetTopologySuite.Proofs.NurbsKnotSpans ---------------------------------------------------------------------------- - Issue #565 / claimId 508-g: knot-vector carrier + induction over spans, - and the two-golden-quarter half-circle instance. + Issue #565 / claimId 508-g: knot-vector carrier + induction over spans. NurbsGeneralLength.nurbs_knot_span_additive is already the two-window special case (curve_length_additive on one curve). This file does NOT @@ -13,9 +12,9 @@ 3. nurbs_spans_additive : induction on the interior-knot list (curve_length_additive at each cons; no new analysis) - Instance: two quadratic golden spans glued at (0,1) — first quadrant - from 508-a, second quadrant the rotate-90 image — on knots [0; 1; 2]. - Total length is π, which is π/2 + π/2, not a new π theorem. + The two-golden-quarter half-circle instance (π/2 + π/2 = π) lives in + NurbsConicExact.v — Category C through 508-a atan. This file stays + 3-axiom. Not Cox-de Boor multi-span evaluation. Oracle N stays single-span. Not a CurveSegment / Exact* zoo type. Does not steal 508-e / 508-h. @@ -35,8 +34,7 @@ ========================================================================== *) From Stdlib Require Import Reals Lra List. -From NTS.Proofs Require Import - Distance CurveLength NurbsQuadraticLength NurbsConicExact. +From NTS.Proofs Require Import Distance CurveLength. Import ListNotations. Local Open Scope R_scope. @@ -93,178 +91,5 @@ Print Assumptions nurbs_spans_additive. (* The two-window special case is already NurbsGeneralLength.nurbs_knot_span_additive - (= CurveLength.curve_length_additive). This file does not remint it. *) - -(* -------------------------------------------------------------------------- *) -(* Rotate-90 isometry (second-quadrant golden span). *) -(* -------------------------------------------------------------------------- *) - -Definition rot90 (p : Point) : Point := mkPoint (- py p) (px p). - -Lemma rot90_dist_sq : forall p q, dist_sq (rot90 p) (rot90 q) = dist_sq p q. -Proof. - intros p q. unfold dist_sq, rot90. simpl. ring. -Qed. - -Lemma rot90_dist : forall p q, dist (rot90 p) (rot90 q) = dist p q. -Proof. - intros p q. unfold dist. f_equal. apply rot90_dist_sq. -Qed. - -Lemma polyline_len_isometry : - forall (f : Point -> Point) (g : Curve) ts t, - (forall p q, dist (f p) (f q) = dist p q) -> - polyline_len (fun u => f (g u)) t ts = polyline_len g t ts. -Proof. - intros f g ts; induction ts as [|u tl IH]; intros t Hf; simpl. - - reflexivity. - - rewrite Hf, (IH u Hf). reflexivity. -Qed. - -Lemma is_curve_length_isometry : - forall (f : Point -> Point) (g : Curve) a b L, - (forall p q, dist (f p) (f q) = dist p q) -> - is_curve_length g a b L -> - is_curve_length (fun t => f (g t)) a b L. -Proof. - intros f g a b L Hf [Hub Hlst]. - split. - - intros l (ts & Hch & Hl). subst l. - apply Hub. exists ts. split; [exact Hch |]. - rewrite <- (polyline_len_isometry f g (ts ++ [b]) a Hf). - reflexivity. - - intros M HM. apply Hlst. intros l (ts & Hch & Hl). subst l. - apply HM. exists ts. split; [exact Hch |]. - rewrite (polyline_len_isometry f g (ts ++ [b]) a Hf). - reflexivity. -Qed. - -Lemma rot90_nurbs2_pt : forall p0 p1 p2 w0 w1 w2 t, - nurbs2_pt (rot90 p0) (rot90 p1) (rot90 p2) w0 w1 w2 t - = rot90 (nurbs2_pt p0 p1 p2 w0 w1 w2 t). -Proof. - intros p0 p1 p2 w0 w1 w2 t. - unfold nurbs2_pt, rot90, nurbs2_den. simpl. - apply point_ext; simpl. - - rewrite <- Ropp_div. f_equal. ring. - - reflexivity. -Qed. - -Definition golden_q2_p0 : Point := rot90 golden_p0. -Definition golden_q2_p1 : Point := rot90 golden_p1. -Definition golden_q2_p2 : Point := rot90 golden_p2. - -Definition golden_q2_param : Curve := - nurbs2_param golden_q2_p0 golden_q2_p1 golden_q2_p2 - golden_w0 golden_w1 golden_w2. - -Lemma golden_q2_rot : forall t, - golden_q2_param t = rot90 (golden_param t). -Proof. - intro t. - unfold golden_q2_param, golden_param, nurbs2_param. - unfold golden_q2_p0, golden_q2_p1, golden_q2_p2. - apply rot90_nurbs2_pt. -Qed. - -Theorem golden_q2_length : - is_curve_length golden_q2_param 0 1 (PI / 2). -Proof. - apply (is_curve_length_ext (fun t => rot90 (golden_param t)) - golden_q2_param). - - intro t. symmetry. apply golden_q2_rot. - - apply (is_curve_length_isometry rot90 golden_param). - + apply rot90_dist. - + exact nurbs2_golden_quarter_length. -Qed. - -(* -------------------------------------------------------------------------- *) -(* Piecewise two-span half-circle on knots [0; 1; 2]. *) -(* -------------------------------------------------------------------------- *) - -Definition golden_half (t : R) : Point := - match Rle_dec t 1 with - | left _ => golden_param t - | right _ => golden_q2_param (t - 1) - end. - -Lemma golden_param_at_1 : golden_param 1 = mkPoint 0 1. -Proof. - unfold golden_param, nurbs2_param, nurbs2_pt, nurbs2_den. - unfold golden_p0, golden_p1, golden_p2, golden_w0, golden_w1, golden_w2. - unfold bern2_0, bern2_1, bern2_2. simpl. - apply point_ext; simpl; field. -Qed. - -Lemma golden_q2_param_at_0 : golden_q2_param 0 = mkPoint 0 1. -Proof. - unfold golden_q2_param, nurbs2_param, nurbs2_pt, nurbs2_den. - unfold golden_q2_p0, golden_q2_p1, golden_q2_p2, rot90. - unfold golden_p0, golden_p1, golden_p2, golden_w0, golden_w1, golden_w2. - unfold bern2_0, bern2_1, bern2_2. simpl. - apply point_ext; simpl; field. -Qed. - -Lemma golden_half_glue : golden_param 1 = golden_q2_param 0. -Proof. - rewrite golden_param_at_1, golden_q2_param_at_0. reflexivity. -Qed. - -Lemma golden_half_on_span0 : forall t, t <= 1 -> golden_half t = golden_param t. -Proof. - intros t Ht. unfold golden_half. - destruct (Rle_dec t 1) as [Hle | Hgt]; [reflexivity | lra]. -Qed. - -Lemma golden_half_on_span1 : - forall t, 1 <= t -> golden_half t = golden_q2_param (t - 1). -Proof. - intros t Ht. unfold golden_half. - destruct (Rle_dec t 1) as [Hle | Hgt]. - - assert (Heq : t = 1) by lra. rewrite Heq. - replace (1 - 1) with 0 by ring. - exact golden_half_glue. - - reflexivity. -Qed. - -Lemma golden_half_span0 : is_curve_length golden_half 0 1 (PI / 2). -Proof. - apply (is_curve_length_ext_on golden_param golden_half). - - intros t _ Ht1. symmetry. apply golden_half_on_span0. exact Ht1. - - exact nurbs2_golden_quarter_length. -Qed. - -Lemma golden_half_span1 : is_curve_length golden_half 1 2 (PI / 2). -Proof. - apply (is_curve_length_ext_on - (fun t => golden_q2_param (t - 1)) golden_half). - - intros t Ht1 _. symmetry. apply golden_half_on_span1. exact Ht1. - - apply (is_curve_length_ext - (fun t => golden_q2_param (-1 + t)) - (fun t => golden_q2_param (t - 1))). - + intro t. f_equal. ring. - + pose proof (is_curve_length_shift golden_q2_param (-1) 1 2 (PI / 2)) - as Hshift. - replace (-1 + 1) with 0 in Hshift by ring. - replace (-1 + 2) with 1 in Hshift by ring. - apply Hshift. exact golden_q2_length. -Qed. - -(* WITNESS {"claimId":"508-g","witness":"508-g-nurbs-spans","topic":"metric","lemma":"golden_half_circle_length","title":"Two golden quarter NURBS spans glue to a half-circle of length π","file":"theories/NurbsKnotSpans.v","board":"#565"} *) - -Theorem golden_half_circle_length : - is_curve_length golden_half 0 2 PI. -Proof. - pose (Ls := [PI / 2; PI / 2]). - assert (H : is_curve_length golden_half 0 2 (list_sum Ls)). - { apply (nurbs_spans_additive golden_half 0 [1] 2 Ls). - - unfold knot_vector. simpl. split; lra. - - unfold Ls. simpl. split. - + exact golden_half_span0. - + exact golden_half_span1. } - unfold Ls, list_sum in H. simpl in H. - replace (PI / 2 + (PI / 2 + 0)) with PI in H by lra. - exact H. -Qed. - -Print Assumptions golden_half_circle_length. + (= CurveLength.curve_length_additive). This file does not remint it. + The golden half-circle instance is NurbsConicExact.golden_half_circle_length. *)