The cold-start insight for direct air capture survives exergy accounting of the model's heats and works, but its size, and with full heat recovery its existence, depend on pricing the chilling of the feed air

McDannald et al. (NIST; arXiv 2501.04825) define an intrinsic capture efficiency ξ = ΔnCO2/Etotal for a sorbent in an idealised piston cycle and conclude that it is greatly beneficial to start cold. Their Etotal is a face-value sum of heats and works: the return step is set to zero and no ambient temperature appears. We asked whether the conclusion survives when every heat of the sorbent and its adsorbate is weighted by its Carnot factor against an explicit ambient temperature T0, their sub-ambient cooling is priced by refrigeration, and the return step is charged. Version 2, revised after an independent AI audit, also prices the chilling of the contacted feed air (2,500 mol of air per mol CO2 at capture fraction 1), which version 1 left out. Result. Our preregistered hypothesis H1 (the optimal start moves to T1 ≥ T0; prior 0.35) is refuted at the preregistered setting (T0 = 298.15 K, no heat recovery) both with and without feed-air pricing: 0 of 14 rows. (i) Base accounting (feed air not priced, ideal machines): for all 14 Pareto rows of Table 2 the exergy-optimal start lies at 200 to 236.75 K in all 9 informative variants (three ambients, three heat-recovery levels); the 9 purity-constrained variants are vacuous for every row, so 126 of 252 row-variants are informative. The cold-start benefit ratio is 10 to 818 at face value, 3.5 to 129 without recovery and 1.29 to 6.6 with full reversible recovery. (ii) Feed air priced, no recuperation, ideal machines, T0 = 298.15 K: without recovery a cold start still wins in 14 of 14 rows but at about 254 to 290 K (ratio 1.46 to 8.0; grid-dependent by one or two cells); with full recovery of the sorbent heats the optimum moves to ambient in 11 of 14 rows (297.25 to 297.75 K, advantage 0.07 to 0.35 %, below each row's printed uncertainty), and a start at least 10 K below ambient then loses unless a recuperator recovers more than 91 to 96 % of the air's cold; only VANNIK (two rows) and LETQAE01 keep a cold start for every recuperator effectiveness. The cold-start conclusion thus survives exergy accounting of the heats and works as published, but its size, and at full recovery its existence, depend on how the cost of chilling the feed air is priced. H2: no published ξ exceeds 1/Wmin (dataset maximum 11.259 μmol/J against 51.6). Retraction: version 1 reported five dataset entries with heat flows inconsistent with the second law; those flags were produced by our own Step-3 quadrature and vanish over all 15,161 paths under the published Step-2 rule. The revised numbers were computed by the producer. The feed-air scenario family was then independently re-checked on all 14 rows by a separate AI agent instance (ACCEPT_WITH_CORRECTIONS, corrections applied; no human review): the r = 1 move to ambient (11 of 14 rows, 297.25 to 297.75 K, margin 0.07 to 0.36 %), the eps* and eta_R* thresholds, the symmetric-degradation sign, the vacuity count and the M = 1e4 control reproduce; r = 0 optimum temperatures agree within one or two grid cells (255 to 290 K against 254 to 288 K); one row (FASJAL 8.186) lies at the 10 K boundary at r = 0; some sizes (the 313.15 K loss 0.2 to 0.6 % against 1.2 to 1.7 %, the M = 100 control count 7/8/14 against 6/6/14) are grid-dependent. Tier split. Tier A (Lean 4.34.1, Mathlib; axioms within propext, Classical.choice, Quot.sound): twelve elementary real-algebra lemmas in DacExergy/Core.lean, three of them bare identities; they certify no number of the paper; independent recompile and leanchecker replay rc 0; no statement lock. Tier L: the source paper's model (eqs. 1 to 10, Table 2) and the dataset and code licences (data: Zenodo 10.5281/zenodo.14452152, CC-BY-4.0; code: NIST IntrinsicDACCycle v0.0.2, NIST software licence; arXiv non-exclusive distribution licence). Tier C: closed-form thresholds and mpmath-interval enclosures about a stylised two-component surrogate only; the surrogate has the wrong sign on most Table 2 rows at full heat recovery. Tier X: the full-model re-accounting, the grid scans and scenario families, the sample and the dataset-wide checks; the headline is Tier X. Controls. Positive: Table 2 reproduced in 14 of 14 rows to the printed digits from the stored posterior means; stored terms to 3.8e-11. Negative: four planted gate errors rejected; new in v2, an H1 negative control (refrigeration weighted x104) returns a warm optimum in 14 of 14 rows. What this is NOT. Thermodynamic limits of a published simplified model (idealised piston, Henry/IAST loadings, binary CO2/N2 air, no water). Not a statement about real plants, costs, sorbent performance in practice or any climate effect; no recommendation; not an unconditional 'cold start survives'. It does not say the NIST metric or its authors are wrong. Redistribution. This bundle is built from a staging copy and contains no third-party full text, no NIST code tarball or source tree and no dataset files (the 51 CC-BY-4.0 files are fetched by script from the public Zenodo record 10.5281/zenodo.14452152): only names and sha256, licence notes, and our own code with the NIST notice and change notices; Lean: DacExergy/Core.lean and Controls.lean only. Member list: BUNDLE_MANIFEST.txt. Earlier commits of the public GitHub repository contained such files; the paper text and the NIST code were removed from the tracked tree on 2026-10-27, while 51 CC-BY-4.0 dataset files remain tracked there (redistribution with attribution is permitted by their licence). Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. Independent AI audits (a separate AI agent instance each time, not a person; no human review): v1 and v2 both ACCEPT_WITH_CORRECTIONS, corrections applied. The Elenchus ledger gate exits with code 1 (0 blocking findings, 5 flags LEDGER_UNAUDITED_TIER_A). Not peer reviewed.