An independent partial check of the three-dimensional Yukawa bcc-to-fcc threshold of Luo and Wei: the threshold reproduced three ways, seventeen Lean statements kernel-checked, and what remains open

Luo and Wei (arXiv:2610.31456) prove that for unit-density point charges with screened Coulomb (Yukawa) repulsion e−κr/r, the body-centred cubic (BCC) lattice minimises the energy among all three-dimensional lattices for κ < κ*, the face-centred cubic (FCC) lattice for κ > κ*, with κ* ≈ 1.7179218684699. The credit for that result belongs to them. This note is an independent partial check of the computer-assisted finite part of their proof, not a refutation: every printed number and inequality that we could check holds, and we found no discrepancy. A step-by-step account for non-specialists explains the bcc/fcc question, what a certified threshold means, and how the finite lemmas are checked, with the Lean statement beside each step. Tier split. Tier A (Lean 4.34.1, pinned Mathlib; axioms within propext, Classical.choice, Quot.sound; leanchecker replay rc 0 on Basic, Shells, Chains, LemmaA5, Lemma61, run by the producer and again by an independent AI audit on privately rebuilt, byte-identical oleans; all 138 declarations of the five modules print only these axioms; no human audit; no statement lock): seventeen Lean theorems (ten substantive; seven are one-line rational facts or bridge lemmas, and lemma61_prop41_bracket is a for-all-x inequality, not a finite statement): the FCC shell multiplicities N1..N12 and the 17 nonzero BCC multiplicities Mℓ (ℓ ≤ 48), proved equal to the count over all of Z3; Lemma A.5 (A.6), (A.7), (A.8) as real-number statements over Real.pi and Real.exp; the constants and tails of the proof of Lemma 6.1; the rational tail of the proof of Lemma A.6; the rational step of Lemma A.1. Several Lean statements are weaker than the printed ones (exp_fcc_21 only at t = 21/10; prop41_bracket only the rational bracket; tail_* only partial sums of the rational majorant; lemmaA5_* over box counts linked through the *_eq_ncard lemmas); the paper tabulates them. Tier L: the paper's own statements, taken as stated. Tier C: Arb ball arithmetic (Lemma A.6 for G = 2(EB − EF) at κ = 1.717921868469903 and 1.717921868469904 and at neighbouring controls; the Lemma A.5 minimum slacks 7.52e-4 and 7.65e-5; Lemmas A.1 and A.3) and three independent reproductions of κ* (Ewald sums in Arb at 320 bits; a direct real-space Arb sum; mpmath quadrature of the paper's integral equation (1.4) at 40 digits), where (E) and (Q) agree to all 25 printed digits and the interval of (D) contains both; the audit added a fourth value (classical Ewald split with a free splitting parameter, 70 digits): 1.71792186846990386425087416660628171879468538, and an independent python-flint 0.9.0 run reproduces both Lemma A.6 signs. Our IEEE-double direct sum reaches 11 digits; double precision cannot resolve the 1e-15-wide enclosure (a float64 Ewald reaches about 12 digits). Tier X: the double-precision value and the repository guard outputs. Controls. Positive: the three reproductions of κ*; shell counts re-enumerated by brute force. Negative: a planted wrong multiplicity N7 = 46, a tampered table entry and a tampered cell bound are all rejected by the kernel (rc 1); a witness file shows the kernel evaluates the tampered checks to false and N7 to 48; a planted sorry and a planted axiom are caught by the axiom audit although the file compiles. Lemma A.3 (A.4): three exponential bounds hold by about 2e-16; the endpoints are outward-rounded (numerators 4.2, 1.05 and 2.5 units beyond the exact logarithms, in the safe direction), 11/25 and 147/1000 are intermediate rationals with slack in Prop. 3.1, and only the bound for beta is tight; not an error. Not done. The assembly of Lemma 6.1 (theta functions as lattice sums, Poisson summation for D(1) = 0, Nn < 30n for all n) is not in Lean; Lemma A.4 (5,828 rectangles) and Lemma A.2 were not re-run because the partition data is not public (arXiv lists no ancillary files; we intend to ask the authors for the data); Lemma A.6 is not in Lean because the pinned Mathlib has no erfc. What this is NOT. This concerns the stated mathematical model of point charges with screened Coulomb repulsion on a lattice, not any real material. It is not a verification of Theorem 1.1 of Luo and Wei and not a refutation of it. Limitations. Partial; Lemma 6.1 not in Lean; the Lemma A.4 re-run is blocked; the Lean runs shared a core with another process and two earlier compiles were killed (probably out of memory); an independent AI audit (verdict ACCEPT_WITH_CORRECTIONS, no blocking item) rebuilt the five modules and replayed them with leanchecker (rc 0), but no human audit and no statement lock exist; the repository guards antigravity_guard.py, test_rigor_guard.py and pytest tests/ fail for pre-existing reasons in other lanes' files and are not claimed passed. Status. Produced by AI agents (Claude) under the author's direction; the author is responsible for the content. The Elenchus ledger gate exits with code 1 (0 blocking findings, 8 flags LEDGER_UNAUDITED_TIER_A, one per Tier A row; the flags stay because no person has certified the glosses; the AI audit reran the gate with the identical result).