C_4b: four 2026 lower bounds (Krachun 0.752796; Jones 0.753742; Naslund 0.758067; Jones 0.758068)

[JD-Jones-ASES]

Four rows appended to the lower-bound table of constants/4b.md, the README cell and "Recent progress" updated, references added. Markdown only. (Updated 20 Sep 2026: the third row, Naslund's 0.75806746, was added after its registration on 19 Sep. Updated 22 Sep 2026: a fourth row, 0.75806770413 from the nk-lean formalization registered on 21 Sep, was appended and the README cell moved to 0.758068; the first three rows are unchanged and stand as the intermediate bounds. The [Jon2026] key became [Jon2026a] to make room for [Jon2026b].)

Row 1 — Krachun (arXiv:2608.01325, 2 Aug 2026), 0.752796… — ten Paley chains glued by CRT; the first bound past 3/4. The page listed nothing after Lewko 2015, so this row is added for the record and because the next rows build on it.

Row 2 — Jones (23 Aug 2026), 0.753741541837329405… — Krachun's gluing over an eleven-block pool: his nine chains (the chain at 23 dropped because 23 | 299) plus two certificates on the square-free composite moduli 235 and 299, lifted by one new lemma. The Comments column lists both certificates in full (17 and 19 residues, heights 11 and 12) and the closed form, so the value can be recomputed without downloading anything; I recomputed both rows' constants from that data before submitting (including the two longest-path heights).

Row 3 — Naslund (19 Sep 2026), 0.75806746 (exact 37903373/50000000) — the best known value until row 4. An interval-moment criterion (digits carry ordered intervals; a component in square base b contributes a moment power f) over nine pairwise coprime components: six Paley chains, two composite three-low-digit codes at 215⁶ and 437⁶, and a 25-state recursion at the prime 2 in base 4^(10^10). The Comments column gives the criterion, the nine bases, the chain lengths and the exact surplus Σ fᵢ − α = 25671/10¹². From the paper's parameter table I rechecked the six chains (every forward difference a nonzero square), the six chain-power thresholds and the surplus identity; the composite and binary moments were not recomputed here. The row says so.

Row 4 — Jones (21 Sep 2026), 0.75806770413 (exact 75806770413/10¹¹) — the current best. Naslund's criterion and his nine components (the six Paley chains, the composite codes at 215⁶ and 437⁶, the 25-state binary recursion with its transition rules unchanged, at depth 10¹⁵) with several retained words of the 19·23 code replaced, intervals repositioned, rational widths changed and all nine moment powers reallocated; the Comments column lists the nine moment powers and the exact surplus Σ fᵢ − α = 38652/10¹⁵. The criterion is proved for every k ≥ 1, and the bound is unconditional with an explicit constant (r(N) ≥ c N^α for every N ≥ 1, not only a liminf). From the repository's certificate data I rechecked the six chains, the six chain-power thresholds, the two composite moment sums over the listed retained words with their free multiplicities, the binary threshold log₂ a > 2α at the certified growth factor, and the surplus identity; the composite arc geometry and the binary growth certificate itself were not recomputed here. The row says so.

Supporting material lives outside this repository, per the contributing guidelines:

• Rows 1–2: note, data, and a stdlib-only verification script: https://github.com/JD-Jones-ASES/fs-lower-bound (commit c2c0687); Lean 4 / Mathlib formalization of the full chain (definitions, the new lemma, Krachun's two lemmas reproved, the liminf statement, and 0.7537 < alphaInf by kernel-checked integer comparison; standard axioms only): https://github.com/JD-Jones-ASES/fs-formal (commit 4e79656); Palomar registry entry PALOMAR-2026-08-26-000004: https://palomar-registry.org/entry.html?id=PALOMAR-2026-08-26-000004&version=1
• Row 3: papers, exact certificate programs and the Lean 4 / Mathlib formalization (Lean 4.32.0; criterion and full value; standard axioms only): https://github.com/enaslund/sarkozy-lower-bound-0.758 (commit e5d6937, Apache-2.0); Palomar registry entry PALOMAR-2026-09-19-000006: https://palomar-registry.org/entry.html?id=PALOMAR-2026-09-19-000006&version=1. Not on arXiv at the time of writing.
• Row 4: the Lean 4 / Mathlib formalization (Lean 4.33.0; the criterion for every k, the full square value, and fourth- and sixth-power values; standard axioms only; certificate data checked by proved Lean verifiers, NanoDa replay) with the exact certificate data and the mathematical account (PROOF.md): https://github.com/JD-Jones-ASES/nk-lean (commit 55acbf0, MIT); Palomar registry entry PALOMAR-2026-09-21-000004: https://palomar-registry.org/entry.html?id=PALOMAR-2026-09-21-000004&version=1. No paper; not on arXiv at the time of writing.

The recorded values are the limits of closed forms or exact rationals; each construction is finite and explicit at every stage. If the maintainers prefer the unverified marker for a bound whose write-up is a repository note rather than a paper, please add the asterisk; in each case the registered formalization is offered as the verification.

AI-use disclosure. Rows 1–2: the result is AI-generated with a human managing the workflow (see the repository's DISCLOSURE.md). Row 3: the cited papers disclose that they were written by GPT-6-Astra under the author's supervision and the Lean development with Codex agents. Row 4: the repository discloses substantial AI assistance (OpenAI Codex agents for the mathematics, certificates and Lean; GPT 6 Pro, Claude and Grok contributed) with a human directing the work; see its DISCLOSURE.md. This pull request's text and the four rows were drafted with Claude (Anthropic); the references were checked by the contributor for rows 1–2, read directly from the registry record and the repository for row 3, and read from the registry record and the repository's certificate data for row 4, where the listed checks were run by the contributor from that data; the contribution note on the page says so.