letter: τ=μ on locked singleton CSTs (claimId 0007-sqlmm-signed-tag) (#742)

* docs: north star SQL/MM Part 3 example oracle (JTS #7)

claimId: none (docs / packaging). Destination document, not a letter.
#740 (cloth_joint) is already on main. ADR-0006/0007 stay Accepted.

This PR was drafted with AI assistance.

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

* letter: SQL/MM signed tag sidecar (claimId 0007-sqlmm-signed-tag)

Qed: first-slice host eggs inhabit a signed §5.1.67/Table 15 tag;
HOLD codes 13-17 and 18-21 do not. CIRCLE is full-span MkCirc, not
WKB 18. CLOTHOID is one egg for both surface forms. COMPOUNDCURVE
only when eval A 1 = eval B 0 (reuses cloth_joint / circ_split).

QEX: factory WKT/WKB emit. Rocq does not inhabit byte strings.
No new oracle keyword. SheetHenCook.v is not grown.

Removes the north-star markdown (#742 docs view). Not a remint of
0007-intake-walker / 0007-clothoid-first-cook / 0007-gamma-mkcirc.

This PR was drafted with AI assistance.

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

* fix: prove PI/2 ≠ ±2π without lra on opaque PI

locked_quarter_not_full failed CI (lra: Cannot find witness).
Use field/ring plus PI_RGT_0. Mode D LS+CS joint now reuses
chord_eval_at_1.

This PR was drafted with AI assistance.

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

* fix: field-algebra for PI/2 ≠ ±2π (avoid Rmult_0_r)

CI failed rewriting r*0 in 3*PI = 3*0. Derive PI=0 from the
assumed equality, then Rlt_irrefl against PI_RGT_0.

This PR was drafted with AI assistance.

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

* fix: order-field proofs that PI/2 ≠ ±2π

transitivity was matching <> (not =). Compare PI/2 < PI < 2π
and −2π < 0 < PI/2 via Rmult_lt_compat / Rlt_not_eq.

This PR was drafted with AI assistance.

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

* letter: first_slice_tag is a function, not a sticker sheet

HostEggInhabits collapsed to first_slice_tag:
  MkChord → LINESTRING (2); every MkCirc → CIRCULARSTRING (8);
  MkClothoid / MkOutOfScope → None. CIRCLE CST is the same MkCirc
  (intake ogc_iso_circle_same_egg), not a second tag.

SqlMmTag is codes 1–12 only. HOLD is nats 13–21, no named
constructors. COMPOUNDCURVE is a bag, not an egg tag. Mode D
reuses cloth_joint and circ_split_join; do not remint
cs_joint_circ. Emit stays QEX.

Kills: dual inhabit, CIRCLE/CLOTHOID in signed I/O, tag_of_wkb
13/14/20 fanfic, π-lemmas, local cs_joint_circ, LS→CS mint.

This PR was drafted with AI assistance.

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

* fix: prove signed/HOLD nat bounds without lia under R_scope

wkb_code_is_signed failed CI (lia: Cannot find witness) because
Local Open Scope R_scope poisoned the nat lemmas. Drop the global
real scope; use PeanoNat (leb_le / le_ngt / le_succ_l) for 1–12
vs 13–21. circ_eval arguments are 1%R / 0%R.

This PR was drafted with AI assistance.

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

* fix: Nat.le_ngt is an iff, not a lemma arrow

CI: Illegal application — Nat.le_ngt n 12 has type
(n <= 12) <-> ~ (12 < n). Use proj1/proj2 wrappers
(leb_true_le / le_leb_true) instead of apply-on-iff.

This PR was drafted with AI assistance.

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

* letter: rung 3 is τ and κ, not an inhabit relation

T_signed = {LINESTRING, CIRCULARSTRING, CIRCLE, CLOTHOID}.
τ(MkChord)=LINESTRING; τ(MkCirc)=CIRCLE iff |sweep|=2π else
CIRCULARSTRING; τ(MkClothoid)=CLOTHOID; τ(MkOutOfScope)
undefined. Unique. Locked quarter/full/cloth/chord evaluate.
κ is 2/8 or none (CIRCLE ≠ 18). HOLD stays nats. Emit QEX.

This PR was drafted with AI assistance.

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

* letter: τ=μ after IntakeWalker mints a singleton egg

Require the mapper. ρ sends locked CST productions to T_signed;
τ of the minted egg agrees. Full-span CIRCULARSTRING and CIRCLE
share one MkCirc; that egg is CIRCLE. Clothoid ISO≡JTS. Unknown
CS (ang_egg) is CIRCLE by sweep. Geodesic Decline. Compound is
two eggs, not a singleton τ. WKT parse stays QEX.

This PR was drafted with AI assistance.

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

---------

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

Author: grootstebozewolf

CONTEXT.md

@@ -114,6 +114,15 @@ Not Fresnel-as-noding. Not a silent `I_ok` demote to `on_chord`.
 _Avoid_: Fresnel noding, Halley noding, mixed first cook, NURBS
 first cook, Campaign I, new oracle keyword
 
+**SQL/MM signed tag** (ADR-0007, claimId `0007-sqlmm-signed-tag`):
+Rungs 3–6 of τ=μ. `τ = first_slice_tag` on eggs; `μ = intake_map`
+on CSTs. They do not share a domain. After μ mints a singleton
+bag, `τ(e)=ρ(π(c))`. Full-span CS and CIRCLE share one MkCirc;
+τ of that egg is CIRCLE. `κ` is 2/8 or none. Emit / WKT parse
+stay QEX.
+_Avoid_: τ=π on full-span CIRCULARSTRING text, Circle-as-18,
+compound-as-τ, new oracle keyword
+
 **ISO validity**:
 Every spec "shall" beyond representability, owned by arc-aware `ST_IsValid`:
 implemented rules answer definite-false naming their clause; unimplemented
@@ -603,4 +612,4 @@ _Avoid_: self-intersection (narrower), retrace (one kind of overshoot)
 
 ## ADR-0007 Accepted
 
-ADR-0007 (sheet/hen/cook) **Accepted** 2026-09-07 by Joost (BDFL). Soft gaps closed. Parks ι / ρ remain landed named QEX. Γ CircGamma is discharged by host MkCirc (claimId `0007-gamma-mkcirc`; `CircularCook.v : circular_gamma_is_discharged`). NodingNG chord is the cook product face (`theories/NodingNG.v`): 𝓘 + one cook step on one sheet; ρ stays obligation. OverlayNG sheet is the snap product face (`theories/OverlayNG.v`): finite snap-sequence ≠ `𝓘` on one sheet; Hobby 4.1 stays Honest remaining. RelateNG face is the DE-9IM product face (`theories/RelateNGFace.v`): matrix/witness + honesty decline + 67-c pin; completeness / Jordan / S15l+ / 523 `?` stay named QEX. IEEE↔R bridge is the Oracle test-surface face (`theories-flocq/IeeeRBridge.v`): two-way binary64 ↔ ℝ under the int-safe regime; FP noder / unrestricted / kiss stay Honest remaining. Clothoid egg sidecar is the cook-axis EggClass face (`theories/SidecarClothoidEgg.v`): tag-Decline + RelateClothoid chord-seed; clothoid×clothoid first cook is QED (`theories/ClothoidCookMkClothoid.v`, claimId `0007-clothoid-first-cook`). NURBS egg sidecar is the next cook-axis EggClass face (`theories/SidecarNurbsEgg.v`): Decline-on-host + demoted unit-square chord-seed; NURBS×NURBS stays QEX; #508 length stays metric. Sinusoid (SIN) egg sidecar is the next cook-axis EggClass face (`theories/SidecarSinEgg.v`): Decline-on-host + demoted unit-square chord-seed; sinusoid×sinusoid stays QEX; thin Spectre profile corpus stays research, not cook. Circle / circular egg sidecar is the next cook-axis EggClass face (`theories/SidecarCircEgg.v`): packages host EggCircularArc tag-Decline + demoted unit-square chord-seed; host circular cook is MkCirc (`theories/CircularCookMkCirc.v`), not this sidecar. Elliptical Curve / EllipticArc egg sidecar is the next cook-axis EggClass face (`theories/SidecarEllipticEgg.v`): Decline-on-host + RelateEllipticArc chord-seed; ellipse×ellipse stays QEX; #508 ellipse length / elliptic-E stay metric. SQL/MM GeodesicString egg sidecar is the next cook-axis EggClass face (`theories/SidecarGeodesicEgg.v`): Decline-on-host + demoted unit-square chord-seed; geodesic×geodesic stays QEX; type-zoo packaging (MkOutOfScope), not Γ progress. SQL/MM ST_SpiralCurve egg sidecar is the last Lesson-1 cook-axis EggClass face (`theories/SidecarSpiralEgg.v`): Decline-on-host + demoted unit-square chord-seed; five ISO names + Unknown on one egg; `EggClothoid` stays; spiral×spiral stays QEX; type-zoo packaging (MkOutOfScope), not Γ / not 𝓘 progress. ι interior Hit discharge is the sidecar circular×chord face (`theories/SidecarCircInteriorHit.v`): distinct `I_ok_interior` Hit; `I_ok_mixed` joint gate stands. Intake walker is the first-slice WKT → CST → SHC bag seam (`theories/IntakeWalker.v`, claimId `0007-intake-walker`): grammar pin grammars-v4 #4997; Intake Decline ≠ cook Decline; no silent chord demote. Intake angles is the CircUnknown construction (`theories/IntakeAngles.v`, claimId `0007-intake-angles`): unique circumcircle + inhabited angle fields → `MkCirc`; collinear / duplicate / bad count Decline by name; not a CircGamma remint. Intake MkClothoid is the host clothoid constructor (`theories/SheetHenClothoidEgg.v`, claimId `0007-intake-mkclothoid`): one `MkClothoid` on `Egg`; ISO and JTS clothoid bag the same locked egg. Clothoid first-cook is the Hit letter (`theories/ClothoidCookMkClothoid.v`, claimId `0007-clothoid-first-cook`). See `docs/adr/ADR-0007-sheet-hen-cook-noding-model.md`. CRV-TOUCH assumes this vocabulary; kiss/FP noder remain on that map.
+ADR-0007 (sheet/hen/cook) **Accepted** 2026-09-07 by Joost (BDFL). Soft gaps closed. Parks ι / ρ remain landed named QEX. Γ CircGamma is discharged by host MkCirc (claimId `0007-gamma-mkcirc`; `CircularCook.v : circular_gamma_is_discharged`). NodingNG chord is the cook product face (`theories/NodingNG.v`): 𝓘 + one cook step on one sheet; ρ stays obligation. OverlayNG sheet is the snap product face (`theories/OverlayNG.v`): finite snap-sequence ≠ `𝓘` on one sheet; Hobby 4.1 stays Honest remaining. RelateNG face is the DE-9IM product face (`theories/RelateNGFace.v`): matrix/witness + honesty decline + 67-c pin; completeness / Jordan / S15l+ / 523 `?` stay named QEX. IEEE↔R bridge is the Oracle test-surface face (`theories-flocq/IeeeRBridge.v`): two-way binary64 ↔ ℝ under the int-safe regime; FP noder / unrestricted / kiss stay Honest remaining. Clothoid egg sidecar is the cook-axis EggClass face (`theories/SidecarClothoidEgg.v`): tag-Decline + RelateClothoid chord-seed; clothoid×clothoid first cook is QED (`theories/ClothoidCookMkClothoid.v`, claimId `0007-clothoid-first-cook`). NURBS egg sidecar is the next cook-axis EggClass face (`theories/SidecarNurbsEgg.v`): Decline-on-host + demoted unit-square chord-seed; NURBS×NURBS stays QEX; #508 length stays metric. Sinusoid (SIN) egg sidecar is the next cook-axis EggClass face (`theories/SidecarSinEgg.v`): Decline-on-host + demoted unit-square chord-seed; sinusoid×sinusoid stays QEX; thin Spectre profile corpus stays research, not cook. Circle / circular egg sidecar is the next cook-axis EggClass face (`theories/SidecarCircEgg.v`): packages host EggCircularArc tag-Decline + demoted unit-square chord-seed; host circular cook is MkCirc (`theories/CircularCookMkCirc.v`), not this sidecar. Elliptical Curve / EllipticArc egg sidecar is the next cook-axis EggClass face (`theories/SidecarEllipticEgg.v`): Decline-on-host + RelateEllipticArc chord-seed; ellipse×ellipse stays QEX; #508 ellipse length / elliptic-E stay metric. SQL/MM GeodesicString egg sidecar is the next cook-axis EggClass face (`theories/SidecarGeodesicEgg.v`): Decline-on-host + demoted unit-square chord-seed; geodesic×geodesic stays QEX; type-zoo packaging (MkOutOfScope), not Γ progress. SQL/MM ST_SpiralCurve egg sidecar is the last Lesson-1 cook-axis EggClass face (`theories/SidecarSpiralEgg.v`): Decline-on-host + demoted unit-square chord-seed; five ISO names + Unknown on one egg; `EggClothoid` stays; spiral×spiral stays QEX; type-zoo packaging (MkOutOfScope), not Γ / not 𝓘 progress. ι interior Hit discharge is the sidecar circular×chord face (`theories/SidecarCircInteriorHit.v`): distinct `I_ok_interior` Hit; `I_ok_mixed` joint gate stands. Intake walker is the first-slice WKT → CST → SHC bag seam (`theories/IntakeWalker.v`, claimId `0007-intake-walker`): grammar pin grammars-v4 #4997; Intake Decline ≠ cook Decline; no silent chord demote. Intake angles is the CircUnknown construction (`theories/IntakeAngles.v`, claimId `0007-intake-angles`): unique circumcircle + inhabited angle fields → `MkCirc`; collinear / duplicate / bad count Decline by name; not a CircGamma remint. Intake MkClothoid is the host clothoid constructor (`theories/SheetHenClothoidEgg.v`, claimId `0007-intake-mkclothoid`): one `MkClothoid` on `Egg`; ISO and JTS clothoid bag the same locked egg. Clothoid first-cook is the Hit letter (`theories/ClothoidCookMkClothoid.v`, claimId `0007-clothoid-first-cook`). SQL/MM signed tag is the rung-3 pair of maps (`theories/SqlMmSignedTag.v`, claimId `0007-sqlmm-signed-tag`): τ sends MkChord/MkCirc/MkClothoid to LINESTRING / (CIRCLE iff |sweep|=2π else CIRCULARSTRING) / CLOTHOID and is undefined on MkOutOfScope; κ is 2/8 or none (not 18); HOLD is nats; emit stays QEX. See `docs/adr/ADR-0007-sheet-hen-cook-noding-model.md`. CRV-TOUCH assumes this vocabulary; kiss/FP noder remain on that map.

_CoqProject

@@ -173,6 +173,12 @@ theories/IntakeAngles.v
 # Host/pure-R. Grammar pin: grammars-v4 #4997. No new oracle
 # keyword. No Admitted.
 theories/IntakeWalker.v
+# ADR-0007 SQL/MM signed tag maps (SqlMmSignedTag).
+# τ on eggs; ρ on IntakeWalker productions; τ=μ after
+# singleton bags. CIRCLE iff |sweep|=2π. κ: 2/8 or none.
+# HOLD is nats. Emit / WKT parse QEX. Does not grow
+# SheetHenCook. No new oracle keyword. No Admitted.
+theories/SqlMmSignedTag.v
 # RelateNG product face lives in _CoqProject.full (RelateNGFace.v):
 # it packages the DE-9IM / RelateNG zoo, which is not host-lane.
 # Integer circle–circle discriminant + hen mint (I_circles_z). 0-axiom.

_CoqProject.full

@@ -2895,6 +2895,12 @@ theories/IntakeAngles.v
 # Host/pure-R. Grammar pin: grammars-v4 #4997. No new oracle
 # keyword. No Admitted.
 theories/IntakeWalker.v
+# ADR-0007 SQL/MM signed tag maps (SqlMmSignedTag).
+# τ on eggs; ρ on IntakeWalker productions; τ=μ after
+# singleton bags. CIRCLE iff |sweep|=2π. κ: 2/8 or none.
+# HOLD is nats. Emit / WKT parse QEX. Does not grow
+# SheetHenCook. No new oracle keyword. No Admitted.
+theories/SqlMmSignedTag.v
 # Integer circle–circle discriminant + hen mint (I_circles_z). 0-axiom.
 theories/CircularCookZ.v
 # R-side p* attach. QEX: no γ:[0,1]. Classical reals.

docs/verified-claims.md

@@ -992,6 +992,8 @@ Skeletons + helpers + guarded dim soundness landed. Rect + triangle helpers + EE
 
 **Clothoid first-cook** (own paragraph; claimId `0007-clothoid-first-cook`, witness `0007-clothoid-first-cook`). Host first cook includes `EggClothoid × EggClothoid` (`SheetHenCook.v : clothoid_egg_first_cook_scope`; `ClothoidCookMkClothoid.v : interpolant_pair_mkclothoid`). Locked crossing `MkClothoid` pair inhabits host `IHit` via `on_cloth` (`ClothoidCookMkClothoid.v : locked_mkclothoid_I_ok`); `try_cook_hit` mints `MkClothoid` hens (`ClothoidCookMkClothoid.v : cooked_mkclothoid_try`; `ClothoidCookMkClothoid.v : cooked_mkclothoid_children_are_clothoid`; `ClothoidCookMkClothoid.v : ticket_0007_clothoid_first_cook_qed_or_qex`). Closed-form small-angle interpolant (`cos θ≈1`, `sin θ≈θ`) — not Fresnel, not chord-parameter, not Fresnel-as-noding and not a silent `I_ok` demote to `on_chord`. Tags stay Decline (`ClothoidCookMkClothoid.v : mkclothoid_tag_still_decline`; `SheetHenCook.v : clothoid_decline_I_ok`). Mixed clothoid×chord stays Decline (`ClothoidCookMkClothoid.v : mkclothoid_mixed_still_decline`; `ClothoidCookMkClothoid.v : clothoid_chord_not_first_cook_scope`). NURBS / SIN / ellipse / spiral / geodesic stay out of first cook. ρ / Campaign stay parked (`SheetHenCook.v : cook_loop_is_obligation`). No new oracle keyword (ADR-0006). ADR-0007 stays Accepted.
 
+**SQL/MM signed tag** (own paragraph; claimId `0007-sqlmm-signed-tag`, witness `0007-sqlmm-signed-tag`). Rungs 3–6 of τ=μ. `τ` is a function on eggs (`SqlMmSignedTag.v : first_slice_tag`; `SqlMmSignedTag.v : ticket_sqlmm_signed_tag_qed_or_qex`; `SqlMmSignedTag.v : tau_unique`; `SqlMmSignedTag.v : full_span_is_circle_not_cs`). Egg-level agreement: after `intake_map` mints a singleton bag, `τ(e)=ρ(π(c))` on locked LS / quarter CS / CIRCLE / full-span CS / both clothoid spellings / unknown-CS (`SqlMmSignedTag.v : ticket_sqlmm_tau_mu_qed_or_qex`; `SqlMmSignedTag.v : tau_mu_locked_ls`; `SqlMmSignedTag.v : tau_mu_locked_cs_quarter`; `SqlMmSignedTag.v : tau_mu_locked_circle`; `SqlMmSignedTag.v : tau_mu_locked_cs_full_ogc`; `SqlMmSignedTag.v : tau_mu_full_span_shared_egg`; `SqlMmSignedTag.v : tau_mu_locked_clothoid_iso`; `SqlMmSignedTag.v : tau_mu_locked_clothoid_jts`; `SqlMmSignedTag.v : tau_mu_unknown_cs`). Full-span CIRCULARSTRING and CIRCLE share one `MkCirc`; τ of that egg is CIRCLE. Geodesic Decline; compound is not a singleton (`SqlMmSignedTag.v : tau_mu_geodesic_decline`; `SqlMmSignedTag.v : tau_mu_compound_not_singleton`). `κ` is 2/8 or none, not 18 (`SqlMmSignedTag.v : sqlmm_kappa`; `SqlMmSignedTag.v : kappa_circle_not_18`; `SqlMmSignedTag.v : signed_code_not_hold`). Emit / WKT parse stay QEX (`SqlMmSignedTag.v : ticket_sqlmm_factory_emit_qed_or_qex`; `SqlMmSignedTag.v : sqlmm_wkt_emit_missing`). Not τ=π on full-span CIRCULARSTRING text. ADR-0006 stays Accepted. ADR-0007 stays Accepted.
+
 **Spiral egg sidecar** (own paragraph; claimId `0007-spiral-egg`, witness `0007-spiral-egg`). Product / sidecar face of `EggSpiralCurve` on the ADR-0007 vocabulary (`SidecarSpiralEgg.v : sidecar_spiral_is_egg_packaging`; `SidecarSpiralEgg.v : ticket_0007_spiral_egg_qed_or_qex`; `SidecarSpiralEgg.v : sidecar_spiral_egg_inhabits`). Host `EggClass` did not have this arm; this letter adds `EggSpiralCurve` / `MkOutOfScope EggSpiralCurve` only. Do not explode `EggClass` into five spiral eggs. No Decline / not-first-cook / try_cook lemmas were added to `SheetHenCook.v` (module-split ceiling after GeodesicString #722); those live on the sidecar and cite existing `first_cook_scope` / `I_ok` (`SidecarSpiralEgg.v : sidecar_spiral_host_decline`; `SidecarSpiralEgg.v : spiral_decline_I_ok`; `SidecarSpiralEgg.v : sidecar_spiral_try_cook_none`; `SidecarSpiralEgg.v : spiral_spiral_not_first_scope`). SQL/MM ISO 13249-3 §4.2.12 five required names (clothoid, bloss, biquadratic, sine, cosine) plus Unknown inhabit one sidecar egg (`SidecarSpiralEgg.v : sidecar_spiral_iso_names_inhabit`; `SidecarSpiralEgg.v : sidecar_spiral_kinds_one_host_egg`). `EggClothoid` / ST_Clothoid stays its own host tag; the clothoid arm is a nameplate, not a remint (`SidecarSpiralEgg.v : egg_clothoid_still_present`; `SidecarSpiralEgg.v : sidecar_spiral_clothoid_nameplate_not_eggclothoid`). Locked unit-square spiral chords reuse `RelateLineLine.v : line_line_proper_cross_geom` (`SidecarSpiralEgg.v : sidecar_spiral_chord_seed`). Demote-to-chord is NodingNG / host first cook, not a spiral Hit (`SidecarSpiralEgg.v : sidecar_spiral_demote_is_nodingng_crossing`; `SidecarSpiralEgg.v : sidecar_spiral_demote_hit_not_spiral_I_ok`). SQL/MM ST_SpiralCurve type-zoo packaging stays packaging, not a cook Hit (`SidecarSpiralEgg.v : sidecar_spiral_metric_is_type_zoo`; `SidecarSpiralEgg.v : sidecar_spiral_metric_not_cook_hit`). Spiral×spiral is not first cook; named missing constructors `MkSpiral` / Hit-arm / first-cook expand (`SidecarSpiralEgg.v : ticket_0007_spiral_not_first_cook_qed_or_qex`; `SidecarSpiralEgg.v : spiral_spiral_not_first_scope`; `SidecarSpiralEgg.v : sidecar_spiral_mkspiral_missing`; `SidecarSpiralEgg.v : sidecar_spiral_hit_arm_missing`). Campaign I–II / spiral-interpolant-as-noding / CircGamma remint / bag loop parked (`SidecarSpiralEgg.v : ticket_0007_spiral_parks_qed_or_qex`; `SidecarSpiralEgg.v : sidecar_spiral_letter_is_landed`; `SheetHenCook.v : cook_loop_is_obligation`). Last Lesson-1 packaging extra. Not Γ. Not 𝓘 progress. Do not remint a spiral interpolant as noding. Do not invent spiral math. Do not remint CircGamma. Do not expand `first_cook_scope`. Do not remint ι / ρ. Do not fold `EggClothoid` away. ADR-0006 stays Accepted. ADR-0007 stays Accepted. Parks Γ / ι / ρ.
 
 **#566 / `508-h` wrap-up** (own paragraph). TRIAGE `M-LEN-ZOO` row, `CONTEXT.md` Metric length sweep, one prose gate (`scripts/validate-claims.sh` over `docs/gated-prose-docs.txt`), and [`docs/scout/508-closing-summary.md`](scout/508-closing-summary.md). Does not remint 508-g theorems. Does not remint `SpeedIntegral.v` / `ClothoidLength_unit.v` / `ClothoidFresnel.v` / `nurbs_knot_span_additive`. Does not close #508. Fresnel inhabitant is a later #564 letter (`ClothoidFresnelInhab.v`); QEX is not owner accept. Witness `508-h-wrap-up`.