A fully tie-free 9/4 lower bound for Greedy Shortest Superstring

This repository gives a symbolic Lean 4 formalization of an infinite family on which Greedy has no tie-breaking choice and its approximation ratio tends to 9/4.

Theorem (formalized asymptotic family). For every positive integer p, there are explicit parameters s = 2p and t = 10p, a reduced family of actual list-valued words, and an operationally tie-free Greedy run such that

Greedy / comparison >= 9/4 - 1/p.

The comparison word is an explicit common superstring, so its length is an upper bound on OPT and the same lower bound holds for Greedy / OPT.

For N = (8s+6)t, the formalization proves the exact lengths

Greedy     = 2(N+1)((18s+10)t+1)+1
comparison = 2(N+1)(N+4s+1)+2N-1.

The public endpoint is Lean/GSC/TieFreeNineFourthsTheorem.lean, and FORMALIZATION_9_4.md gives the proof map and audit instructions. Here fully tie-free has the operational meaning relevant to Greedy: the argmax over ordered pairs is a singleton at every live state. Losing pairs may have equal scores; no tie-breaking rule is ever consulted.

Status. The symbolic theorem is formalized without sorry, admit, a custom axiom, or native_decide. The independent finite replay modules use native_decide for large closed computations and therefore have a wider trust boundary. Neither result has yet been externally peer reviewed.

Earlier exact finite certificate (> 2)

The repository also retains the earlier computer-assisted finite counterexample:

Finite theorem. There is a reduced family of 627 words over 26 symbols such that the maximum-overlap ordered pair is unique at every one of the 626 Greedy steps. The forced output has length 1,598,889, while the exact optimum is 798,858.

Greedy          = 1,598,889
OPT             =   798,858
Greedy - 2*OPT  =     1,173
ratio           = 2.0014683460640064
unique maxima   = 626 / 626
final overlap   = 3

This finite artifact is dated 28 August 2026. It passed two independent executable replays, a separate proof audit, PDF visual QA, and modular Lean formalization.

Read the proofs

The symbolic 9/4 proof is organized from the parametric base construction, through the proper Greedy chronology and endpoint-rank transfer, to the public theorem listed above. See FORMALIZATION_9_4.md for the module-by-module decomposition.

The six-page paper is A Fully Tie-Free Counterexample to the Greedy Superstring Conjecture. Its source is paper/tie_free_counterexample.tex, built through paper/tie_free_release.tex.

The earlier adverse-tie construction remains documented in the original paper. It supplies the compact 627-word base certificate used here.

Verify the earlier concrete instance

Both tie-free verifiers use only the Python standard library:

python3 checker/verify_tie_free.py
python3 checker/verify_tie_free_independent.py

The compact verifier replays the base chronology, checks the endpoint-rank permutations, proves the selected pair is the unique maximum at all 626 stages, audits every possible optimal Euler closing pair, and derives the exact optimum.

The independent verifier reconstructs the construction from the four displayed periods, uses an exact run-length representation of every disturbed live word, recomputes each singleton global maximum, materializes both claimed hosts, performs 1,254 literal coverage checks, and verifies these SHA-256 digests:

dataset
9204a6f292d6a5864cabcf20b19c62536232d3bc0efc9676e763c57af02cd90b

forced Greedy host
2b5f737c8f518754395494d16189e3946bde0a48bddadcffce9a07ebd3112615

optimal host
c45807a376c13065d84e41e857d50c050cc9b728ea8f89c41bf4e93813daebf8

The original literal certificate can also be checked with:

python3 checker/verify_counterexample.py
python3 checker/verify_independent.py
python3 checker/verify_adversarial_replay.py

Lean 4 coverage

The project is pinned to Lean 4.33.1 and has no external package dependency:

lake build

Lean/GSC/TieFreeNineFourthsTheorem.lean is the end-to-end symbolic endpoint. Its family_certificate theorem constructs actual transformed inputs, proves that they are reduced, gives a singleton- argmax operational Greedy run with the exact forced length, and supplies an explicit covering comparison host with its exact length. tie_free_nine_fourths proves the limiting ratio by natural-number cross multiplication, without real-number division. This parametric dependency cone contains no native_decide.

