TJC-1814: fix first CI run: grep guard, explicit pinned nanoda step

[arcaputo3]

Two failures surfaced on the inaugural CI run (30047099497), both fixed here:

• Paper job (exit 127): current ubuntu-latest images no longer ship ripgrep, so the fail-closed guard tripped on rg --version — exactly the failure mode it was designed to catch loudly. The guard now uses grep -qE (always present). Verified locally in both directions (no match on the real paper; synthetic @local/#import input trips it).
• Lean job (nanoda): lean-action's nanoda integration cannot run on this package — its module detection greps for a [package] table that Lake's TOML schema rejects (top-level name is mandatory; verified empirically), and it conflates the package name with the root module name (goemans vs Goemans). Replaced the nanoda: input with an explicit step in ci.yml and release.yml that exports module Goemans directly and pins lean4export and nanoda_lib by commit — stricter provenance than the action's unpinned HEAD clones. The pinned lean4export builds cleanly against the repo toolchain (checked locally). Permitted axioms mirror the action's default with sorryAx excluded (equivalent to nanoda-allow-sorry: false).

🤖 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