[carlostoledo1891]

#216 and #230 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." In 3010f7e the four new $C_{1a}$ and $C_{1b}$ rows from #225 were marked as "replayed only by the submitting team's own checker". This PR offers that replay for all four, decided from the bytes the rows cite, with no code shared with the claimants. Markdown only.

bound	bytes replayed	exact value
$C_{1a} \leq 1.5027434868$ [A2026]	atrislabs/records @ 1fa857a0, 1a-sidon-autocorrelation/construction.json, sha256 7387452d1da7… (65,536 rational heights)	1.50274348670958337974…
$C_{1a} \leq 1.5027435320$ [EA2026]	EinsteinArena solution 2603 (AgentDiscover, 3 Oct): the element with that id of GET /api/solutions/best?problem_id=2, fetched 18 Oct (65,536 heights)	1.50274353195395969900…
$C_{1b} \leq 0.3808585504$ [A2026]	atrislabs/records @ 1fa857a0, 1b-erdos-minimum-overlap/construction.json, sha256 62a976fa1366… (114,688 rational heights)	0.38085855031642856010…
$C_{1b} \leq 0.3808585749$ [EA2026]	EinsteinArena solution 2507 (CodexProLong, 15 Aug), from the same endpoint, fetched 2 Oct and again 18 Oct, the same heights (3,584)	0.38085857485785830914…, scaled to $\sum h = n/2$ (below)

How. For a step function with $n$ equal steps, the autoconvolution ($C_{1a}$) and the correlation of $h$ with $1-h$ ($C_{1b}$) are piecewise linear with knots on the grid, so the supremum is a grid value: $2n \max_k \sum_i a_i a_{k-i} / (\sum_i a_i)^2$ for $C_{1a}$, and $(2/n) \max_m \sum_i a_i (D - a_{i+m}) / D^2$ for $C_{1b}$, with the heights $a_i/D$ over one common denominator. Both are computed as exact integer products (Kronecker substitution) and maximised over every shift, after the admissibility conditions are checked exactly ($f \geq 0$; $0 \leq h \leq 1$ and $\sum h = n/2$). Two implementations do this, sharing no code with each other or with the claimants' scorers (not run): Python (fractions and int) and JavaScript over BigInt. They give the same fraction for all four. The leaderboard heights are read as the floating-point numbers the platform parses.

One repair, stated. CodexProLong's heights as published sum to $n/2 + 1.9 \times 10^{-13}$, so as published they are not admissible, and both implementations refuse them. Scaled down to $\sum h = n/2$ exactly (the rescaling the leaderboard's own verifier applies in floating point), they stay in $[0, 1]$ and give 0.38085857485785830914…, below 0.3808585749. The row's note says so.

Red controls, which must come out wrong in both implementations: a bound $10^{-15}$ below the Atris $C_{1a}$ value, and the same function with one height doubled, are refuted; a negative height, a height above 1, and CodexProLong's heights as published are refused.

Re-derive from https://github.com/carlostoledo1891/cert-machine at 5de570c:

node tools/replay-stepfun.js --check   # the JavaScript decider against the record, a few seconds; the red controls must fire
node tools/replay-stepfun.js           # both implementations (~5 min; the Python one dominates)

Write-up: https://carlostoledo.co/reports/optconst-queue.html#step-functions (§2).

What changes:

• The README cells for 1a and 1b show 1.5027435 and 0.38085856 without the asterisk.
• The "(unverified)" Recent-progress line is updated, and one line is added in the form Remove the asterisk from C3b, C3c and C71: certificates independently replayed #216 and Remove the asterisk from C3c ≥ 1.674894211307116: the two-law certificate independently replayed #230 were recorded.
• The four page rows lose the asterisk and get a one-sentence replay note, with a [T2026b] reference ([T2026] is already Together AI on these pages) and a contribution note.

The Atris rows were first decided on #225 on 15 Oct (#225 (comment)); the EinsteinArena rows and the second implementation were added so that this replay covers every row the marker was put on, to the same two-implementation standard as #216 and #230.

AI-assisted: prepared with Claude (Anthropic) in a certified-arithmetic setting: the replay code, the records 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 and the leaderboard's API before sending.

🤖 Generated with Claude Code

[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.