The methodology arm of the Arithmon program: a formal standard for the question how surprising is a claimed exact relation between mathematical invariants and measured physical constants?
Sometimes a short formula in fundamental constants and small whole numbers lands surprisingly close to a measured quantity. Sometimes that is a real clue about nature. Sometimes it is an accident, made to look meaningful afterwards by a lucky choice of formula. The hard part is telling the two apart before you know which one it is.
History has both kinds. Eddington argued the fine-structure constant had to be exactly 1/136, then exactly 1/137 once the measurement moved: a coincidence, refitted after the fact. The quantum Hall resistance, by contrast, is an exact ratio that was predicted, never revised, and later explained: a real relation. The field usually only sorts cases like these in hindsight, once the verdict is already in.
The Sieve is an attempt at an instrument that sorts them in advance, by a rule fixed before looking. The inputs (which constants count, which formulas are allowed) are written down and time-stamped with a public DOI before any search runs, so nothing can be quietly tuned to the answer. The instrument is then checked on known cases (Eddington and quantum Hall are the development poles), with the duty to report which components and policies separate them, including where the frozen rule does not reproduce the received verdict: it admits Eddington's 1941 claim as a screen survivor, and says so. Only after that is it turned on anything we care about, including the K₇ framework itself. Anyone can run it on their own framework, including one built to try to beat it.
The rest of this page is the technical specification: the expression space, the complexity measures, the four null models, the scorecard. If you only wanted to know what the Sieve is and why to trust it, you have it.
The program's charter and open problems live in the program repository; the map of adjacent work lives in the atlas; the machine-checked formal layer (certified expression-space counts, isolation ranks, and the in-framework-theorem rebate) lives in lean.
freeze/holds the frozen inputs: the observable list (28 dimensionless measured constants, framework-independent inclusion criteria, values verified against CODATA 2022 / PDG 2025 / NuFIT 6.1 / Planck 2018 with per-value citations) and the expression grammars (three alphabets, two complexity measures, anti-gaming guards).scripts/holds the pipeline: the expression-space engine (three grammars, two complexity measures), the four null models N0 to N3, the calibration controls, and the generic scorecard (coincidence_scorecard.py: feed it any framework's claims against the frozen targets and get the full component report).results/holds the machine-readable outputs of every run, deterministic seeds throughout.docs/holds the living pre-registration: the decisions ledger (discipline, milestones, dated decisions) and the legend that resolves every label used across the program.
- Freeze before search. The observable list and the grammars are deposited with a dated DOI before any expression search runs. The DOI timestamp is the proof. A data update (new PDG edition, new global fit) is a new freeze version with its own DOI; verdicts against the old version stand.
- Development checks and calibration before use. The method must condemn deliberately constructed fake frameworks and be run against the historical development cases (Eddington's 1/136-then-1/137, with a penalty for the revision; the quantum Hall relation) before it is allowed to score anything we care about. Development verdicts are reported as computed, never tuned to the received ones: where the frozen rule disagrees with the textbook verdict (it admits Eddington-1941 at the registered thresholds), the disagreement is published and priced. If calibration surfaces a failure, that failure is the result.
- The scorecard, not a single p-value. Per-relation local significance, joint global significance under each null, complexity budget consumed, and an explicit declaration of researcher degrees of freedom.
- Open by construction. Frozen inputs, pinned environment, deterministic seeds. Anyone can re-run the pipeline against any framework, hostile parties included.
Freeze v1.0 DEPOSITED 2026-06-12: DOI 10.5281/zenodo.20666879 (concept DOI for all versions: 10.5281/zenodo.20666878). At deposit time, no expression search had run; everything below operates against these inputs as frozen.
Freeze v1.1 DEPOSITED 2026-07-30: DOI 10.5281/zenodo.21705149. Adds the held-out registration, the case file, and the frozen analysis runner, deposited before the held-out runs it governs. Verdicts against v1.0 stand.
Erratum v1.1.1 DEPOSITED 2026-08-06: DOI 10.5281/zenodo.21820451. Corrects statements, re-runs nothing: the v1.1 registration text stands as frozen, errors included, with the erratum above it; the analysis runner is byte-identical and the held-out results are re-derived bit-for-bit from it. No value, node count or verdict moves. The held-out run record enters the deposit for the first time (v1.1 was deposited before the runs, by design).
Companion preprint PUBLISHED 2026-07-30, revised (v2) 2026-08-06: Preregistration Requires a Decision Rule, concept DOI 10.5281/zenodo.21706145 (v1: 10.5281/zenodo.21706146, v2: 10.5281/zenodo.21824030). The argument: freezing the inputs is not enough; without a frozen decision rule (explicit thresholds, fixed before the run), a registration still leaves room to choose the verdict after the fact. The paper freezes the Sieve's rule and applies it back to the development case. The honest headline is printed in the abstract: the frozen rule, applied to the contested historical case, admits Eddington's 1941 relation as a screen survivor. Freezing did not make the contested verdict go away; it made the commitment explicit and priced it. Anyone who prefers a stricter rule must freeze it, and say so, before the next run.
Development checks and scaffold calibration completed (scaffold budget, 5-6 nodes):
- Negative controls CONDEMNED: an adversarial best-match fit and an invented-alphabet framework land at the 89th and 17th percentile of the fitting null (survival requires the 99.9th).
- Historical development cases run: at the scaffold screen (agreement within 1 sigma), Eddington's 136-then-137 fails at every era (revision penalty applied) and the quantum Hall quantization passes (exact, essentially unique, never revised, explained by TKNN 1982). Under the frozen v1.1 rule (tau_z = 2), Eddington-1941 is admitted as a screen survivor, as the preprint entry above reports; the two statements differ by the agreement threshold, which is the preprint's point.
- Four nulls implemented: N1/N2 price the search (survival thresholds clear the N2 alphabet-freedom envelope), N3 catches assignment vagueness, N0 anchors the accidental-match baseline.
- First N1 against the frozen list: at a 5-node budget, 6/28 (G_INT), 3/28 (G_STRUCT) and 2/28 (G_TRANS) entries carry information at their measured precision; a lone match on a loosely measured constant is worth little by construction.
Issues are welcome, in particular: historical cases that should join the calibration set, null models we have not considered, and ways to game the scorecard (rule 4 means finding them is a contribution). The four procedures the Sieve owns (propose or attack a null model, submit a hostile framework, challenge a freeze, report a cherry-picking issue) are spelled out in CONTRIBUTING.md. House style is enforced by the org linter: plain language, no promotional vocabulary, no em-dashes.
K₇ (formerly GIFT) is the founding framework of the Arithmon program. Program: arithmon.com · github.com/arithmon