TJC-1814: use dollar math delimiters in release notes and checklist

[arcaputo3]

GitHub Markdown renders only $...$ / $$...$$ math — the LaTeX-style \(...\) and \[...\] delimiters in RELEASE_NOTES.md and RELEASE_CHECKLIST.md displayed as literal source (user-reported on the release notes). Same content, GitHub-native delimiters; the ^{\ast} superscript form from #2 is retained.

🤖 Generated with Claude Code

[linear]

TJC-1814 Formalize Goemans gap paper in Lean 4: Rybin counterexample + Theorem A (ρ* worst case)

Formalization project for the Weaver/TJC paper "How Far Can Goemans's Cost Conjecture Fail?" (r3, 2026-07-23), per its Appendix A targets. Repo: ~/git/goemans (Lean 4.32.1 + mathlib v4.32.1). See the repo README for the full theorem/status table.

Milestones

M1 — Counterexample (machine-checked refutation) ✅ done 2026-07-23

• H* path/routing model of §2 as a finite structure (Goemans/Model.lean)
• Rybin instance d=(15,10,15), f=(5,4,5), c=(2,3,2): fractional cost 58, min admissible unsplittable cost 60 — kernel-decided over ℤ; cost_conjecture_false + exact ratio 30/29 (Goemans/Rybin.lean)
• Prop 4.1 concrete members: (17,12,1000) and Pell (577,408,10⁶) — kernel-checked record ρ(H*) > 1.0938363, within 2.1·10⁻⁹ of ρ* (Goemans/Family.lean)

M2 — Theorem A upper bound (worst case): ρ(H) ≤ ρ = 2/(2√2−1) ≈ 1.0938363** ✅ done 2026-07-23

• Lemma 1 (admissibility ⟺ three linear inequalities) — admissible_iff
• Lemma 2 (blocked pair ⇒ z_i + z_j ≤ 1) — pair_bound
• Lemma 3 (split LP: all-blocked ⇒ Σz ≤ 4−2√2) — splitLP, certificate (√2δ−D)² ≥ 0
• Lemma 4 (reduction to nonnegative savings) — inside exists_admissible_ucost_le
• Lemma 5a (weight inequality, four cases) — weight_core_a/b/c/d + exists_admissible_weight
• Assembly: exists_admissible_ucost_le — every instance has an admissible routing of cost ≤ ρ*·(fractional cost)

M3 — Sharpness + non-attainment ✅ done 2026-07-23

• ℤ→ℝ cast bridge (FlowInstance.toReal); Rybin ratio 30/29 in the real ratio space (rybinPositive_ratio)
• Lemma 5b (strict split LP + strict weight cores) ⇒ non-attainment (exists_admissible_ucost_lt)
• Prop 4.1 symbolically (general (a,b,M)) + dense-rational integral family limit ⇒ theoremA_exact : rhoHStar = rhoStar ∧ rhoStar ∉ hStarRatios (IsLUB)
• Fidelity: two-paths-per-terminal enumeration (walk_s_terminal_iff), flow decomposition (IsCommodityFlow.exists_split), and the unparametrized restatement theoremA_graph : sSup graphRatios = rhoStar ∧ rhoStar ∉ graphRatios

M4 — Section 5 formalization (gate collapse + Prop 5.1) ✅ done 2026-07-23

• Gate gadget (Def 5.0) digraph with kernel-checked path enumeration: 3/4/4 paths per terminal, splices exist (gateWalk_terminal_iff)
• Exact collapse over ℤ (d=100, f=49): designed pairs blocked, designed-space min 200, splice routing admissible at cost 100 = global min vs fractional 153 — headline gate_collapse
• Proposition 5.1 generically (ranked digraphs, prefix determinism): splice_eq, axioms [propext, Quot.sound]

Working over ℤ for decidable checks (kernel decide cannot reduce ℚ arithmetic — Rat.add normalization is WF Nat.gcd) and ℝ for Theorem A. No native_decide, zero sorry; all endpoints audit to [propext, Classical.choice, Quot.sound] or smaller.

Review in Linear