The Feynman-Bijl single-mode bound in Lean, and a diffraction test of the Bogoliubov envelope on published structure factors of superfluid 4He and trapped Bose gases

The Feynman–Bijl argument bounds the lowest excitation energy of a Bose fluid at wavevector k by ħ2k2/(2mS(k)), with S(k) the static structure factor. This preprint formalises its single-mode core in Lean 4.34.1 with Mathlib and applies the one-sided diffraction test S(k) ≤ √(k/2k*) (k* = 2mc/ħ) of an earlier preprint to published data. Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature; excerpts: prose as extracted, mathematics transcribed linearly), C (human argument, not machine-checked) and X (floating-point arithmetic or values read from a figure, which never supports a claim). Tier A (Lean 4.34.1 and Mathlib, pinned toolchain; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught; independently recompiled by a separate AI auditor with a private olean build, axioms identical, planted controls and two auditor mutations caught; no human audit): on a finite-dimensional complex inner product space with a symmetric H and an eigenvector ψ, the identity ⟨ψ,[ρ†,[H,ρ]]ψ⟩ = A(ρ) + A(ρ†) holds with no extra hypothesis. With the k ↔ −k symmetry and the f-sum value taken as hypotheses, the trial state ρψ/||ρψ|| has excess energy f/(2NS) and an eigenvector overlapping ρψ obeys λ − E0 ≤ ħ2k2/(2mS); a gap form gives 0 < λ − E0 under two further hypotheses. A kernel-checked counterexample shows that the symmetry hypothesis cannot be dropped from the halving step (A(ρ) = 1 ≠ 1/2 = f/2); that the final bound also fails in that example is a hand computation (Tier C), not a Lean theorem. A kernel-checked witness shows that all hypotheses hold together and the bound is attained. The Bogoliubov link (the Feynman energy from SB equals the Bogoliubov energy; SB ≤ √(k/2k*)) is re-proved on the pinned stack. The physics (f-sum rule from the canonical commutation relations, the symmetry, momentum conservation) is not in Lean. Tier X data analysis, Tier C reading: for 4He, 99 points of Table 14.1 of the Donnelly–Barenghi compilation (a secondary source; 1.4–4 K, not T = 0; no printed error bars) with k* = 3.00379 Å-1 from c = 238.3 m/s: 63 points refuted, 29 consistent, 7 undecided, all 21 points in the roton/peak region 1.7–2.4 Å-1 refuted by a factor 1.62–2.49. The refutation threshold (0.082, the gap between the two datasets' peak maxima) was defined after seeing the data and is a deviation from the preregistration; the strict-run endpoint (Q = 5.129 is refuted by 0.0830) and the counts above 2.4 Å-1 depend on its third decimal (refuted 60–64 for thresholds 0.07–0.10), while the roton-region result does not (smallest margin 0.328, about 4 thresholds) and also holds on the Donnelly–Barenghi recommended subset (X-ray for Q < 1, neutron for Q > 1). Read conditionally, this says only that 4He is not a Bogoliubov gas, which is textbook; no novelty is claimed for the physics or for the Feynman–Bijl argument. For trapped Bose gases only values read from figures exist (Tier X): the three absolute points of Stamper-Kurn et al. lie below a local-density-averaged bound with low test power (no ‘BEC consistent’ claim), and the Steinhauer et al. points were multiplied by 2.3 by the authors, so no decisive test is possible. A trapped-gas positive control shows that single-k* bounds fail their own control and only the LDA-averaged bound is valid. No rusty-SUNDIALS or LeanFlow change was made in this lane (the numerics are Python), so none is claimed. The Elenchus ledger gate reports 0 blocking findings and 11 flags (exit code 1), one for each Tier A row whose statement adequacy no human has audited. The work was produced by AI agents (Claude) under the author's direction and was audited by a separate AI agent (verdict ACCEPT_WITH_CORRECTIONS, corrections applied); no human has audited it; the author is responsible for the content.