TJC-1814: leanchecker per push, nanoda at release; brace README superscripts

[arcaputo3]

Follow-up to #1 after the second CI run:

• Per-push kernel re-check → built-in leanchecker (ships in the toolchain; lean4checker is deprecated in its favor). All 25 modules replay in ~1:39 locally.
• Release-time independent re-check → nanoda pinned to json_string, the branch that parses lean4export's current NDJSON format — the previously pinned debug branch predates the format switch (Feb 2026), which is what produced invalid digit found in string on the 1.6 GB export. Verified locally end-to-end: 308,672 declarations, no typechecker errors, 39s on 4 threads.
• unpermitted_axiom_hard_error stays false deliberately: Lean core declares sorryAx in every environment, so strict mode fails on the declaration alone (verified). Dependency-level axiom policy is enforced in-build by Goemans.TrustAudit.
• Markdown math fix (user-reported): H^*/ρ^* superscripts braced as ^{\ast} in README/RELEASE_NOTES/RELEASE_CHECKLIST so GitHub's emphasis pass can't mangle them.

🤖 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