Method

What “conditional κ” means

Upstream CrocSwap/integer-mult-bounds races an asymptotic integer-multiplication bound of the shape T(n) = O(n (log n)^(1−κ)). Every κ published there is conditional: it holds only if a list of earlier steps the construction relies on, and does not re-prove, are correct. The race names them (in its own terms: the all-size compiler, the weighted common-ancestor chart, restored rows, selectors and routing, prime supply, precision and recovery, complex symbolic correctness, and the analytic transfer). A larger κ is better. It is not an unconditional multiplication-exponent theorem, and this dashboard never presents it as one.

Tiers

• claimed — default. Any open upstream PR whose title/body carries a parseable κ value (exact fraction and/or decimal). Draft PRs stay claimed and render hollow-grey; they are never promoted.
• human-verified — only when a PR’s exact (κ fraction, κ decimal) matches upstream certificates/selected-result.json on main (maintainer-reviewed checkpoint, bound by its certificate_sha256). v1 expects exactly one such point.
• lean-verified — reserved; requires a Lean formalization artifact. No upstream PR has one today, so v1 ships this set empty (schema support only).

Quarantine policy

A record is quarantined (stale: true) when its stated fraction and decimal disagree beyond 15 significant digits, when a κ-looking claim is unparseable, or when the pull request’s latest commit (its head) changed and could not be re-read. Quarantined records stay in data/records.json and under feed.json’s quarantined[] (never silently deleted) but are excluded from the chart step-line until re-resolved.

Record key and staleness

One record per pull request and commit. When a contributor rewrites a pull request’s history (a force-push), its new commit gets a new record and the old row is kept; rows are only ever added. fetched_at and pr_updated_at drive the age display. The caveat at the top of the dashboard is always on, because the race moved roughly every ten minutes and nothing served here is a live quote.

Since the move to Foundation0, the dashboard also reads the race’s own certificates/selected-result.json live in your browser and shows it at the top, labelled with the time it was fetched; when this feed is more than a day old, it says so beside that value.

Pipeline

Status: not running since 11 October 2026, 17:41 UTC. The tracker was designed to refresh every 15 minutes through a scheduled GitHub Actions job (.github/workflows/update.yml). That schedule has not run since the feed’s last generation on 11 Oct 2026, 17:41 UTC (the job is switched off in the repository’s Actions settings), so the claims on the dashboard are a snapshot.

As designed, each run calls scripts/fetch.py, which reads the race’s pull requests from GitHub and asks only for what changed since the last run, then scripts/gate.py, which makes four checks: the files match the published schema; rebuilding them from scratch gives the same bytes; the reviewed value is bound to the exact bytes of the race’s record file; and no claimed value is ever labelled reviewed. Only if all four pass does the job commit the regenerated docs/feed.json and docs/chart-data.json; a failed run changes nothing and the last good state stays up. The parser that reads κ out of pull-request text is tested against saved examples, PRs #419, #425, #431 and #433 (tests/golden_kappa_parse.json, tests/run_golden.py).

Schema reservations (v2, additive)

feed.schema.json already permits project_id, claim_id, machine_checked, ai_refereed_count and feed_version: 2 for the planned multi-project feed (integer-mult-kappa, threesum-derand, mobius-x1). v1 producers emit none of them.