letter: famous GEODESICSTRING fixtures (0007-famous-geodesicstring)

[grootstebozewolf]

Lock the two Science / arXiv:1804.07389 (Chabukswar & Mukherjee) endpoints as WKT fixtures on existing μ (0007-intake-geodesic / #744). Fixtures + τ honesty only — not a new cook, not a remint of #744 or tools #745.

This PR was drafted with AI assistance.

Base / tip

• Base: origin/main @ 6d6871843f519406f42059b0b75025e74146e734 (after Chip 2: peel two allowlist-clean files from audit-exceptions #711)
• Tip: 095cdabf28f8471a690d392ad16786695e61c621
• claimId: 0007-famous-geodesicstring (does not remint 0007-intake-geodesic / letter: GeodesicString as sheet geodesic (claimId 0007-intake-geodesic) #744 or tools tools: GEODESICSTRING n≥2 maps to the LineString MkChord bag #745)
• Successor of letter: famous GEODESICSTRING fixtures (0007-famous-geodesicstring) #746 (old tip cd54887 had essay .md that conflicts with ratchet docs: markdown prose ratchet (AGENTS.md + ci-guards) #750). Do not force-merge that tip. letter: famous GEODESICSTRING fixtures (0007-famous-geodesicstring) #746 is closed with a pointer here.
• Await human go. Do not merge.

topics: overlay · witness: 0007-famous-geodesicstring · claimId: 0007-famous-geodesicstring

Cite (PR body only — zero .md diffs)

Rohit Chabukswar and Adwait Kumar Mukherjee, “Longest straight line paths on water or land on the Earth”, arXiv:1804.07389. Science news on the longest ocean / land straight paths. Endpoints locked DMS → decimal lon lat (OGC order).

Zero non-blank .md growth vs origin/main. Dropped from #746: CONTEXT.md, docs/adr/*, docs/attacks/2026-09-13-famous-geodesicstring.md, docs/verified-claims.md, tools/WktIntakeWalker/README.md. Destination + cite + QEX park live here.

Locked WKT

1. Water / sailable: Sonmiani PK → Karaginsky RU
   GEODESICSTRING (66.6666666667 25.2833333333, 162.2333333333 58.6166666667)
2. Land / drivable: Quanzhou CN → Sagres PT
   GEODESICSTRING (118.6333333333 24.55, -8.9166666667 37.0333333333)

QED (this letter)

• Both become tagged CST TGeodesicString pts and μ → IntakeBag with only MkChord chickens — same bag as the matching LINESTRING on those two points.
• Tools smoke (tools/WktIntakeWalker/smoke.ps1): each WKT’s bag-string equals the LineString bag; existing GEODESICSTRING (0 0, 2 0) kept. smoke.sh is archive-only after the tools: .NET hunter for SqlMmExampleFactory vs C# WktIntakeWalker μ #748 C# port; fixture checks reminted onto the live smoke. Exact Java decimal pretty-print is not the letter (C# G17).
• τ honesty: first_slice_tag = Some TagLineString; cst_prod_tag = None; no TagGeodesic; κ does not gain 13.
• Empty / singleton still ID_Empty / ID_BadPointCount; spiral still Decline.
• claimId 0007-famous-geodesicstring / ticket / WITNESS / Print Assumptions; no Axiom / Parameter / deferred stub.
• Lemmas in theories/IntakeFamousGeodesic.v: ticket_0007_famous_geodesicstring_qed_or_qex, famous_water_same_bag_as_ls, famous_land_same_bag_as_ls, famous_water_tau, famous_land_tau, famous_no_tag_geodesic, famous_kappa_not_13, famous_empty_declines, famous_singleton_declines, famous_spiral_declines.

QEX (named — do not discharge)

• Earth great-circle length (~32090 km / ~11241 km) or angular span (~288°35′ / ~101°6′) — famous_earth_length_missing
• ETOPO1 land/water mask / “longest uninterrupted” — famous_etopo1_missing
• Sphere vs WGS84 ellipsoid / geoid — famous_sphere_vs_wgs84_missing
• Optimality of branch-and-bound — famous_branch_bound_missing
• Emit of GEODESICSTRING bytes / WKB 13 as signed I/O — famous_emit_wkb13_missing

Hard no

• Remint letter: GeodesicString as sheet geodesic (claimId 0007-intake-geodesic) #744/tools: GEODESICSTRING n≥2 maps to the LineString MkChord bag #745 claimIds
• MkGeodesic / geodesic_eval / MkSpiral / spiral_eval as γ
• Expand first_cook_scope; CompoundEgg / compound_eval
• Halley/Fresnel as γ or 𝓘
• Unhold ADR-0007 NURBS first-cook (claimId 0007-nurbs-first-cook) #729 NURBS
• Silent chord demote framed as Earth geodesic / “we proved the Science path length”
• Axiom / Parameter / deferred stub

Verification

• make ci-guards PASS (md-prose-ratchet: no *.md changes vs origin/main)
• tools/WktIntakeWalker/smoke.sh — not present on this tree (retired to archive/ after tools: .NET hunter for SqlMmExampleFactory vs C# WktIntakeWalker μ #748)
• pwsh tools/WktIntakeWalker/smoke.ps1 PASS (famous-water / famous-land bags equal matching LINESTRING, MkChord-only; GEODESICSTRING (0 0, 2 0) kept)
• Host Rocq compile of IntakeFamousGeodesic.v is CI’s macOS rocq job (no local rocq on this agent). File reminted from letter: famous GEODESICSTRING fixtures (0007-famous-geodesicstring) #746 tip against unchanged μ APIs on 6d68718.
• Await human go. Do not merge.