theories: #423 ticket-10 line 1 — discrete ≤ locus Hausdorff and the densify-step bound

[grootstebozewolf]

#423 ticket-10 line 1 only: the discrete-vs-locus densification bound. theories/HausdorffDensify.v, claimId 423-t10-densify.

Two values, both terms

• directed_discrete_h A B = max_{a vertex of A} d(a, locus B) — JTS DiscreteHausdorffDistance's h: vertices of A against the whole geometry B (point-to-segment via LECSegmentRow.seg_dist). This is not the 423-a value (HausdorffDiscrete.directed_hausdorff_sq, vertex-to-vertex, squared); 423-a is not restated.
• directed_locus_h A B = sup_{q on locus A} d(q, locus B) — the JTS DirectedHausdorffDistance locus value, built as a real number with Stdlib completeness (bounded by discrete + max edge length via the 1-Lipschitz property; nonempty via a vertex).

Proved (unsquared dist, 3-axiom Reals, no classic)

	Lemma
discrete ≤ locus on any polyline with an edge	discrete_le_locus
densify step: same locus, every edge ≤ δ ⇒ 0 <= locus(A,B) - discrete(A',B) <= δ	densify_step_bound, densify_step_bound_max_edge
locked JTS pair (0 0, 100 0, 10 100) vs (0 100, 0 10, 80 10): discrete = √500 (22.36)	jts_discrete_value
locus ≥ 910/19 (47.89), witness (910/19, 1100/19) on the diagonal edge	jts_locus_lower
√500 < 910/19: the vertex value is a strict under-estimate on this pair	jts_discrete_strictly_below_locus
ticket stop	ticket_423_t10_line1_qed_or_qex (QED arm)

f(δ) = δ: distance-to-a-set is 1-Lipschitz, so a δ-fine refinement closes the gap linearly. This is the polyline twin of ArcChordDensity.n_chords_achieve_eps (arc side, quadratic in the refinement), quoted in the header, not remade. Equality locus = 910/19 on the pair is not claimed; only the lower bound and the strict gap are.

Hard-no honoured

No 423-a / 423-b / FrechetMaxmin remint; no HAUSDORFF_* keyword (line 2 is next); no NTS/GEOS port; no CurveSegment growth; no first_cook_scope; Linearise.hausdorff_le is not used.

Ledger

Registered in _CoqProject.full after LECSegmentRow.v; counts 635 / 544; verified-claims 423-a row extended in place; TRIAGE_NTS_JTS_ISSUES.md #423 entry and docs/scout/map-hausdorff-functions.md remaining-ask row amended in place (line 1 landed, line 2 remains). make ci-guards all pass.

AI-drafted, human-reviewed.
Assisted-by: Claude

🤖 Generated with Claude Code

https://claude.ai/code/session_01RLRSgKZrz5hV2dsf44PADc

---

Generated by Claude Code

[grootstebozewolf]

Review (cannot APPROVE: same account as the author). Approve-shaped on the letter; merge-order issue with #791.

Line 1 is the right slice. directed_discrete_h is vertices-against-locus (JTS DiscreteHausdorffDistance, unsquared, seg_dist), not 423-a vertex-to-vertex squared. directed_locus_h is a term via Stdlib completeness (3-axiom Reals, not classic). densify_step_bound is 0 ≤ locus − discrete(A') ≤ δ under same-locus + max-edge ≤ δ. f(δ)=δ from 1-Lipschitz. JTS pair pins discrete=√500 and locus ≥ 910/19 with a strict gap; equality of the locus value is not claimed. Line 2 (HAUSDORFF_*) stays open. Linearise.hausdorff_le unused. Hard-nos held.

ring_edges here is the open consecutive chain (2-point list = one edge, no last→first wrap). That is the right carrier for the JTS LINESTRINGs.

CI: all four checks green. mergeable_state: clean vs dd46260.

Do not merge both #791 and #792 without a count rebase. Both bump 634→635 / 543→544. Second one to land must bump 636 / 545.

Do not claim. Ticket 10 is not closed. #423 is not closed. Locus h is not computed exactly on the pair. NTS#812 is not ported.

Nits. dist_to_edges [] = 0 and list_max [] = 0 are dummy zeros; every theorem that matters guards ring_edges _ <> []. Keep it that way. TRIAGE “Green” on line 1 is fine if line 2 stays named remaining.

[grootstebozewolf]

Acknowledged. Merge order: #791 lands first (your review there authorised it); this PR then gets rebased onto main with counts bumped to 636 / 545 before anything else happens to it. No merge here without your word.

Nits kept as is: dist_to_edges [] = 0 and list_max [] = 0 stay dummy zeros and every theorem that matters keeps the ring_edges _ <> [] guard. Not claimed: ticket 10 closed, #423 closed, exact locus value on the pair, NTS#812 ported. Line 2 (HAUSDORFF_*) stays named remaining in TRIAGE.

---

Generated by Claude Code

[grootstebozewolf]

COMMENT (same-account; cannot APPROVE).

Standards: new theories/HausdorffDensify.v; count bump expected; CI must be green after rebase on #793.

Spec / honesty: #423 ticket-10 line 1 only — discrete ≤ locus + densify-step bound; JTS pair √500 < locus lower. Explicitly leaves line 2 (HAUSDORFF_*) and does not close #423.

Merge: squash when CLEAN after update-branch.

[grootstebozewolf]

Squash-merged: #423 ticket-10 line 1 only (discrete ≤ locus + densify bound). Line 2 / HAUSDORFF_* still open; #423 not closed.