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.
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.
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.
A quantized vortex in a thermal two-dimensional Bose gas is dragged by the normal fluid (friction α), pushed sideways by it (transverse coefficient α′) and kicked by it (diffusion η). We measure the three coefficients in the projected Gross-Pitaevskii equation — microcanonical, no damping term, no noise put in by hand — with sub-grid vortex tracking and estimators that are identities of the dissipative point-vortex model, machine-checked in Lean 4. Every hypothesis, gate and decision rule was committed before the corresponding run; the instrument failed its T = 0 control twice before it passed, an earlier gate verdict built on the flawed instrument is withdrawn, and both are reported. Results. At T/TBKT = 0.14, 0.27, 0.43: α = 0.0062(4), 0.014(2), 0.02(1), size- and estimator-independent, α ≈ 0.24 ρn/ρ. α′ is zero within 1% once the T = 0 compressible pair speed is subtracted; the Iordanskii value ρn/ρ is excluded at 18σ and the registered Iordanskii-like prediction is refuted. The Einstein relation is inconclusive by the registered rule (one admitted temperature at ηK/α = 2.1 ± 0.7; informally 1.4-3x, not 100x). Single pairs stop shrinking while the phonon band takes the impulse they shed (a self-generated counterflow with a published precedent in the truncated GPE); the decisive box-size control is not run. The single non-equilibrium pair that corrupts the superfluid-stiffness estimator in finite boxes decays by 4-27x given Lz-scaled time (six of six L = 192 trajectories admitted, one unfinished at t = 14 500). The pre-registered mode-by-mode dielectric relation fails in the thermal pair gas (coherence 0.06-0.28), while the vortex-charge structure factor equals the Kosterlitz-Thouless polarisability Σd2 from the measured pair sizes to 5-21%. The Josephson offset ηK − 1 = +0.3 survives at L = 192 in equilibrium, independent of fit window and torus geometry. Formal companions (Lean 4 / Mathlib, standard axioms): energy dissipation of any skew-plus-gradient vortex flow, the d2 law and lifetime bound, the centre-velocity identity, the wind stall, the zero-flux/Einstein equivalence, the pair-polarisation form and response ceiling, the charge-density/matching bound, the Kosterlitz-flow invariant, the bounded increments of quasi-periodic signals. Pre-registrations, amendments, gate records, data and code are in the software repository (concept DOI 10.5281/zenodo.22855581). No physics is claimed as new; the numbers, the refutations and the method are.
Depuis la description de la condensation d'un gaz de boson refroidit à 0K par Bose puis Einstein au début du XXe siècle, de nombreux travaux mathématiques, physiques et numériques ont été dédiés à l'étude des condensats de Bose-Einstein, et plus généralement de la superfluidité. Nous proposons dans cette étude des outils numériques dédiés à l'étude des excitations dans les condensats, ainsi qu'un modèle de la friction mutuelle dans l'hélium-II. Le modèle de Gross-Pitaevskii, consistant en une équation de Schrödinger non-linéaire, est utilisé pour décrire les superfluides. Des algorithmes basés sur les éléments finis, accompagnées d'une implémentation via le logiciel FreeFem++, sont proposées pour identifier les vortex dans des simulations numériques 2D et 3D ainsi que dans des images expérimentales. Diverses propriétés des vortex identifiés sont calculées: rayon des vortex, spectre de Kelvin, courbure, etc. Le problème aux valeurs propres de Bogoliubov-de Gennes, décrivant la stabilité d'un état stationnaire grâce à une linéarisation de l'équation de Gross-Pitaevskii autour de cet état, est ensuite étudié en couplant une méthode de Newton pour la recherche de l'état stationnaire et une bibliothèque de calcul de valeurs propres (ARPACK ou SLEPc) pour la résolution de l'équation de Bogoliubov-de Gennes. Deux codes FreeFem++ utilisant l'adaptation de maillage, l'un séquentiel, l'autre parallèlisé avec PETSc, sont proposés. Leur fonctionnement est validé sur des cas tests issus de la littérature pour des condensats à une et deux composantes. En ce qui concerne la friction mutuelle dans l'hélium-II, un modèle phénoménologique couplant les équations de Navier-Stokes et de Gross-Pitaevskii est proposé. Ce modèle est implémenté dans un code pseudo-spectral Fortran parallélisé et testé en deux et trois dimensions sur des exemples où des résultats analytiques dans le cas d'un couplage dans une seule direction permettent la détermination des paramètres numériques. Des résultats connus sont retrouvés pour valider le travail de modélisation effectué et des simulations de structures formées de trois anneaux de vortex et de reconnection de lignes de vortex sont réalisées.
Version 1 (first deposit, 2026-08). 19 pages. Every quantitative claim traces to a pre-registered evidence block with an archived log in the companion zip; the ledger of failed predictions is an appendix of the paper. A long-running dispute asks whether a quantum world selects its own decomposition into subsystems from the Hamiltonian and the state alone. Stoica (Adv. Theor. Math. Phys. 26, 3895 (2022)) proves that a structure so constructed cannot be both essentially unique and physically relevant, the non-uniqueness being modulo the unitaries commuting with H; Soulas, Franzmann and Di Biagio (arXiv:2512.07468) object that producing a second structure that way modifies the input pair, and prove a positive uniqueness theorem under two hypotheses. Both are correct, about different groups, and this paper makes the difference arithmetic. Working inside the collision architecture of the companion flagship (doi:10.5281/zenodo.22014601, all versions), where an interior memory writes records of a system and audits itself from them, the two invariance groups an interior audit actually has are measured. FIRST, the audit's Hamiltonian-side content is exactly constant on the orbits of the commutant of H, the fibres of the transport map are exactly those orbits, and the resulting gauge has the closed form sum_i m_i^2 - 1 in the eigenvalue multiplicities: the degeneracy has a computable size, three dimensions inside sixteen for a generic four-level Hamiltonian, five at (2,3), and larger exactly when the symmetry group is NON-ABELIAN (Heisenberg gives nine; abelian symmetry forces no spectral degeneracy). SECOND, the audit's total content is invariant not under that commutant but under the stabiliser of the PAIR (H, psi), which is trivial precisely under the Soulas hypotheses: the orbit holds the Hamiltonian side fixed to 2.7e-15 and pays for the second structure entirely on the state side, 1.14. The stabiliser formula quantifies exactly when their free-action condition holds and by how many dimensions it fails otherwise. THIRD, the record statistics carry their own blindness: the directions invisible to the census, whatever the state and the time, form a group, and for a register read in one basis per cell it is exactly span{I, T} at every fragment count, proved by a symplectic argument over F_2 requiring no induction -- in this deposit, by two algorithmically independent F_2 implementations plus a dense-matrix verification. That scope is the result rather than a caveat: the one-bit blindness is the price of a one-basis readout, and it is the only thing that price buys; reading a second basis on every cell collapses the group to the identity and credentials the full matrix algebra. The twist is the product of the observer's own precession with all of its own readouts, T = P R_1 ... R_k exactly, so the blindness group is the CENTRE of the credentialed algebra: an interior observer cannot see the centre its own operations generate. The credentialed algebra is everything commuting with that one bit, of dimension d^2/2. Blindness under this reading is an identity and not a similarity: for T in the blindness group the census under rho and under T rho T-dagger agrees exactly at trace distance 0.740, so no additional sampling can separate them. The paper prints the response functional every margin and census count is computed from, together with its grid and state. Around the group sit its measured collapse conditions: the price list of restorations (menus that eject the twist restore visibility at costs that double register by register, 10/20/40 contexts on the z-menu and 4/8/16 on the y/z-menu at k = 2, 3, 4, stated as observed at three points, not derived); the sorting condition for which twist configurations a restoration menu revives, named as reach membership of the displacement in the Krylov closure of the menu (63/63 exact at k = 2 in three independent engines, 255/255 at k = 3 in exact rational arithmetic; an all-time reach lemma proves the decision grid decision-faithful and shows it deliberately not span-complete); the genericity of visibility (the blindness locus is a union of alignment strata computed in part: a QND family at the minimal codimension 2 and twist families indexed by subsets of cells at codimension 2k, with a bounded search that surfaced a mixed partial-twist family the hand count had missed); and both branches of the open-world dichotomy reproduced from the group definition alone. The transport side is independently rebuilt: the W-alone computation the framework's kill switch depends on was reconstructed from the printed setting alone and the switch does not fire. A closing section isolates the mechanism shared with an earlier half-space result and shows, against the natural reading, that the two halves are distinct subspaces meeting in a quarter: one lemma, distinct instances. All quantitative claims were pre-registered before their runs. The ledger of failed predictions is an appendix and is kept in full, including a posted mechanism that died, a symmetry law corrected to Schur's criterion, a numerics trap caught only because a posted claim came back wrong, engine deaths from the exact-census campaign convicted by their own gates, and errors printed in earlier drafts and caught in review. The delineation of what is inherited from the literature is stated throughout; the paper asserts no priority claims.
Depuis la description de la condensation d'un gaz de boson refroidit à 0K par Bose puis Einstein au début du XXe siècle, de nombreux travaux mathématiques, physiques et numériques ont été dédiés à l'étude des condensats de Bose-Einstein, et plus généralement de la superfluidité. Nous proposons dans cette étude des outils numériques dédiés à l'étude des excitations dans les condensats, ainsi qu'un modèle de la friction mutuelle dans l'hélium-II. Le modèle de Gross-Pitaevskii, consistant en une équation de Schrödinger non-linéaire, est utilisé pour décrire les superfluides. Des algorithmes basés sur les éléments finis, accompagnées d'une implémentation via le logiciel FreeFem++, sont proposées pour identifier les vortex dans des simulations numériques 2D et 3D ainsi que dans des images expérimentales. Diverses propriétés des vortex identifiés sont calculées: rayon des vortex, spectre de Kelvin, courbure, etc. Le problème aux valeurs propres de Bogoliubov-de Gennes, décrivant la stabilité d'un état stationnaire grâce à une linéarisation de l'équation de Gross-Pitaevskii autour de cet état, est ensuite étudié en couplant une méthode de Newton pour la recherche de l'état stationnaire et une bibliothèque de calcul de valeurs propres (ARPACK ou SLEPc) pour la résolution de l'équation de Bogoliubov-de Gennes. Deux codes FreeFem++ utilisant l'adaptation de maillage, l'un séquentiel, l'autre parallèlisé avec PETSc, sont proposés. Leur fonctionnement est validé sur des cas tests issus de la littérature pour des condensats à une et deux composantes. En ce qui concerne la friction mutuelle dans l'hélium-II, un modèle phénoménologique couplant les équations de Navier-Stokes et de Gross-Pitaevskii est proposé. Ce modèle est implémenté dans un code pseudo-spectral Fortran parallélisé et testé en deux et trois dimensions sur des exemples où des résultats analytiques dans le cas d'un couplage dans une seule direction permettent la détermination des paramètres numériques. Des résultats connus sont retrouvés pour valider le travail de modélisation effectué et des simulations de structures formées de trois anneaux de vortex et de reconnection de lignes de vortex sont réalisées.