Lean/GSC/TieFreeNineFourthsMain.lean is an independent finite checkpoint at s=7,t=5: 310 reduced inputs, 309 unique actual maxima, forced length 423,583, a covering host of length 210,860, and gap Greedy - 2*host = 1,863. Its large closed computations deliberately use native_decide, so their trust boundary includes the Lean native compiler and runtime.

Lean/GSC/Counterexample.lean is the closed literal certificate for the earlier 627-word construction. Lean/GSC/TieFree.lean checks its complete 626-step endpoint-rank replay, and Lean/GSC/TieFreeEndpoint.lean reflects all 1,083 directed overlap-9 closing pairs and their maximum endpoint score 1,213.

Earlier finite construction in one page

Start with the certified base run whose overlap profile is

551 copies of 9, then 19 copies of 2, then 56 copies of 0.

Insert a fresh bridge symbol around every old symbol. This changes every overlap k into 2k+1, makes the former zero tail positive, and commutes with every scheduled merge.

Number the 626 merges by t=1,...,626. Give each original input a head rank alpha and tail rank beta according to the step at which that endpoint is consumed, with the final endpoints ranked 627. Insert runs of a second fresh delimiter between the bridge symbols. If a live bridge-level pair has overlap q, right-head rank c, and left-tail rank b, its exact disturbed overlap is

628*q + 627 - c - b.

At step t, the scheduled pair has ranks (t,t). Every competitor has no larger bridge overlap and ranks at least t, with at least one rank strictly larger when its bridge overlap ties. Hence the scheduled ordered pair is the unique maximizer.

The forced selected overlaps are

12,557, 12,555, ..., 11,457
 2,663,  2,661, ...,  2,627
   113,    111, ...,      3

For exact optimality, every Hamiltonian order deficient by one old overlap symbol has transformed length at least 800,073. A base-optimal order must be an Euler circuit. Exhausting all 1,083 possible closing overlap-9 pairs shows the largest endpoint saving is 1,213, attained by the certified rotated tour, giving exact optimum 798,858.

Build everything

make verify
make lean
make paper

The paper build requires pdflatex.

Repository map

• Lean/GSC/TieFreeNineFourthsTheorem.lean: public symbolic 9/4 theorem.
• Lean/GSC/NineFourthsRun.lean: arbitrary-parameter proper Greedy chronology.
• Lean/GSC/NineFourthsPlateau.lean: symbolic maximum-overlap plateau.
• Lean/GSC/NineFourthsResidual.lean: residual overlap tables and cleanup run.
• Lean/GSC/TieFreeAssembly.lean: generic operational tie-free certificate.
• Lean/GSC/TieFreeNineFourthsMain.lean: independent finite s=7,t=5 checkpoint.
• FORMALIZATION_9_4.md: proof map, build commands, and trust-boundary notes.
• checker/verify_tie_free.py: compact exact certificate.
• checker/verify_tie_free_independent.py: independent exact RLE and literal-host audit.
• checker/verify_adversarial_replay.py: paper-from-scratch audit of the base construction.
• Lean/GSC/TieFree.lean: symbolic endpoint-rank certificate.
• Lean/GSC/TieFreeEndpoint.lean: exhaustive endpoint-maximum certificate.
• Lean/GSC/DelimiterExact.lean: generic framed exact-overlap and merge laws.
• Lean/GSC/TieFreeBridge.lean: exact bridge overlap and merge-commutation laws.
• Lean/GSC/TieFreeRealization.lean: full two-layer realization formula.
• paper/tie_free_counterexample.tex: formal proof.
• output/pdf/greedy_superstring_tie_free_counterexample.pdf: visually checked paper.
• ADVERSARIAL_AUDIT.md: audit of the original base construction.

AI-use disclosure

The search, construction, falsification cycle, executable certificates, formalization, manuscript, and audits were developed with substantial assistance from OpenAI Codex and multiple model instances, in the spirit of the Cycle Double Cover experiment. Executable evidence does not replace external mathematical review.

No license has yet been selected. Public visibility permits inspection but does not itself grant reuse rights.