Merge pull request #743 from grootstebozewolf/cursor/sqlmm-tau-mu-kinks-62c0

letter: fold geodesic+spiral and iron CST τ=μ kinks (0007-sqlmm-signed-tag)

Author: grootstebozewolf

CONTEXT.md

@@ -115,13 +115,19 @@ _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
+Rungs 3–6 of τ=μ. Achievable ring is locked `exists b e`
+agreement (not ∀ on all CSTs). `τ = first_slice_tag` on eggs;
+`μ = intake_map` on CSTs. They do not share a domain. After μ
+mints a singleton bag, `τ(e)=ρ(π(c))`. `intake_rho` /
+`cst_prod_tag` here are the CST production tag in that equation
+— not ADR-0007 park ρ (`EmitRhoBagLoop` / bag-loop). Full-span
+CS and CIRCLE share one MkCirc; τ of that egg is CIRCLE.
+`intake_rho` is egg-aware on CIRCULARSTRING and is not
+`cst_prod_tag`. GeodesicString / SpiralCurve Decline (τ unused).
+`κ` is 2/8 or none. Emit / WKT parse stay QEX. Production-level
+τ=π on full-span CIRCULARSTRING text stays QEX.
+_Avoid_: ∀-mapper on all CSTs, Circle-as-18, compound-as-τ,
+park-ρ remint, new oracle keyword
 
 **ISO validity**:
 Every spec "shall" beyond representability, owned by arc-aware `ST_IsValid`:

docs/verified-claims.md

@@ -992,7 +992,7 @@ 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.
+**SQL/MM signed tag** (own paragraph; claimId `0007-sqlmm-signed-tag`, witness `0007-sqlmm-signed-tag`). Rungs 3–6 of τ=μ. Achievable ring is locked `exists b e` agreement, not ∀ on all CSTs. `τ` 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`; `SqlMmSignedTag.v : ang_egg_sweep_is_two_pi`). Full-span CIRCULARSTRING and CIRCLE share one `MkCirc`; τ of that egg is CIRCLE. `intake_rho` / `cst_prod_tag` are the CST production tag in τ=μ, not ADR-0007 park ρ (`SqlMmSignedTag.v : cst_prod_tag`; `SqlMmSignedTag.v : intake_rho_egg_aware_on_fullspan_cs`; `SqlMmSignedTag.v : sqlmm_tau_eq_pi_fullspan_cs_missing`). `intake_rho` is egg-aware on CS and is not `cst_prod_tag`. TCircle `intake_rho` ignores the egg (`SqlMmSignedTag.v : intake_rho_tcircle_ignores_egg`; `SqlMmSignedTag.v : intake_rho_tcircle_always_circle`). Geodesic + spiral Decline, `intake_rho = None`, `first_slice_tag` none; compound is not a singleton (`SqlMmSignedTag.v : tau_mu_geodesic_decline`; `SqlMmSignedTag.v : tau_mu_spiral_decline`; `SqlMmSignedTag.v : first_slice_tag_geodesic_none`; `SqlMmSignedTag.v : first_slice_tag_spiral_none`; `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`). Production-level τ=π on full-span CIRCULARSTRING text stays QEX (`SqlMmSignedTag.v : sqlmm_prod_tag_fullspan_cs_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 Γ / ι / ρ.