Goemans Gap

Lean 4 formalization and reproducibility artifact for the preprint How Far Can Goemans's Cost Conjecture Fail? An Exact Extremal Theorem for the Rybin Digraph, with Obstructions to Amplification.

The main result determines the exact worst-case cost ratio on the seven-vertex Rybin digraph $H^{\ast}$:

$$ \rho(H^{\ast})=\rho^{\ast}=\frac{2}{2\sqrt 2-1} =\frac{4\sqrt 2+2}{7} \approx 1.0938363214. $$

Here $\rho(H^{\ast})$ is the supremum, over positive-fractional-cost instances on $H^{\ast}$, of the least admissible unsplittable cost divided by the fractional cost. The supremum is not attained. The repository also checks D. Rybin's original counterexample exactly: fractional cost 58 versus minimum admissible unsplittable cost 60, a ratio of $30/29$.

This is a research preprint dated July 23, 2026. It has not been peer reviewed. The GitHub URL in the citation metadata is the planned public location; this working tree does not claim that a public tag or archival DOI already exists. See the publication release checklist for the gates that must be checked against the eventual release commit.

What is certified

The artifact deliberately separates proof-producing components from exploratory computation.

Component	Method	Claim level
Goemans/	Lean 4 + mathlib, kernel checked	Exact upper bound, explicit integral Pell lower family, supremum equality, and strict non-attainment on $H^{\ast}$ — in parametrized and first-principles graph form, with path enumeration, flow decomposition, and literal model round trips proved; plus the Section 5 gate collapse, both conclusions of Proposition 5.1, Definition 6.1, Lemmas 6.2–6.4, Remark 6.5, and Definition 7.1/Lemma 7.2 with the one-stage unit-demand threshold and strict ratio bound
verify-goemans	Exhaustive integer enumeration	Exact 58-versus-60 counterexample and exact violation-budget thresholds
amplify-family	fractions.Fraction	Exact checks for the displayed integral families
revision-checks	Exhaustive rational enumeration	Exact checks for the general-family examples, gate collapse, and dummy-terminal embedding
certify-sweep	Seeded floating-point vertex enumeration (numba-jitted) and local search	Numerical stress test on $H^{\ast}$ plus a sampled four-terminal side search; boundary points and cases with more than nine admissible routing vectors are skipped, so this is not a proof certificate
interval-search	Exhaustive finite structure enumeration plus truncated assignment enumeration and floating-point grid/refinement	Exploratory records in the stated chain subclass; at most the first 16 minimal-transit assignments per structure are examined
laned-search	Seeded floating-point heuristic over every fifth canonical structure	Exploratory records in the stated laned subclass; a deterministic one-fifth structure subsample

The Lean development contains no sorry, admit, or native_decide. Its publication-facing endpoints are:

theorem theoremA_exact :
    rhoHStar = rhoStar ∧ rhoStar ∉ hStarRatios

theorem theoremA_graph :
    sSup graphRatios = rhoStar ∧ rhoStar ∉ graphRatios

theoremA_graph states Theorem A over first-principles instances (demands, conservation-law flows, costs, routings over genuine s → tᵢ walk choices): the split parametrization is proved, not assumed (walk_s_terminal_iff, IsCommodityFlow.commoditySplit_spec). The translations between graph and split instances are literal inverses. The computable Pell recurrence pellPair supplies genuine integral instances whose exact ratios converge to rhoStar. The Section 5 gate collapse is gate_collapse; splice_eq and pathUnionArborescence formalize both conclusions of Proposition 5.1. Goemans.Chain formalizes the complete-arc exit-cost model of Definition 6.1 and Lemmas 6.2–6.3. Goemans.ChainComposition proves the genuine disjoint parallel-union bound of Lemma 6.4 and the appended-stage dummy construction of Remark 6.5, including exact optimum/ratio preservation and realized-ratio inclusions for terminal counts. Goemans.Laned defines full routing paths and complete-arc admissibility independently of packing, proves the iff in Lemma 7.2, identifies chains as the one-lane case, and proves the exact one-stage unit-demand cardinality threshold. Goemans.LanedRatio uses a separately proved strict weighted-selection theorem to certify that the corresponding positive-cost ratio is strictly below one. The numerical searches and Conjectures B–D remain exploratory/open rather than Lean-certified. Concrete integral checks use kernel decide; analytic arguments use explicit linarith/nlinarith certificates over the real model. Python is an independent reproduction layer, not part of the Lean proof.

