What we added

The problemA cheap model can score millions of compositions, but it can only be wrong in ways it cannot see. The first survey of the design space passed seven compositions. Off the lattice, every one of them loses to crystals a bcc model cannot represent (E54, E56).

The ideaNo single model gives the verdict. Each candidate climbs a ladder of rungs, and each rung asks a different physical question that the one below cannot: its energy on the bcc lattice (rung 0), whether it orders inside 90–1000 K (rung 1), whether a different crystal off the lattice is lower (rung 2), whether order could form in time (rung 3), and a full DFT calculation on the find itself (rung 4). A candidate goes up only by passing. From E35 on, the log's decisive tests are pre-registered: the prediction, the bar that would falsify it and the decision it drives are written before the run, and the result is scored against them, including when it fails.

What it boughtThe off-lattice rung withdrew all seven of the survey's qualifiers. At 90 K each sat 98–185 meV/atom above the cheapest mixture of competing phases (E56). At HfV₂ and ZrV₂ the C15 Laves phase lies 119–123 meV/atom below bcc, 21 times the expansion's own error (E54). On the current walk, 32 finds entered rung 1 and 11 passed rungs 0–2 (E240). One goes to DFT (E242, running). The bar decides what ships: E238's new labels failed theirs, so the model that ships is E237's.

From the operator

The target the ladder is built around is the operator's. In E39 they set the deliverable as short-range order and order–disorder transition temperatures, not the lowest free energy; that is the question rung 1 asks of every candidate.

Verified by

Each rung must pass a known answer before its verdicts count. Rung 1 must put equiatomic Mo–Ta's ordering inside 500–2600 K; it gives 1149 ± 114 K, against a published cluster-expansion Monte Carlo value of 2020 ± 545 K (E242). Rung 2's hull reproduces all seven Laves phases the literature reports as stable in this system (E56).

Builds on

Tiered screening, with cheap filters ahead of expensive calculations, is the standard high-throughput pattern (Curtarolo et al., Nat. Mater. 12, 191, 2013). Pre-registration comes from the replication literature (Nosek et al., PNAS 115, 2600, 2018). Every rung's model is someone else's: pyeCE, MACE, Quantum ESPRESSO. Ours are the questions, their order, the known answer each rung must pass and the rule that the bar comes first.

The problemFor two days rung 1 put every ordering temperature at about half the published value. The model was blamed, and refits were built to cure it (v6a and v6b, E190b).

The ideaStop asking the model and test the sampler on a problem whose answer is known exactly. Fit the same network to a nearest-neighbour Ising model on bcc (J = 19.12 meV, exact transition 1410 K), give it to pyeCE's sampler, and compare with an independent Metropolis sampler written here. Then read pyeCE's source for a convention that would produce a factor. It was there: the model gives an energy per atom for each two-site cell, the sampler adds cells to price a swap, so it sees half the true change and samples at twice the temperature it was asked for. The same aggregation turns its short-range-order column into the average of α and its own standard deviation, (α + σ)/2. That can be decoded exactly for an ordering pair (α < 0) and not at all for α > 0, so the decoder refuses rather than guesses.

What it boughtOrdering temperatures became comparable with the literature. On the physical axis, v5 put Mo–Ta at 910–1037 K by every estimator (published 2020 ± 545 K) and MoNbTaVW at 697–702 K (published 742 and 750 K). Against Sobieraj et al.'s table, four of five systems land within 22 %; the fifth is a Cr–Ta disagreement that DFT then settled (E222). The refits' starting premise, "rung 1 reads half the published value", was the sampler's factor, not the model's.

From the operator

The external scorecard this section scores against began with the operator's request in E42 to reproduce a result published by a professor on the project, Sobieraj et al. 2020, on Ta–Ti–V–W. It came out at 383 ± 75 K against their 500 K, with the same strongest ordering pair, Ta–W.

Verified by

The exact Ising model came out at 612 K nominal, against 1300–1340 K from the independent sampler (E215). On a fine grid the factor is 2.000 ± 0.03 (E215c). On pyeCE's own sampler object, v5's true swap change of 538.4 meV was seen as 269.2 meV, a ratio of exactly 0.500. Decoded α agrees with the independent sampler to within 0.007 at four temperatures. Tests pin both conventions (tests/test_pyece_sampler_factor.py, tests/test_pyece_sro_encoding.py), so a future pyeCE that changes them turns a test red. Adversarial code reviews caught an earlier, guessed reading of the SRO column and then confirmed the decoding algebra.

Builds on

The Metropolis algorithm (Metropolis et al., J. Chem. Phys. 21, 1087, 1953); Warren–Cowley short-range order (Cowley, Phys. Rev. 77, 669, 1950); pyeCE and the embedded cluster expansion (Müller & Natarajan, npj Comput. Mater. 11, 60, 2025); and the published numbers it was scored against (Kim & Widom, Phys. Rev. Materials 7, 063803, 2023; Sobieraj et al., PCCP 22, 23929, 2020). The upstream fix is pyeCE's to make. Here every temperature is read as nominal × 2, with the factor stated.

The problemRung 1 prices about 1.8 million swaps per composition (E238). pyeCE's forward pass managed 28 swaps a second at embedding 9, the size that got Mo–Ta right, so one rung-1 walk would take about 15 hours (E233). Accuracy and cost were pulling in opposite directions.

The ideaRe-evaluate the model instead of approximating it. The eCE energy is a small network applied to correlation functions, and those are sums over clusters. Written as one correlation tensor per orbit, with the linear embedding folded into the first layer, the same numbers come out of a few tensor contractions instead of a loop that gathers each cluster.

What it bought1,519 swaps a second against 28 at embedding 9 (54×), and 2,788 against 1,009 for v5 (E237). Rung-1 cost stopped depending on the embedding size, so the shipped model (embedding 6) was chosen on accuracy alone. Rung 1 now samples the mean of the three-seed ensemble.

