The Bogoliubov structure factor under the dual-scale envelope sqrt(k/2k_s): kernel-checked shape theorems, a one-sided diffraction test, and a Gross-Pitaevskii linear-response check in rusty-SUNDIALS
- 1SocrateAI Lab
Abstract
For the zero-temperature weakly interacting Bose gas, the Bogoliubov static structure factor is SB = ε0/εB = k/√(ks2+k2), with ks = 2mc/ℏ. Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature, quoted verbatim), C (human argument, not machine-checked) and X (floating-point exploration, which never supports a claim). Tier A (Lean v4.34.0-rc2 in the QuantumFluids project environment, importing its DualLength module; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught). 26 statements about the model formulas: the envelope SB ≤ √(k/2ks), with equality exactly at k = ks; strict monotonicity; the two-sided phonon bound k/(ks+k) < SB < k/ks; SB < 1, 1 − SB ≤ ks2/k2, and SB → 1; a one-sided diffraction test: a structure factor above the envelope is not SB; and, given Feynman's inequality as an explicit hypothesis, the dispersion is then not Bogoliubov. The test's controls are kernel-checked: it fires on S = 1 and never fires on SB. The Bijl–Feynman identities hold by construction, because SB is defined as ε0/εB. Nothing in this paper depends on the openai/math release. A step-by-step human demonstration for undergraduates pairs each step with its Lean statement. Tier X: a new linear-response module in the rusty-SUNDIALS crate qf-gpe2d recovers the Bogoliubov dispersion from Gross–Pitaevskii dynamics to 4.1e-5 relative error. All 14 numeric gates pass, including g = 0 and splitting negative controls. We also found that the pinned upstream Python reference data are reproduced (to 2.5e-16) by a reused-phase composition, not by the symmetric Strang step; the upstream source itself was not inspected. The crate's own step/evolve use the same composition. In linear response its amplitude converges only at first order. A true Strang option fixes this. Real data: from the published 4He dispersion table (Godfrin et al., Tier L), the roton threshold is √(QR/2ks) = 0.5662. Assuming Feynman's inequality, the dispersion alone shows the test silent for k ≤ 0.90 Å−1 (Tier X evaluation). From 0.95 Å−1 upward, including the roton, it cannot decide. We do not claim that the 4He roton peak exceeds the threshold. HuggingFace (unmet deliverable): the task asked for a HuggingFace dataset to illustrate the result, and that was not delivered. 30 queries found no structure-factor dataset; the single neutron-diffraction hit is out of scope, and nothing was substituted. The published 4He table, which is not on HuggingFace, is the real-data illustration instead. Tier L here covers verbatim data values and quotes, which is looser than the Elenchus L tier (theorem statements only). No novelty is claimed in mathematics or physics: the core inequality is (k − ks)2 ≥ 0. Statement adequacy has been reviewed by AI agents only. The ledger gate reports 0 blocking findings and 8 flags (Tier A rows not audited by a person). The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content.
Related
- Shell structure and spontaneous decay of superheavy Z=124 isotopes with the deformed relativistic Hartree-Bogoliubov theory in continuum
- X2SBench: an open benchmark for evaluating crystal structure determination from powder diffraction
- Beyond the ETH envelope: exact two-resolvent fluctuation structure, projected microscopic closure, and rigid versus nonperturbative sectors
- Structure of niobium to 365 GPa using ultrafast x-ray diffraction and shock compression
- Covariant Gross-Pitaevskii-like equation for relativistic fermions
BibTeX
@misc{callens2026bogoliubov,
title = {{The Bogoliubov structure factor under the dual-scale envelope sqrt(k/2k_s): kernel-checked shape theorems, a one-sided diffraction test, and a Gross-Pitaevskii linear-response check in rusty-SUNDIALS}},
author = {Xavier Callens},
howpublished = {Zenodo (CERN European Organization for Nuclear Research)},
year = {2026},
month = oct,
doi = {10.5281/zenodo.23646116},
url = {https://doi.org/10.5281/zenodo.23646116},
note = {CC BY},
}
RIS
TY - UNPB
TI - The Bogoliubov structure factor under the dual-scale envelope sqrt(k/2k_s): kernel-checked shape theorems, a one-sided diffraction test, and a Gross-Pitaevskii linear-response check in rusty-SUNDIALS
AU - Xavier Callens
PY - 2026
DA - 2026/10/25
PB - Zenodo (CERN European Organization for Nuclear Research)
DO - 10.5281/zenodo.23646116
UR - https://doi.org/10.5281/zenodo.23646116
AB - For the zero-temperature weakly interacting Bose gas, the Bogoliubov static structure factor is SB = ε0/εB = k/√(ks2+k2), with ks = 2mc/ℏ. Every claim is filed in an Elenchus claim ledger with tiers A (kernel-checked Lean), L (cited literature, quoted verbatim), C (human argument, not machine-checked) and X (floating-point exploration, which never supports a claim). Tier A (Lean v4.34.0-rc2 in the QuantumFluids project environment, importing its DualLength module; axioms within propext, Classical.choice, Quot.sound; planted sorry and planted-axiom controls caught). 26 statements about the model formulas: the envelope SB ≤ √(k/2ks), with equality exactly at k = ks; strict monotonicity; the two-sided phonon bound k/(ks+k) < SB < k/ks; SB < 1, 1 − SB ≤ ks2/k2, and SB → 1; a one-sided diffraction test: a structure factor above the envelope is not SB; and, given Feynman's inequality as an explicit hypothesis, the dispersion is then not Bogoliubov. The test's controls are kernel-checked: it fires on S = 1 and never fires on SB. The Bijl–Feynman identities hold by construction, because SB is defined as ε0/εB. Nothing in this paper depends on the openai/math release. A step-by-step human demonstration for undergraduates pairs each step with its Lean statement. Tier X: a new linear-response module in the rusty-SUNDIALS crate qf-gpe2d recovers the Bogoliubov dispersion from Gross–Pitaevskii dynamics to 4.1e-5 relative error. All 14 numeric gates pass, including g = 0 and splitting negative controls. We also found that the pinned upstream Python reference data are reproduced (to 2.5e-16) by a reused-phase composition, not by the symmetric Strang step; the upstream source itself was not inspected. The crate's own step/evolve use the same composition. In linear response its amplitude converges only at first order. A true Strang option fixes this. Real data: from the published 4He dispersion table (Godfrin et al., Tier L), the roton threshold is √(QR/2ks) = 0.5662. Assuming Feynman's inequality, the dispersion alone shows the test silent for k ≤ 0.90 Å−1 (Tier X evaluation). From 0.95 Å−1 upward, including the roton, it cannot decide. We do not claim that the 4He roton peak exceeds the threshold. HuggingFace (unmet deliverable): the task asked for a HuggingFace dataset to illustrate the result, and that was not delivered. 30 queries found no structure-factor dataset; the single neutron-diffraction hit is out of scope, and nothing was substituted. The published 4He table, which is not on HuggingFace, is the real-data illustration instead. Tier L here covers verbatim data values and quotes, which is looser than the Elenchus L tier (theorem statements only). No novelty is claimed in mathematics or physics: the core inequality is (k − ks)2 ≥ 0. Statement adequacy has been reviewed by AI agents only. The ledger gate reports 0 blocking findings and 8 flags (Tier A rows not audited by a person). The work was produced by AI agents (Claude) under the author's direction; the author is responsible for the content.
ER -