letter: GeodesicString as sheet geodesic (claimId 0007-intake-geodesic) - #744
Merged
Merged
Conversation
cursor
Bot
changed the title
…sic) Change μ, not another map of names. Well-formed TGeodesicString pts returns IntakeBag (map_ls S pts) — same hens and MkChord chickens as LineString. ID_GeodesicString is not the well-formed answer. Spiral still Declines. One signed-tag agreement row: τ is LINESTRING, cst_prod_tag stays None. No TagGeodesic; κ does not gain 13. Breaking: TGeodesicString now carries list Point (was a unit ctor). This PR was drafted with AI assistance. Co-authored-by: Jeroen Bloemscheer <grootstebozewolf@users.noreply.github.com>
…lines Well-formed GEODESICSTRING is 0007-intake-geodesic. Do not remint 0007-intake-walker. This PR was drafted with AI assistance. Co-authored-by: Jeroen Bloemscheer <grootstebozewolf@users.noreply.github.com>
Compress the geodesic letter so μ stays in this file without crossing the monolith threshold. This PR was drafted with AI assistance. Co-authored-by: Jeroen Bloemscheer <grootstebozewolf@users.noreply.github.com>
μ(S, TGeodesicString pts) = μ(S, TLineString pts). Eggs are MkChord only. γ_ch joints, τ=LINESTRING, π(G)=GEODESICSTRING ∉ T_signed. Consecutive eggs already first_cook_scope. Companion IntakeGeodesic.v keeps IntakeWalker under the module-split gate. This PR was drafted with AI assistance. Co-authored-by: Jeroen Bloemscheer <grootstebozewolf@users.noreply.github.com>
cursor
Bot
force-pushed
the
cursor/intake-geodesic-mkchord-62c0
branch
from
September 13, 2026 09:11
fbe00ce to
995ee9c
Compare
grootstebozewolf
changed the base branch from
cursor/sqlmm-tau-mu-kinks-62c0
to
main
September 13, 2026 09:14
Empty commit so GitHub Actions sees a synchronize event now that the pull request base is main (workflows only run for PRs targeting main). Rebase itself was already force-pushed at 995ee9c. This commit was drafted with AI assistance. Co-authored-by: Jeroen Bloemscheer <grootstebozewolf@users.noreply.github.com>
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.
Based on main after #743 merge (
cst_prod_tag). Rebased the geodesic letter off the stackedcursor/sqlmm-tau-mu-kinks-62c0tip ontoorigin/main. New claimId0007-intake-geodesic. Does not remint0007-sqlmm-signed-tagor0007-intake-walker. Does not touch #729,SheetHenCook.v, orSidecarGeodesicEgg.vcook story.This letter changes μ, not another map of names. A well-formed GeodesicString tagged CST becomes an SHC bag of
MkChordon sheet (S), the same bag family as LineString.μ (
IntakeWalker.v).TGeodesicStringnow carrieslist Point(breaking vs the unit ctor in letter: τ=μ on locked singleton CSTs (claimId 0007-sqlmm-signed-tag) #742/letter: fold geodesic+spiral and iron CST τ=μ kinks (0007-sqlmm-signed-tag) #743).intake_map S (TGeodesicString pts)for (n\ge 2) returnsIntakeBag (map_ls S pts)— same hens,chords_of_pts,MkChordchickens.ID_Empty/ID_BadPointCount(same as LineString).ID_GeodesicStringis not the well-formed answer.locked_geodesic_cstuses the same controls aslocked_ls_cst; μ of both is the same bag. One production (OGC≡ISO is trivial).TSpiralCurve/TOutOfSlicestill Decline. No spiral fold-in.MkGeodesic. Successful chickens areMkChord.MkOutOfScope EggGeodesicStringstays sidecar packaging.τ row (
SqlMmSignedTag.v, no new ticket zoo).TagGeodesic. HOLD 13 stays a nat.κdoes not gain 13 (kappa_not_13).tau_mu_locked_geodesic: μ bags[MkChord],first_slice_tag e = Some TagLineString,cst_prod_tag locked_geodesic_cst = None.Qed.
intake_map default_sheet locked_geodesic_cst = IntakeBag _bag_eggs/ chickens areMkChordonlyfirst_slice_tagisSome TagLineStringTSpiralCurvestill DeclinesQEX (named). Ellipsoid geodesic γ; WKB 13 as signed I/O; emit of GEODESICSTRING bytes; τ=π on the geodesic production.
Not this letter: first-cook expand, emit / JTS #7 /
tools/visitor (still Declines GEODESICSTRING — next repo rung), oracle keyword, park ρ / ι / CircGamma.This PR was drafted with AI assistance. Rebase onto main was also AI-assisted.