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

[grootstebozewolf]

Follow-up after #742 (a9317df / f750b95 line). Reuses claimId 0007-sqlmm-signed-tag. Does not remint #472. Does not touch #729.

Achievable ring stays locked exists b e agreement lemmas — not ∀ on all CSTs.

Kinks.

1. GeodesicString + Spiral fold-in. tau_mu_geodesic_decline keeps Decline + intake_rho TGeodesicString _ = None. Spiral now mirrors both. first_slice_tag (MkOutOfScope EggGeodesicString) = None and EggSpiralCurve. Both Declines sit in the QED arm of ticket_sqlmm_tau_mu_qed_or_qex.

2. Honest QEX arm. The right-hand side is no longer “τ of the locked full egg is CIRCULARSTRING” (already impossible). It is production-level τ=π on full-span CIRCULARSTRING text:

   sqlmm_prod_tag_fullspan_cs_text / sqlmm_tau_eq_pi_fullspan_cs_missing via cst_prod_tag (CST constructor name, no egg read). intake_rho stays egg-aware on CS and is not cst_prod_tag.

3. ρ naming. intake_rho / cst_prod_tag here are the CST production tag in τ=μ. They are not ADR-0007 park ρ (EmitRhoBagLoop / bag-loop).

4. TCircle intake_rho ignores the egg. Always Some TagCircle. A hypothetical non-full MkCirc under TCircle would give ρ=CIRCLE and τ=CIRCULARSTRING; first slice does not inhabit that bag; the function still allows it.

5. ang_egg is definitional full-span. Rabs (circ_sweep ang_egg) = 2 * PI because ang_egg is mkCircularEgg _ _ _ (2*PI) in IntakeAngles — same policy as the OGC full-span CS clash, not a fixture accident.

Qed. ticket_sqlmm_tau_mu_qed_or_qex left arm: locked exists ring + geodesic/spiral Decline.

QEX. Right arm: sqlmm_prod_tag_fullspan_cs_text (production τ=π). Emit ticket unchanged.

New / changed names.

• New: cst_prod_tag, cst_prod_tag_circularstring, cst_prod_tag_circle, cst_prod_tag_fullspan_cs, intake_rho_tcircle_ignores_egg, intake_rho_tcircle_always_circle, intake_rho_egg_aware_on_fullspan_cs, first_slice_tag_geodesic_none, first_slice_tag_spiral_none, ang_egg_sweep_is_two_pi, sqlmm_prod_tag_fullspan_cs_text, sqlmm_tau_eq_pi_fullspan_cs_missing
• Changed: tau_mu_geodesic_decline, tau_mu_spiral_decline, tau_mu_unknown_cs, ticket_sqlmm_tau_mu_qed_or_qex

Verify. make ci-guards OK. make host OK (SqlMmSignedTag.vo). Print Assumptions on the new lemmas: Closed under the global context, or the three host classical-reals axioms only.

Fences: no ∀ mapper, no emit/ANTLR/factory hex, no CC as τ, no first-cook expand / NURBS / Java twin / park-ρ Discharge. Sidecar only.

This PR was drafted with AI assistance. Do not merge.

  

[grootstebozewolf]

Score vs CST re-pitch kinks — tip 6f92a30

Pass.

Kink	Fix
GeodesicString fold	Decline + intake_rho=None + first_slice_tag MkOutOfScope EggGeodesicString = None; Spiral mirrored; both in ticket QED
Wrong QEX arm	Now sqlmm_prod_tag_fullspan_cs_text via cst_prod_tag (CST name, no egg) — production τ=π park, not τ xor
intake_rho vs park ρ	Header + CONTEXT: CST production tag ≠ EmitRhoBagLoop
TCircle ρ ignores egg	intake_rho_tcircle_ignores_egg / _always_circle
unknown_cs / ang_egg	ang_egg_sweep_is_two_pi — definitional full-span
Still locked-exists	Explicitly not ∀

CI green. Do not merge from courier — awaiting go.