Verified by

Parity with pyeCE's own forward pass: over 2,304 swaps, a mean difference of 0.0012 meV and a maximum of 0.0071 (E237). An adversarial review on seven models found per-cell differences of at most 6.3 × 10⁻⁷ eV and no measurable drift over more than 1,300 accepted swaps. Rung 1 on the same model gives 1148 ± 114 K against 1175 ± 114 K through pyeCE. The fold is proved in Lean and tested. A tiling known answer covers pairs longer than half the cell (1.5 × 10⁻⁵ meV/atom). A fitted surrogate was tried and failed parity (55.7 meV RMS per swap), although its transition landed at 1170 K. That is why parity, not the transition temperature, is the acceptance test.

Builds on

The embedded cluster expansion and its network are Müller & Natarajan's (npj Comput. Mater. 11, 60, 2025; the pyeCE software), and the correlation-function form of the energy is Sanchez, Ducastelle & Gratias's (1984). Ours are the re-evaluation and its checks.

The problemEvery refit was judged on 48 held-out RHEA rows. Refit the same model with two more random seeds and that number barely moves: 7.2, 7.4 and 7.5 meV/atom.

The ideaTrain every candidate model as at least three seeds and judge the ensemble on DFT that no model was chosen or steered by: eleven Quantum ESPRESSO cells, and later the search's own random cells. The spread across seeds is reported as the model's error bar on each cell.

What it boughtThe same three fits miss the eleven cells by 22.9, 16.6 and 23.8 meV/atom. The seed spread averages 8.5 meV/atom per cell and reaches 25 on the most strongly ordered one (log, 22 Sept., before E229). Judged this way, embedding 5 was not shipped although it passed its own bars: it missed Mo₇₀Hf₂₀Ti₁₀ by +23.9 meV/atom with a seed spread of only 2.9. Embedding 6 held both tests (E237).

From the operator

In E40 the operator required that the circuit learn uncertainty properly. There, a bootstrap ensemble's spread proved worse than a constant (interval width 1.763 against 1.124) because the error was a reproducible bias, not a variance; conformal prediction made every signal honest (after Hu, Musielewicz, Ulissi & Medford, Mach. Learn.: Sci. Technol. 3, 045028, 2022). That is the standard this section holds an error bar to: it counts only once it is checked against errors the model did not see.

Verified by

The rule caught two confidently wrong models. Embedding 9 over-binds two of the search's three random cells by about 13 meV/atom with a seed spread of 1.2–1.8 (E223, rung 4), and embedding 5 is the case above (E237). In both, the spread alone would not have flagged the error; the unsteered DFT cells did.

Builds on

Ensembles of independently trained networks as an uncertainty estimate (Lakshminarayanan, Pritzel & Blundell, NeurIPS 2017). Müller & Natarajan already report that eCE validation errors vary across random initialisations (npj Comput. Mater. 11, 60, 2025). Ours are finding that the held-out metric was blind to the spread, and the rule that every refit is judged as an ensemble on DFT no model chose.

The problemIn the fly's mushroom body only a few per cent of Kenyon cells fire for an odour, and learning happens only at synapses from cells that fired. The model set its threshold so that 10 % of the raw input cleared it. Recurrent inhibition then silenced most of what cleared, and on the near-pure compositions a corner-seeking search visits, 0.07 % fired: three cells of 4,064 (E61).

The ideaSet the threshold by bisection against the quantity actually specified, the fraction of cells that fire after inhibition, measured on probe compositions.

What it boughtThe learning fly then beat its own frozen twin on every seed: +4.68 ± 1.40, Wilcoxon p = 0.0039, 8 of 8 seeds, against +0.45 ± 0.51 (p = 0.40) with the starved code. The result repeated on eight fresh seeds, +5.02 ± 0.90 (E61). It was measured before the 19 September fix that stopped the reward depending on process history, so it is a within-run comparison, not an identical-reward one.

Verified by

The probes fire at 10.04 % after calibration. The difference between compositions in the Kenyon layer rose from 1.43 to 4.99, and the held-out correlation between the circuit's score and its reward from 0.291 to 0.560 (E61).

Builds on

Sparse Kenyon-cell coding held in place by feedback inhibition from the APL neuron (Lin et al., Nat. Neurosci. 17, 559, 2014). Neither the gain nor the threshold is in the connectome; setting them against the evoked code is ours.

The problemThe ladder's numbers rest on a handful of identities: the 2T convention, detailed balance of the swap move, the SRO decode, the Warren–Cowley bound, the label algebra and the evaluator's fold. A proof about an idealised formula can hold while the code does something else, and a test can pass on the wrong formula.

The ideaState each identity in Lean 4 with Mathlib, over the reals with explicit hypotheses, and tie each theorem to a pytest of the production function that computes it, so the proof and the code answer to the same statement. An audit test refuses sorry, admit, new axioms and native_decide.

What it boughtSix modules are checked: Temperature, DetailedBalance, SroDecode, WarrenCowley, VolumeMiss and FeatureFold. No proof found the code disagreeing with the mathematics. One proof explains why a check matters: a volume minimum found at the edge of the searched bracket says nothing about what lies beyond it, which is why every label carries a flag for that case. All 5,836 labels of E238 have an interior minimum.

Verified by

An adversarial review of the statements checked their fidelity to the code, checked for vacuity with compiled witnesses, and mutated the code (4 of 4 mutations caught). It found two overclaims, both fixed (E238).

Builds on

Lean 4 (de Moura & Ullrich, CADE 2021) and Mathlib (The mathlib Community, CPP 2020). The theorems are standard mathematics; the tie to the production code is ours.