letter: τ=μ on locked singleton CSTs (claimId 0007-sqlmm-signed-tag) - #742
Merged
grootstebozewolf merged 10 commits intoSep 13, 2026
Merged
Conversation
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>
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>
cursor
Bot
changed the title
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>
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>
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>
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>
cursor
Bot
changed the title
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>
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>
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>
cursor
Bot
changed the title
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>
cursor
Bot
changed the title
This was referenced Sep 13, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Rungs 3–6 of the τ=μ ladder. Head is
4aa7236. Compiled locally (SqlMmSignedTag.vo) before push.claimId: 0007-sqlmm-signed-tag. Reuses0007-intake-walker/0007-clothoid-first-cook/0007-gamma-mkcirc(does not remint). Sidecar only. Does not growSheetHenCook.v. No new ADR-0006 keyword.τ and μ do not share a domain.
μ = intake_map : TaggedCst × S → IntakeResult.τ = first_slice_tag : Egg ⇀ T_signed. Agreement is after μ mints a singleton bag:μ(c,S)=IntakeBag(b) ∧ eggs(b)=[e] ⇒ τ(e)=ρ(π(c))Locked equalities (rung 4).
locked_ls_cst→ LINESTRINGlocked_cs_quarter_cst→ CIRCULARSTRINGlocked_circle_cst→ CIRCLElocked_cs_full_ogc_cst→ sameMkCircas CIRCLE, tag CIRCLE (production-level τ=π fails here; this is the strongest statement)Plus ISO/JTS clothoid → CLOTHOID (
tau_mu_locked_clothoid_*).Rung 5.
unknown_cs_cst/ang_eggclassified by|sweep|=2π→ CIRCLE.Rung 6.
TGeodesicStringisIntakeDecline; τ is not applied. Compoundlocked_cc_csthas two eggs — not a singleton τ.Qed.
ticket_sqlmm_signed_tag_qed_or_qex(τ, κ).ticket_sqlmm_tau_mu_qed_or_qex(agreement).QEX. emit / ANTLR WKT string / κ as bytes (
ticket_sqlmm_factory_emit_qed_or_qex).Not this letter: τ=π on full-span CIRCULARSTRING text; compound-as-τ; factory hex.
#741 is not this landing and is not closed.
This PR was drafted with AI assistance. Do not merge until go.