[carlostoledo1891]

#216, #230 and #232 applied the CONTRIBUTING rule that the marker "is removed when that changes — when the paper is refereed and published, or when the argument is formalized or independently replayed." This PR offers that replay for the two C31 rows merged in #231, with no code shared with the claimant. Markdown only.

What was replayed. [J2026] runs Lueker's upper-bound method ([L2009], Theorem 3.3): an automaton $M_h$ over pairs of binary strings with history length $h$, a weight matrix $A_z$, and a positive vector $v$ with $A_z v \le \lambda v$, which gives $\gamma_2 \le 2\log(2z)/\log\lambda$. Lueker computed $h \le 8$; the two rows take $h = 9$ and $h = 10$.

row	states (ours = [J2026])	$z$	our certified $\lambda$	[J2026]'s $\lambda$	our bound	printed
$h = 9$	51,425,006	0.3298	$\le 0.364708361168896$	0.364708361184292	$\gamma_2 \le 0.8251002730$	$0.825101$ ✓
$h = 10$	400,253,317	0.3376	$\le 0.385532597279844$	0.385532705434511	$\gamma_2 \le 0.8241195407$	$0.824120$ ✓

Beside each certificate a certified lower bound on the spectral radius of $A_z$, $\rho \ge 0.364708361168863$ at $h = 9$ and $\rho \ge 0.385532597279807$ at $h = 10$ (the minimum ratio under downward rounding): no certificate for these automata can print a $\lambda$ below it, and both of [J2026]'s sit above it, by $1.5 \times 10^{-11}$ and $1.1 \times 10^{-7}$. Any positive vector certifies, so those are valid, less converged certificates, not errors; both printed bounds hold with room.

