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
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.
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.
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.
Classical-field (projected Gross-Pitaevskii) simulations of two-dimensional Bose fluids are usually scripts whose correctness is checked, when at all, by a few conservation laws. We describe qf-pgpe, the quantum-fluids module of the rusty-SUNDIALS numerical library: a pure-Rust integrating-factor RK4 engine for the projected equation on a periodic grid, a vortex instrument (periodic theta-function imprint, sub-grid detection, tracking), the registered estimators of vortex friction and diffusion, a thermal-state toolkit, a vortex-phonon scattering instrument, and a Python extension (pyo3, numpy) with a drop-in stepper. Every module is a port of a Python original of an ongoing pre-registered research programme and carries a numeric cross-check against it: estimators agree to 2e-14 on real vortex tracks, a 31-run scattering matrix to 5e-11, measurements on a shared thermal field to 1e-14; the engine is checked against known answers and against rusty-SUNDIALS' own CVODE (global error falling as dt^4.00). The cross-checks found three defects, one of them in the Python programme: its primary estimator of the mutual friction is biased low by vortex diffusion (-8 to -22 %), a flaw the registered synthetic gate had not shown. On one thread of a 2013 laptop CPU the engine is 4.3, 4.2, 2.7, 2.5 times faster per step than the numpy engine at N = 64, 128, 256, 512 (3.2 to 1.5 times against the fastest Python engine tried, torch on CPU), and the drop-in extension makes an end-to-end thermal-state measurement 5.3 times faster with identical results. No claim is made about GPU codes or other published solvers, which were not measured. Version 2 adds the first reproduction of an external, published solver run (Kwon and Shin, flow past a penetrable obstacle: a different scheme and precision): the initial field is reproduced to 2.8e-8, the force on the obstacle to 2e-4 over 10 time units, and the vortex counts at 9 of 10 times up to t = 50, with the disagreements stated (force differences of 0.19 % of the maximum once the wake forms; one count differs by one). It also reports a JAX/XLA row (checksums equal to 1e-13; faster than the single-threaded Rust step at N >= 256 only because it uses threads; pinned to one core Rust is 1.1-1.8 times faster) and an optional, bit-identical intra-step threading mode of the engine (2.4 times at N = 512, measured on a loaded machine).
We obtain ab-initio estimations of the dynamic structure factor, S ( q ,ω), of Bose gases at zero temperature. More precisely, we use the Genetic Inversion via Falsification of Theories (GIFT) algorithm to perform analytic continuations of imaginary time correlation functions computed via an exact Path Integral projector method. Using the hard-sphere potential to model the two-body interactions between the atoms, we compute S ( q ,ω) changing the gas parameter from the dilute regime ( na 3 = 10 −4 ) up to the density corresponding to superfluid 4 He at equilibrium ( na 3 = 0.2138). With increasing density, we observe the emergence of a broad multiphonon contribution accompanying the quasiparticle peak and a crossover of the dispersion of elementary excitations from a Bogoliubov-like spectrum to a phonon-maxon- roton curve. Apart from the low wave vector region, for na 3 = 0.2138 the energy-momentum dispersion relation and the static density response function, χ( q ), turns out to be in good agreement with the superfluid 4 He experimental data at equilibrium density.
This paper is the forty-second in a sequence developing an interpretive framework that redescribes physical reality as a causally consistent history of information updates rather than as a collection of independently existing objects. It is the recovery panel of the twelfth grouping — the U3 construction program — and it adopts nothing new. Paper 41 adopted, at the claim level L3-A defined there, the common record-history kernel P_ker (one classical-quantum GKSL-type generator whose fixed Lindblad operators are export-event operators driven by a classical, adapted record-export intensity), computed a nonempty admissible coefficient space, and left four obligations to this paper: the recovery conditions RC1/RC2a/RC2b and the single calibration RC3, under a binding ledger (one calibration, spent on lambda_dec only; lambda_diff carried as a gate-bounded prediction band; thresholds never re-tuned). This paper executes them. RC1 is proved as a theorem: in any sector containing no certified export channels, the kernel's matter/order dynamics is exactly unitary — a sector statement, not a coefficient limit, and not a claim that unexported mass ceases to gravitate. RC2a is proved as a bounded-residual theorem: the Newtonian baseline drift is fixed by definition to the imported Newtonian classical-quantum mean dynamics, the export correction is shown to be cell-mean-zero by the decomposition bookkeeping (with the adopted sourcing law's first moment checked — a real failure mode, not realized), and the residual mean-source shift is dipole-suppressed below every declared class tolerance delta_g(class); the honest status row records that no current class co-locates audited export density with a Newtonian-verification measurement, so the world-side probe is today bounded, not probed. RC2b is split in advance: an executed compatibility check — the Jacobson-route hypotheses of Paper 36 reduced row by row to declared criteria with declared tolerances, of which the normalization row is satisfied (G an input, never an output), the entropy-monotonicity row is satisfied under a displayed record-basis pinching condition, and the local-equilibrium and Clausius-defect rows are fixed as criteria whose concrete exhibition and evaluation are assigned to Paper 43's audit program (no row failed; the which-entropy circularity imported as a live defect) — and a typed covariant debt (relativistic microcausality, dressed sources, species), named and not discharged. RC3 is spent exactly once, on the single calibration benchmark declared before any dephasing datum was consumed: the measured measurement-induced dephasing of a dispersively read superconducting qubit (Schuster et al. 2005; channel model Gambetta et al. 2006). The audit is non-vacuous by construction: certified exports are the output-port photons insofar as their field modes are amplified into the retained quadrature record at the declared grain — the certified intensity is nu_eff = eta_cert kappa nbar with eta_cert = eta_ext eta_rec, the output coupling times the record-chain efficiency, both declared as intervals — and the per-event pointer-overlap deficit is computed from the device's spectroscopic parameters (2 chi / kappa = 1.0, so the which-state information is fully exported per photon). The declared linear fit proves mathematically inapplicable at this device's measurement strength, so the extraction is executed as a documented protocol-deviation conservative bound — a declared-tolerance ceiling read against the source's own validated line-shape model, from text-stated quantities only, with a full sensitivity table — and the source's data show no excess dephasing beyond that model: the calibration returns not a point but the pre-declared gate-truncated band Lambda_cal = [5e-5, 2.1], computed at the conservative corner of the declared inputs (including the record-chain efficiency) so the dominant systematics sit inside the band; the two bookkeepings of standard budget and kernel excess are ledger-distinct while the physical carriers may overlap. The band is nonempty, so the normalization survives: lambda_dec is bounded above, for the first time, by a declared-tolerance reading of laboratory line-shape data (a factor of five below Paper 41's illustrative interferometric ceiling at the most conservative record-chain reading, tightening to a factor of fifty under the architecture-level reading), lambda_dec = 0 is never carried (the trade-off floor truncates from below), and the normalized kernel — the lambda_dec band, the lambda_diff prediction band, the computed order coefficient, the unchanged thresholds — is handed to Paper 43. The retired authority is the Global Reducer: the demand that an adopted dynamics earn its standing only by a globally certified exact reduction of the established theories. Its methodological face falls to the construction — exact-but-sector-relative unitarity, on-average Newtonian sourcing over declared classes, imported-route compatibility at declared order, and declared-calibration normalization are how correspondence is legitimately held; its substantive face (one true global reduction) is declined, not refuted. Every result is conditional on P_ker; the calibration datum is spent, never scored; no gate is crossed and no U3 is claimed.
The best known lower bound for the minimum Kochen-Specker vector system in R3 -- 24 vectors -- rests on a computational proof whose combinatorial half emits DRAT proofs but whose geometric half does not: the non-embeddability of thousands of candidate graphs is established by Z3's nonlinear real arithmetic, which produces no checkable proof objects. We close this gap for the proof's blocking database. We introduce exact rational case-tree certificates of real non-embeddability, whose splits are polynomial factorizations and rational sum-of-squares decompositions and whose leaves are discharged by injectivity, ideal-membership, or Positivstellensatz-shaped positivity arguments, and we certify all 291 source lines (180 distinct graphs) of the published pipeline's order-10 to order-13 blocking lists. Certificates are replayed by two independent checkers that share no code with the generator: a pure-Python replay over exact fractions, and a total checker implemented and proved sound in Lean 4. The soundness theorem -- acceptance implies that no injective-on-rays, orthogonality-respecting assignment of nonzero real vectors realizes the graph -- is kernel-checked with axiom closure {propext, Classical.choice, Quot.sound}, and a gcd-free rational arithmetic layer makes the entire verdict computation kernel-reducible, so each per-graph non-embeddability result is a closed kernel theorem proved by decide. The formalization surfaced findings about the published pipeline, including a load-bearing injectivity side condition in its embeddability notion, hidden WLOG case obligations invisible to Z3-based workflows, and an unreproducible candidate count that we resolve against the published artifacts. All certificates, checkers, and proofs are available and replayable from a single build.
We show that Bogoliubov theory correctly predicts the low-energy spectral properties of Bose gases in the Gross-Pitaevskii regime. We recover recent results from \cite{BBCS,BBCS4}. While our main strategy is similar to the one developed in \cite{BBCS,BBCS4}, we combine it with new ideas, taken in part from \cite{Hainzl,NT}; this makes our proof substantially simpler and shorter. As an important step towards the proof of Bogoliubov theory, we show that low-energy states exhibit complete Bose-Einstein condensation with optimal control on the number of orthogonal excitations.