oracle+theories: #423 t10 line 2 — HAUSDORFF_* emit directed_discrete_h (q_ddh_sq)

Keep main's HausdorffDensify.v (line 1 from #792). Add HausdorffDiscreteQ.v
and ADR-0006 adapters HAUSDORFF_DIRECTED / HAUSDORFF_SYMM. JTS pair → 500/1
(√500), not locus/47.8. #423 stays open.

Author: claude

.github/workflows/build-oracle.yml

@@ -236,6 +236,8 @@ jobs:
             > oracle/arc_distance_tests.txt
           ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_i_circular_tests.py \
             > oracle/i_circular_tests.txt
+          ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_hausdorff_tests.py \
+            > oracle/hausdorff_tests.txt
           ORACLE_BIN=oracle/oracle_bin python3 oracle/gen_ieee_oracle_bridge_tests.py \
             > oracle/ieee_oracle_bridge_run.txt
 

README.md

@@ -87,8 +87,8 @@ make host
 ```
 
 `make host` builds the 78 modules in `_CoqProject`, the foundational
-Stdlib-only layer. The full corpus is 636 registered modules —
-545 registered under `theories/` and 91 registered under
+Stdlib-only layer. The full corpus is 637 registered modules —
+546 registered under `theories/` and 91 registered under
 `theories-flocq/` — and is the pinned container.
 Toolchain: **Rocq 9.2.0 + Flocq 4.2.2**. Those counts, the two
 audit-exception counts above, and the `Defined.` count are checked against

TRIAGE_NTS_JTS_ISSUES.md

@@ -347,7 +347,7 @@ witness: <fixture or none>
 6. **#423** — Formal proofs for distance metrics: directed/discrete Hausdorff
    and Fréchet correctness (`metric`). `423-a` / `423-b` Green. Ticket-10
    line 1 (densification bound) Green: `HausdorffDensify.v : densify_step_bound`;
-   line 2 (`HAUSDORFF_DIRECTED` / `HAUSDORFF_SYMM`) remains. JTS locus class is unported
+   line 2 Green: `HAUSDORFF_DIRECTED` / `HAUSDORFF_SYMM` over `HausdorffDiscreteQ.v : q_ddh_sq`. JTS locus class is unported
    on NTS develop (NTS#812). Engine grill:
    [`docs/scout/map-hausdorff-functions.md`](docs/scout/map-hausdorff-functions.md).
 7. **#424** — Formal proofs for hull constructions: minimum bounding triangle,

_CoqProject.full

@@ -3351,6 +3351,7 @@ theories/LECArcRow.v
 # Full-only: imports LargestEmptyCircle.v, LECObstacleDistance.v.
 theories/LECSegmentRow.v
 theories/HausdorffDensify.v
+theories/HausdorffDiscreteQ.v
 
 # The LEC n-ary FLATTEN row (ledger rung "CompoundCurve / n-ary flatten"
 # closed + failed path F5).  Generic exact_clearance algebra (union = Rmin,

docs/READING-GUIDE.md

@@ -582,7 +582,7 @@ The repository has two source directories:
 
 The host lane builds the 78 modules in `_CoqProject`, the
 foundational `theories/` layer;
-the container `_CoqProject.full` builds the entire corpus (636 registered modules — 545 registered under `theories/`, 91 registered under `theories-flocq/`).
+the container `_CoqProject.full` builds the entire corpus (637 registered modules — 546 registered under `theories/`, 91 registered under `theories-flocq/`).
 
 **Status.** The foundational layer (real-number, vector, distance,
 orientation, segment, bbox, triangle, convex, lex-order, plus their
@@ -771,7 +771,7 @@ for Scholar Sam / Tech-Lead Tess / Joost the BDFL paths.
   proofs don't reach: floating-point rounding, exceptions, performance,
   cross-platform consistency, interaction with the rest of the runtime.
 - This is **not** complete. Current coverage is over 7,600 Qed-closed
-  theorems across 636 registered modules — 545 registered under `theories/`,
+  theorems across 637 registered modules — 546 registered under `theories/`,
   91 registered under `theories-flocq/` (78 of them modules in `_CoqProject`
   as the host foundational target). There are **no
   `Admitted` theorems today** — both the counterexample and

docs/oracle-handrolled-allowlist.txt

@@ -473,3 +473,14 @@ run_envelope_unified
 # non-degenerate inputs; on-boundary behaviour (point on vertex/edge) returns 0
 # consistently (implementation-defined, documented in gen_winding_number_tests.py).
 run_winding_number
+
+# --- HAUSDORFF_DIRECTED / HAUSDORFF_SYMM : INTERFACE-BOUNDARY -----------------
+# Mode: HAUSDORFF_DIRECTED / HAUSDORFF_SYMM (#423 ticket-10 line 2).
+# Java/C#: JTS DiscreteHausdorffDistance.distance / orientedDistance (NTS
+# DiscreteHausdorffDistance.Distance) return Math.sqrt of the squared
+# max-min; the sqrt is the transcendental step with no Coq-extractable form.
+# Exact companion: the squared value is the Coq-EXTRACTED rational
+# HausdorffDiscreteQ.q_ddh_sq / q_hsymm_sq (agreement theorems q_ddh_sq_R /
+# q_hsymm_sq_R against HausdorffDensify.directed_discrete_h), printed as the
+# second wire token `num/den`; the float token is sqrt(num/den) rounded once.
+hausdorff_wire_of_q

docs/scout/map-hausdorff-functions.md

@@ -135,7 +135,7 @@ Last port comment: JTS-1.10 `DiscreteHausdorffDistance`. No
 | Already Green | Remaining ask (ticket 10; do not remint) |
 |---|---|
 | `HausdorffDiscrete.v : directed_discrete_hausdorff_max_min` (`423-a`) | Densification bound landed: `HausdorffDensify.v : densify_step_bound` (line 1); line 2 below remains |
-| `HausdorffMetricSym.v` / `HausdorffMetricInstance.v` (HKR symmetrization, discrete instance) | Oracle modes `HAUSDORFF_DIRECTED` / `HAUSDORFF_SYMM` |
+| `HausdorffMetricSym.v` / `HausdorffMetricInstance.v` (HKR symmetrization, discrete instance) | Oracle modes landed: `HAUSDORFF_DIRECTED` / `HAUSDORFF_SYMM` over `HausdorffDiscreteQ.v : q_ddh_sq` (line 2); #423 stays open (Fréchet gap, NTS#812, locus class) |
 | `FrechetDiscrete.v` / `423-b` discrete Fréchet | — |
 | `Linearise.v : hausdorff_le` sandwich | **Not** the engine. Do not steal it as the densify bound |
 

docs/verified-claims.md

@@ -217,7 +217,7 @@ Unconditional exact-reals — the most directly citable rows.
 | `ArcMinorWitness.v : major_arc_witness_naive_bound_fails` (+ `major_arc_witness_not_minor`, `major_arc_witness_mid_far_from_chord`, `major_arc_witness_sagitta_lt_sqrt2_sq`) | **Why `arc_minor` is required (companion counterexample, in the style of `SpectreChordArcWitness.v`):** the three control points `(1,0)`, `(-1,0)`, `(0,1)` on the unit circle trace the "major" labeling — 270° the long way around from start to end — so `arc_mid = (-1,0)` sits on the SAME side of the chord as the circumcenter (`arc_side_chord` same sign at both), failing `arc_minor` (`major_arc_witness_not_minor`). `arc_mid` is unconditionally (for every segment parameter `t`, not just `t ∈ [0,1]`) at distance `≥ √2` from the chord segment `(1,0)–(0,1)` (`major_arc_witness_mid_far_from_chord`, via `dist_sq(mid, segment_point t) − 2 = 2(t−1)² ≥ 0`), while `sagitta² < 2` (`major_arc_witness_sagitta_lt_sqrt2_sq`, reusing `sagitta_nonneg`/`sagitta_le_arc_radius` rather than recomputing the exact sagitta) — so the naive unconditional "every arc point is within sagitta of the chord segment" claim fails by a wide margin exactly on the major side, motivating the `arc_minor` hypothesis `ArcHotPixelSagittaBridge.v` requires. **3-axiom** (no exemption) `[exact]` | 3 |
 | `ArcHotPixelSagittaBridge.v : arc_touches_implies_chord_touches_margin` (+ `arc_point_near_chord_segment`, `chord_misses_margin_implies_arc_misses`, `chord_endpoint_touches_implies_arc_touches`) | **Sagitta / hot-pixel bridge (issue #64), the correctly-qualified replacement for the bare claim `SpectreChordArcWitness.v` refutes:** `SpectreChordArcWitness.v` disproves "chord touches a hot pixel ⟹ arc touches it" unconditionally; the honest fix needs BOTH an `arc_minor` hypothesis (subtended angle ≤ π — `ArcOrient.arc_minor`, the regime the chord-sign span test is designed for; the major-side failure is exhibited concretely by `ArcMinorWitness.v`) AND a sagitta-margin dilation on the chord side, not a bare bidirectional bound. Core lemma `arc_point_near_chord_segment`: for a valid, `arc_minor` arc, every in-span on-circumcircle point `Y` is within `sagitta a` of some point of the actual chord SEGMENT `[arc_start a, arc_end a]` (not just the chord line or a fixed midpoint) — witness parameter `t = alongS(Y)/W`; proved via the 2-D Lagrange identity at two base points (`arc_center`, `chord_midpoint`), `arc_minor` + `arc_span_contains` giving the sign condition `Q·perp(Y) ≤ 0`, and a case split on `Q = ±√W·d` bounding `perp(Y)² ≤ W·sagitta²`. Headline `arc_touches_implies_chord_touches_margin`: a sound REJECTION filter (arc touches a hot pixel ⟹ the sagitta-dilated chord touches it too), the curved analogue of `HotPixel.segment_touches_implies_bb_overlap`'s cheap pre-filter. Pure algebra, no new trig/atan2, **3-axiom** (no exemption). Deferred: `ArcOverlay.v`'s `H_A_bridge`/`H_B_bridge` need the OPPOSITE direction (chord-region point ⇒ nearby arc point) — a distinct, harder gap this file does not close `[exact]` | 3 |
 | `ArcSegmentJordanSound.v : arc_seg_parity_membership_sound_in_true_segment` (+ `gtri_pos_implies_in_arc_control_triangle`, `arc_seg_geometry_parity_sound_in_true_segment`) | **V-CP Jordan soundness (issue #64), a bounded next rung for the single-arc circular-segment ("lens") curve geometry:** bridges two already-`Qed` pieces one algebraic step apart — `RelateCurveArcSegment.arc_seg_control_interior_in_curve_geometry` (real ray-parity membership on the `arc_seg_curve_geometry` `to_geometry` object reduces, under `ray_avoids_vertices`, to `0 < gtri (arc_start a)(arc_mid a)(arc_end a) p`) and `ArcControlTriangleInSegment.arc_control_triangle_in_circular_segment` (affine control-triangle interior ⇒ TRUE circular-segment membership). The new bridge `gtri_pos_implies_in_arc_control_triangle`: `gtri`-positivity gives the three inward signed areas `gsA,gsB,gsC > 0` (`GeneralTriangleSeparation.gtri_pos_iff`), whose sum IS `gdbl` (`g_sum`) — so `gdbl > 0` (hence CCW) comes for free, no separate orientation hypothesis needed — and `beta := gsC/gdbl` (weight of `arc_mid`), `gamma := gsA/gdbl` (weight of `arc_end`) satisfy `in_arc_control_triangle`'s affine-combination conditions via `g_baryx`/`g_baryy` (`field`/`nra`). Composed headline: genuine ray-parity membership on a real curved `to_geometry` object provably implies TRUE-region membership — the first such instance in the corpus, for the single-arc-lens case. **3-axiom** (no exemption). Deferred (unchanged, thesis-scale/RED): multi-arc rings with holes, self-tangency, the general `{-1,0,+1}` winding characterization, and the general Jordan Curve Theorem `[exact]` | 3 |
-| `HausdorffDiscrete.v : directed_discrete_hausdorff_max_min` (+ `min_dist_sq_to_le`, `min_dist_sq_to_attained`, `ddh_ge_component`, `ddh_attained`, `min_dist_sq_to_step`, `ddh_step`, `min_dist_sq_to_nonneg`, `directed_hausdorff_sq_nonneg`) | **423-a Green — the directed discrete Hausdorff value is the attained max-min** (Huttenlocher–Klanderman–Rucklidge 1993 eq (2), the h(A,B) of JTS/NTS DiscreteHausdorffDistance, squared convention): on nonempty lists, *cover* — every A-point has a B-point within h — and *attain* — some A-point is at ≥ h from every B-point — hold for h = `directed_hausdorff_sq A B`, so h is exactly max-min and both the max and the inner min are realised. The four aggregation facts are instantiations of the shared score-agnostic layer (`MaxMinScore.v`, post-#431/#432 consolidation); nonnegativity closes the package. Mirrored self-contained in `eval/Claim423a.v` with the rational pins (pair 1/1; asymmetric 4/9 min-inside/max-outside/directedness killers; WITNESS 423-a, topic: metric). Ticket-10 line 1 (claimId `423-t10-densify`, vertices-against-locus, unsquared, not a 423-a remint): the locus h is a term by completeness (`HausdorffDensify.v : directed_locus_h`), discrete ≤ locus (`HausdorffDensify.v : discrete_le_locus`), densify-step bound 0 ≤ locus − discrete(A') ≤ δ with f(δ) = δ (`HausdorffDensify.v : densify_step_bound`, `HausdorffDensify.v : densify_step_bound_max_edge`), and on the JTS pair (0 0, 100 0, 10 100) vs (0 100, 0 10, 80 10) discrete = √500 < 910/19 ≤ locus (`HausdorffDensify.v : jts_discrete_value`, `HausdorffDensify.v : jts_locus_lower`, `HausdorffDensify.v : jts_discrete_strictly_below_locus`, `HausdorffDensify.v : ticket_423_t10_line1_qed_or_qex`); line 2 (`HAUSDORFF_*` modes) remains `[exact]` | 3 |
+| `HausdorffDiscrete.v : directed_discrete_hausdorff_max_min` (+ `min_dist_sq_to_le`, `min_dist_sq_to_attained`, `ddh_ge_component`, `ddh_attained`, `min_dist_sq_to_step`, `ddh_step`, `min_dist_sq_to_nonneg`, `directed_hausdorff_sq_nonneg`) | **423-a Green — the directed discrete Hausdorff value is the attained max-min** (Huttenlocher–Klanderman–Rucklidge 1993 eq (2), the h(A,B) of JTS/NTS DiscreteHausdorffDistance, squared convention): on nonempty lists, *cover* — every A-point has a B-point within h — and *attain* — some A-point is at ≥ h from every B-point — hold for h = `directed_hausdorff_sq A B`, so h is exactly max-min and both the max and the inner min are realised. The four aggregation facts are instantiations of the shared score-agnostic layer (`MaxMinScore.v`, post-#431/#432 consolidation); nonnegativity closes the package. Mirrored self-contained in `eval/Claim423a.v` with the rational pins (pair 1/1; asymmetric 4/9 min-inside/max-outside/directedness killers; WITNESS 423-a, topic: metric). Ticket-10 line 1 (claimId `423-t10-densify`, vertices-against-locus, unsquared, not a 423-a remint): the locus h is a term by completeness (`HausdorffDensify.v : directed_locus_h`), discrete ≤ locus (`HausdorffDensify.v : discrete_le_locus`), densify-step bound 0 ≤ locus − discrete(A') ≤ δ with f(δ) = δ (`HausdorffDensify.v : densify_step_bound`, `HausdorffDensify.v : densify_step_bound_max_edge`), and on the JTS pair (0 0, 100 0, 10 100) vs (0 100, 0 10, 80 10) discrete = √500 < 910/19 ≤ locus (`HausdorffDensify.v : jts_discrete_value`, `HausdorffDensify.v : jts_locus_lower`, `HausdorffDensify.v : jts_discrete_strictly_below_locus`, `HausdorffDensify.v : ticket_423_t10_line1_qed_or_qex`); line 2 (claimId `423-t10-oracle`): `HAUSDORFF_DIRECTED` / `HAUSDORFF_SYMM` attach as ADR-0006 adapters (`oracle/driver.ml`, generator `oracle/gen_hausdorff_tests.py`) over the Coq-extracted exact rationals `HausdorffDiscreteQ.v : q_ddh_sq` / `HausdorffDiscreteQ.v : q_hsymm_sq`, whose square roots are the proven values (`HausdorffDiscreteQ.v : sqrt_q_ddh_sq`, `HausdorffDiscreteQ.v : sqrt_q_hsymm_sq`, via `HausdorffDiscreteQ.v : q_ddh_sq_R`); JTS pair `HausdorffDiscreteQ.v : jts_q_ddh_sq_500`; the wire prints sqrt once past the exact companion (INTERFACE-BOUNDARY `hausdorff_wire_of_q`); locus value not extracted (`HausdorffDiscreteQ.v : ticket_423_t10_line2_qed_or_qex`) `[exact]` | 3 |
 | `PenetrationGauge.v : gauge_hex_sublevel` (+ `gauge_hex_nonneg`, `gauge_hex_zero_iff`, `gauge_hex_abs_homogeneous`, `gauge_hex_subadditive`, `gauge_hex_unit_ball`, `gauge_sandwich`, vertex/edge/interior pins) | **Wen–Zhang (IEEE RA-L 2022) Lemma 2 at the paper's hexagon gauge (eq 18a):** the closed-form gauge `max((|x|+|y|)/2, |y|)` is nonnegative, definite, absolutely homogeneous, subadditive, and its sublevel sets are exactly the dilations `λF` — the identity that turns "largest inscribed dilation" (generalized penetration depth, eq 9) into 1-D root finding. Norm-equivalence sandwich `ℓ¹/2 ≤ hex ≤ ℓ∞ ≤ ℓ¹` bounds any cross-gauge depth swap by 2×. Rational vertex (2,0)/(1,1)/(0,1) and interior (1,1/2) pins; strict probes kill the ℓ∞ and ℓ¹ misreadings. All rational Rmax/Rabs case algebra `[exact]` | 3 |
 | `PenetrationMinimax.v : secant_step_safe` (+ `convex_three_point`, `interval_minkowski_diff`, `f_box_nonneg`, `f_box_nondecreasing`, `f_box_convex`, `f_box_zero_iff`, `box_inclusion_iff_le`, `box_inclusion_iff_fzero`, `f_box_affine_above`, `secant_one_step_exact`, `secant_pin_paper_init`, `secant_box_never_undershoots`) | **Wen–Zhang Theorems 1–2 mechanics + the exactly-solvable box instance (eqs 9–13):** the secant iterate for the largest zero of a convex nondecreasing profile stays in `[λ*, λᵏ)` — never undershoots, i.e. never reports overlapping bodies "separated" — derived from the convexity inequality alone via the cleared three-slope lemma (even the slope gap is derived). Box model: `f(λ) = max(0, λ−c)` satisfies Theorem 1, eq (10)'s inclusion ⟺ h = 0 ⟺ λ ≤ c chain is exact, the 1-D interval Minkowski difference is `[−(s+u), s+u]`, and one secant step from the paper's own λ⁰ = 200 initialisation lands exactly on the depth `[exact]` | 3 |
 | `HausdorffMetricSym.v : Hsym_triangle` (+ `Hsym_nonneg`, `Hsym_symmetric`, `Hsym_zero_iff`, `vor2_zero_at_sites`, `vor2_nonneg`, `vor2_midpoint_ridge`, `vor2_translation`, `vor2_lipschitz`, `vor2_profile_0_4`, `vor2_nearest_not_farthest`) | **Huttenlocher–Klanderman–Rucklidge (IEEE PAMI 1993) eq (1) is a metric, abstractly:** for ANY directed dissimilarity with nonnegativity, a zero-iff-subshape law and the directed triangle inequality, the symmetrization `max(h(A,B), h(B,A))` has symmetry, the mutual-inclusion zero law, and the triangle inequality — the ranked-model-database guarantee, proved at the layer micro-claim 423-a's Green will instantiate (the discrete max-min itself stays RED on the eval surface by design). Plus the 1D two-site Voronoi surface pinned: zeros at sites, midpoint ridge at half separation, translation covariance (the `H(A,B⊕t)` machinery), 1-Lipschitz cone (the §IV half-pixel rasterization seed), rational egg-carton profile for sites {0,4} `[exact]` | 3 |

oracle/Makefile

@@ -59,6 +59,10 @@ arc-arc-tests: $(TARGET)
 i-circular-tests: $(TARGET)
 	cd .. && python3 oracle/gen_i_circular_tests.py
 
+# Extracted q_ddh_sq / q_hsymm_sq (HAUSDORFF_DIRECTED / HAUSDORFF_SYMM, #423 t10 line 2).
+hausdorff-tests: $(TARGET)
+	cd .. && python3 oracle/gen_hausdorff_tests.py
+
 # IEEE↔R bridge (claimId 0007-ieee-oracle-bridge): existing keywords only
 # (INTERSECT_FILTERED / INTERSECT_POINT_XY / OVERLAY_UNIFIED / ORIENT).
 # Gates NodingNG Hit/Empty + OverlayNG/RelateNG 67-c parallel chords.