Which stored elastic tensors in JARVIS-DFT are not positive definite? An exact-rational Born-stability audit of 34,323 tensors (a statement about stored DFT tensors, not about materials)

An unstressed crystal is elastically stable only if its 6×6 stiffness matrix is positive definite (the Born criterion, as stated by Mouhat and Coudert, PRB 90, 224104). We tested every full 6×6 elastic tensor stored in the JARVIS-DFT dft_3d dataset (CC BY 4.0; figshare article 6815699; unzipped json sha256 9dacb55a…5907) with exact rational arithmetic. Of 93,902 records, 59,400 carry no tensor ("na"), 179 contain a non-finite number, and N = 34,323 are analysed. Reading each stored float as the exact rational of its shortest decimal and testing the symmetric part: 22,842 tensors are positive definite and 11,481 (33.45 %) are not, each with an exact rational witness x ≠ 0, xTSx ≤ 0. Three exact methods agree on every entry (the producer's LDLT and Bareiss elimination, and an independent auditor's characteristic-polynomial sign pattern), and the auditor re-checked all 11,481 witnesses. 234 tensors are numerically zero; without them 11,247 of 34,089 (32.99 %) are not positive definite. Under an exact worst-case rounding test (each printed value within half a unit of its last printed place): 22,809 robustly positive definite, 11,244 robustly not, 55 certified ambiguous, 215 undecided (210 of them null tensors). 342 tensors pass the incorrect linear orthorhombic criterion (Mouhat–Coudert Eq. 19) but are not positive definite. This is a statement about stored DFT tensors under one stated reading, not about materials. Many entries are raw DFT outputs, including hypothetical, unrelaxed and dynamically unstable structures, so a large fraction is expected. It does not say that JARVIS-DFT or its authors are wrong and says nothing about any material being unstable in a laboratory. The criterion tested is the zero-stress one (Mouhat–Coudert Eq. 20: under load the relevant matrix is B, not C), so residual stress in a computed cell changes the relevant test. To our knowledge no exact-rational Born audit of the whole JARVIS elastic dataset has been published (not an exhaustive search, not a priority claim). Tier split. Tier A (Lean 4.34.1, Mathlib, pinned toolchain; axioms within propext, Classical.choice, Quot.sound), provisional: 12 witnesses x ≠ 0 with xTSx ≤ 0 and 6 LDLT identities with positive pivots for 18 explicit dataset matrices, plus 2 control statements; three tampered certificates are rejected; independently recompiled and replayed with leanchecker by the auditor; the anse/formal/lean_runner.py gate and a statement-lock entry are still owed, and the step from the LDLT identity to positive definiteness is outside Lean. Tier L: the criterion (Mouhat–Coudert), the dataset and its licence; Born–Huang (1954) was not read. Tier C: all exact counts (exact rational arithmetic on the stored decimals; not kernel-checked). Tier X: float pipelines (numpy eigvalsh with and without tolerance disagrees on 0, 236 and 3 tensors for three conventions) and context counts; the producer's ehull bins are withdrawn because the field's meaning was not verified. Controls. Positive: Cu, Si and diamond tensors are positive definite; the Mouhat–Coudert footnote-26 tensor passes the incorrect linear criterion and fails the exact test; stored values of five materials reproduce a published table; Voigt K and G recomputed from the tensors match the stored moduli within 1 % for about 98 % of entries. Negative: sign flips flip the verdicts; singular and near-boundary tensors are flagged undecided; planted wrong Lean certificates are rejected. Dataset observations, neutral. 234 numerically zero tensors, 12 with a zero row, 922 not exactly symmetric (598 differ by more than 1 GPa, median 19.5 GPa), 874 with over-precise entries, 18 entries above 1e4 GPa. The owner has not forwarded these to the dataset authors. Redistribution. No dataset file and no per-entry table is included (the dataset is fetched from figshare by hash); 22 dataset tensors appear in a Lean file and a json file, each with a CC BY 4.0 attribution line (Choudhary et al., npj Comput. Mater. 6, 173 (2020)). The derived summaries, code and Lean files are released under the licence of this record; they do not enlarge the dataset's licence. Member list: BUNDLE_MANIFEST.txt. Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. Independently audited by a separate AI agent instance (ACCEPT_WITH_CORRECTIONS, corrections C1–C10 applied; full re-classification of all 34,323 entries with 0 mismatches); no human audit. Still unverified: the lean_runner gate and a statement lock, the meaning of the ehull and min_ir_mode fields, Born–Huang 1954, a re-run of the producer's controls.py by the auditor. The Elenchus ledger gate exits with code 1 (0 blocking findings, 2 flags LEDGER_UNAUDITED_TIER_A). Not peer reviewed.