How. The automaton was written from [L2009] alone (the 2008 extended version, whose Figure 8 and Theorem 2 are the journal's Figure 7 and Theorem 3.3), twice: a Python reference in the standard library and a C builder, which share no code with each other or with [J2026] (its src/ and review/ were never fetched). The two give identical tables for $h \le 5$; at $h = 8$, $9$ and $10$ the C table was checked by re-deriving the transitions of 2,000, 2,000 and 1,000 random states in the reference, 0 mismatches; the complement symmetry of the state set was checked. Calibration on Lueker's own Table II for $h = 2 \ldots 8$: every state count (7, 98, 1,020, 10,160, 89,960, 780,368, 6,419,109), every $\lambda$ to his nine digits and every bound to his six; at $h = 8$ the accepted-transition count, 91,508,397, is the one [J2026] publishes. The witness vectors are our own, from power iteration (294 and 338 passes); the certificate $\max_s (A_z v)_s / v_s$ is taken with the rounding mode set upward in every thread (self-tested) and the weights rounded up, once more in round-to-nearest with an explicit inflation; the bound $2\log(2z)/\log\lambda$ is evaluated outward in 60-digit decimal arithmetic. Every printed upper bound above is rounded up at its last digit, every lower bound down.

Red controls, which must come out wrong: the weights off by one power of $z$ and the truncation weight not summed both miss Lueker's $\lambda$ at $h = 8$; a claim below the certificate, $z = 1/2$, $\lambda = 1$, a vector with a zero entry, a vector of the wrong length and the all-ones vector are refused; a claimant $\lambda$ below the certified lower bound on $\rho$ is refuted. 9 of 9 fired.

Re-derive from https://github.com/carlostoledo1891/cert-machine at 61aae8eb42f1967e16d37d78cfe8a5c1be6d0d72:

python3 tools/run-lueker.py --check     # seconds: the reference automaton at h <= 4, every decision re-derived from the record's hex values, the pins, the red controls
python3 tools/run-lueker.py DATA_DIR    # the full run against stored tables and vectors (h = 10: 3.8 h to build the 29.5 GB table and 3.4 h of iteration on an M2 laptop)

Write-up: https://carlostoledo.co/reports/chvatal-sankoff.html.

What changes:

• The README cell for 31 reads 0.824120 without the asterisk; its "(unverified)" Recent-progress line is updated, and one line is added in the form the earlier replays were recorded.
• The two page rows lose the asterisk and get a one-sentence replay note, a [T2026] reference and a contribution note.

AI-assisted: prepared with Claude (Anthropic) in a certified-arithmetic setting: the replay code, the record and this pull request. Every number above is read from the pinned record at the commit cited, and was re-checked against the upstream files before sending.

🤖 Generated with Claude Code

[chessing234]

all good

[JeetuSK0808]

A third, separate replay agrees with this one. It reimplements Lueker's automaton in C from his published programs
(ics.uci.edu/~lueker/papers/lcs/code/upper/), with no code from [J2026] or from cert-machine, and certifies in
round-to-nearest with an explicit (1 − 2⁻⁵³)^−(4h+1) inflation:

h	z	states	λ_cert	γ₂ ≤
8	0.3209	6,419,109	0.341832258732947	0.8262791786 (Lueker's 0.826280)
9	0.3298	51,425,006	0.364708580678097	0.8251007652 < 0.825101
10	0.3376	400,253,317	0.385532782589023	0.8241199563 < 0.824120

Both vectors were stopped once the bound was certified, so their λ is a little above yours and above the
claimant's, as expected. Code and outputs: https://github.com/JeetuSK0808/tao-constants-certificates/tree/fbe82cc/c31-chvatal-sankoff-replay

(Written with Claude Code.)

[carlostoledo1891]

Thank you. That's three independent readings now, and the state counts agree exactly at h = 8, 9 and 10 (6,419,109; 51,425,006; 400,253,317). Our bounds are 0.8251002730 and 0.8241195407, a little tighter only because our vectors were iterated further, as you say.

[teorth]

Holding this one, with a policy change behind it rather than any objection to the work.

The asterisk-removal requests have reached seven across two accounts (#216 and #230 merged; #232, #235, #242, #243, #249 open), covering C_1a, C_1b, C_1c, C_1d, C_3b, C_3c, C_31, C_49, C_71, C_82 and C_86. Each replay is carefully documented — certificate bytes by sha256, two implementations sharing no code, red controls that must fire — and I have no reason to doubt any of them individually. The problem is structural: a marker that one party can clear across the whole repository stops distinguishing anything, which defeats the purpose of having it.

So CONTRIBUTING now says:

Removing an asterisk takes a second party. Adding the marker is a reviewer's call, but taking it off is a claim that someone other than the submitter has checked the work, so it needs evidence from someone other than whoever is asking. Any one of these is enough: the paper is refereed and published; the argument is registered with a service that mechanically checks the proof against the stated theorem, such as Palomar; a maintainer signs off; or someone independent confirms the replay in the pull request or issue thread. A replay carried out by the person requesting the removal is not by itself sufficient, however carefully it is documented [...] Post the replay, and let a second party confirm it.

What this means here. The replay stands as posted; it just needs one of the four. The quickest routes are a Palomar registration of the construction, or someone unconnected confirming in this thread that they re-ran it and got the same enclosure. Your write-ups make that easy to do — the sha256 and the command line are already there.

I am leaving these open rather than closing them, so the confirmations can land on the existing threads.

One mechanical note: #232 is subsumed by #243, which covers the same two constants plus C_1c and C_1d. Whichever route you take, #243 alone is enough and #232 can be closed.

Thanks for the care in these; the issue is the shape of the rule, not the quality of the replays.

[carlostoledo1891]

Thank you, and understood. On the new rule: JeetuSK0808's replay above may already be the second party. It is their own C, written from Lueker's published programs with no code from [J2026] or from us, and as far as we know they have no connection to us. They get the same state counts at h = 8, 9 and 10, and bounds of 0.8251007652 and 0.8241199563, below the 0.825101 and 0.824120 in the rows. If that counts, the asterisks can come off; if not, we'll wait for one that does.

[JeetuSK0808]

Just confirming the independence part, since it's what the new rule turns on. I have no connection to Carlos or to the
authors of [J2026], and the replay above was written from Lueker's published programs only, with none of their code.
As I mentioned in that comment, it was produced with Claude Code, and the counts and bounds are exactly as posted. Happy
to go whichever route you prefer, including a Palomar registration if that's easier on your end.

[carlostoledo1891]

Thank you for confirming it. For the record on this side: your K5 and K6 certificates (#277, #279) are replayed the same way, with no code of yours run, on those threads.