Reproduce

The commands below assume a source checkout. The Python project is a local convenience package and is not published to PyPI.

Lean 4

The toolchain and mathlib revision are pinned by lean-toolchain and lake-manifest.json.

lake exe cache get
lake build --wfail

The build includes Goemans.TrustAudit, which guards the exact axiom inventory of every publication endpoint and runs all default environment linters over the Goemans namespace. To run that boundary by itself:

lake build Goemans.TrustAudit --wfail

The analysis, optimization, graph, Pell, gate, arborescence, and chain endpoints use only the guarded standard inventory [propext, Classical.choice, Quot.sound]; splice_eq needs only [propext, Quot.sound]. Changing an inventory or introducing a linter finding breaks the build.

Python

uv 0.11.6 or later is recommended; Python 3.11 through 3.14 is supported, and 3.14 is the default.

uv sync --frozen
uv run --frozen pytest

The default test run executes the three exact, fast verifiers and compares their complete output byte-for-byte with outputs/. The numerical searches are intentionally separate because they take several minutes:

uv run --frozen pytest -m slow

Individual entry points are also available:

uv run --frozen verify-goemans
uv run --frozen amplify-family
uv run --frozen revision-checks
uv run --frozen certify-sweep
uv run --frozen interval-search
uv run --frozen laned-search

Slow tests assert stable scientific guardrails rather than platform-dependent floating-point tie breaks.

Standalone paper

The paper uses only vanilla Typst and repository-local assets—there are no private package or font dependencies. With Typst 0.15.1:

typst compile --ignore-system-fonts \
  paper/goemans_gap_paper.typ paper/goemans_gap_paper.pdf

--ignore-system-fonts verifies that the document depends only on fonts embedded with Typst. The .typ file is the canonical paper source.

Publication supplement

To build the deterministic release archive and its SHA-256 checksum:

uv run --frozen python tools/build_release_bundle.py --version 0.1.0
(cd dist && sha256sum --check goemans-gap-v0.1.0-supplement.zip.sha256)

The ZIP contains a second MANIFEST.sha256 covering every payload file.

Repository map

Goemans/          Lean definitions and proofs
paper/            canonical Typst source, standalone PDF, and cover logo
src/goemans_gap/  exact verifiers and exploratory numerical searches
tests/            exact-output and numerical-guardrail regressions
outputs/          committed reference output
tools/            deterministic release-bundle builder

Provenance

Rybin publicly posted the original 58-versus-60 instance on X, together with a shared GPT-5.6 Pro transcript. Both links were accessed July 23, 2026. In the discussion that followed, H. Juang posted a three-parameter counterexample family on the same digraph with the extremal parameter direction (accessed July 23, 2026); the paper's Section 4 relates it to Proposition 4.1. This repository formalizes and extends Rybin's result; it does not claim authorship of the original counterexample. A. Richard Caputo III is the human author of the present artifact. The paper's acknowledgements identify Weaver, a research agent based on Anthropic's Fable 5, as assisting with exploration, drafting, and Lean formalization, and GPT-5.6 Sol as assisting with Lean formalization and reviewing the mathematics and publication artifact. These systems are acknowledged as assistance, not listed as authors.

Citation and license

Pre-release citation metadata is in CITATION.cff. It does not assert a release tag or DOI. Once published, please cite a tagged, durably archived release so the proof, paper, scripts, and outputs remain aligned.

Repository-authored material is available under the MIT License. The TJC name and logo are excluded from that license; see NOTICE.