QuantumFluids: a machine-checked Lean 4 library of quantum-fluid structure, applied to published neutron-scattering work

Abstract

An open Lean 4 / Mathlib library of 235 machine-checked theorems on the mathematical structure of quantum fluids, with the accompanying paper. Contents. Correctness of the phase-winding algorithm by which Gross-Pitaevskii codes locate quantized vortices, including its exact failure case (a phase step of exactly pi, where the antisymmetry that codes routinely assume is false); quantization of circulation, with the quantum shown to be attained; the discrete divergence-free condition that makes vortex-line tracing well posed (our own tracer had assumed it without proof); the Galerkin-truncated Gross-Pitaevskii nonlinearity on an arbitrary finite mode set; the Madelung decomposition; a bridge into the vocabulary of OpenAI's Lean formalization of the Navier-Stokes problem, imported as a real dependency; and two modules addressed to published experiment. Applied to published work. HeliumKinematics formalises identities the neutron-scattering analysis of superfluid helium-4 by Godfrin et al. (Phys. Rev. B 103, 104516) rests on: three-phonon decay is kinematically open if and only if the dispersion is anomalous; two rotons carry total momentum in [0, 2k_R]; and any comparison of the dispersion with twice the roton gap is invariant under recalibration. From the published coefficients this yields three distinct closing thresholds (0.404, 0.455, 0.566 inverse angstrom) that are usually quoted as a single k_c. BoseIntegral verifies the leading coefficient of that paper's specific-heat series -- the series for which it reports that earlier published versions contain errors -- from the Bose integral pi^4/15 through to A = 0.0831 J/(mol K^4), matching the printed value. The Bose integral is now proved at every natural order, which surfaced a structural fact about that series: two of its six coefficients carry zeta(7) and zeta(9), which have no known closed form, so those two can never be adjudicated by exact algebra -- only numerically. This is not a physics-discovery deposit. Two results once regarded as findings were withdrawn after a literature check (RETRACTIONS.md), and a topological hypothesis was refuted by simulation. The paper is organised around what formal verification does and does not buy in physics: it caught a false lemma, an inequality that prose had turned into an equality, a constant voiding a bound in the limit that mattered, eleven theorems that had escaped audit, and a lemma exempted from independent checking by a visibility modifier. It could not tell that a correct theorem was already known, nor that a hypothesis was naive. Run in the other order the literature search is cheap, and it later stopped a further proposal before implementation by showing that 0-dimensional persistence of a dispersion minimum is exactly its topographic prominence. Reuse. import QuantumFluids (Lean 4.34.0-rc2, Mathlib tag v4.34.0-rc2). VortexWinding, QuantizedCirculation, GPGalerkin, HeliumKinematics and BoseIntegral depend only on Mathlib. Code: MIT OR Apache-2.0. Paper and documentation: CC BY 4.0. New in v1.5.0. The six-coefficient phonon specific-heat series of Godfrin et al., PRB 103, 104516 (2021), Eq. (22), and its printed inverse dispersion series, are derived independently and machine-checked end to end (PhononSeries, PhononSpecificHeat): all coefficients are confirmed. Truncation is stated as nilpotency in an arbitrary commutative ring, with computer-algebra certificates checked by the kernel. The paper gains a related-work section and is revised as an experience report for a formalization venue. New in v1.6.0. Second paper, Known answers first (paper/kinetic_known_answers.pdf): a computer-assisted certified enclosure of the Landau damping root (k=0.5: ω=1.4156618886… − 0.1533594669…i), a Vlasov–Poisson solver validated against it, a closed-form plasma echo, Lean proofs that undamped zero sound exists iff F0s>0 in 2D and 3D, and persistent-homology instruments that were pre-registered and refuted (14 of 25 criteria met). No new physics is claimed; nonlinear Landau damping is formalized in Lean by Bedrossian (arXiv:2609.16801). Library: 145 theorems, all accepted by two kernels. New in v1.7.0. Third paper, A Lean 4 tribute to Cédric Villani (paper/villani_tribute.pdf): a full, sorry-free Lean 4 proof of Ollivier and Villani's discrete Brunn–Minkowski inequality on the hypercube (SIAM J. Discrete Math. 2012, Theorem 1 at zero curvature); a corollary of Mathlib's Data Processing Inequality, stated explicitly as not a contribution; a survey, checked against the pinned Mathlib, of what in Villani's work is and is not formalizable today; and a literature gate that stopped a Pomeranchuk/Penrose stability proposal before any code was written. Library: 161 theorems in 19 modules, all accepted by two independent kernels. New in v1.9.0. Fifth paper, How loose is Wasserstein stability on a vortex field? (wasserstein_slack.pdf): the Skraba–Turner cellular bound W_p ≤ ||f−g||_p computed exactly on both sides for the seven closed-loop pairs, certified by dual potentials, and found vacuous on all seven (bound / triangle-inequality bound = 139–3200 at p=1, minimum over p never below 2); the mechanism measured (cells per bar); a pre-registered prediction that failed, reported as failed; an erratum to the previous paper's phase-space certificate; the BKT and Fricke/K3 directions taken to their gates and stopped, with Dolgachev's theorem read in full (verdict: the same involution without the group). New Lean module Fricke (12 theorems): the Fricke matrix normalizes Mathlib's Gamma0(n), its axis action is DualLength's involution — group theory only, no physics claimed. Library: 181 theorems, 21 modules. New in v1.8.1. Fourth paper, Closing one loop (paper/closed_loop.pdf): a pre-registered test of the Cohen–Steiner–Edelsbrunner–Harer stability theorem on seven pairs of real 2D Gross–Pitaevskii density fields — it holds on all seven and is vacuous on six, the mechanism that refuted this project's earlier vortex detector, now measured; a Wasserstein-1 distance between persistence diagrams certified on every pair by an explicit primal transport plan and explicit dual (Kantorovich–Rubinstein) potentials, with the general finite LP weak-duality theorem and one hand-verified instance proved in Lean 4 (WassersteinCertificate); a pipeline-transmission bug found and fixed, reported as data about method; and three gated directions on duality (Lp-stability, the BKT transition, and where the project's older R↔α'/R involution belongs). Library: 169 theorems in 20 modules, all accepted by two independent kernels. New in v1.10.0. Two papers. Does topology causally influence physics? (paper/causal_topology.pdf): the question posed in the interventionist sense (descriptor / constraint / difference-maker); a machine-checked chain of 28 new theorems in three modules (TopologicalProtection: winding conserved by every continuous evolution without a phase slip, a change of winding forces a slip, XY-ring mountain pass and a positive barrier for n ≥ 10 that is false at n = 9; ScaleResolvedWinding: discrete Stokes, a bound pair invisible from every enclosing scale; ContinuumWinding: the sampled principal-branch loop sum equals the topological degree for every fine enough sampling, via Mathlib path lifting through R → R/2πZ and Heine–Cantor — closing the gap VortexWinding had declared unproved); and a pre-registered, energy-matched intervention in a projected Gross–Pitaevskii classical field: four injected vortex pairs versus the same energy as phonons, on three equilibrated bases — condensate lower by 0.49–0.73, coherence exponent 9–44× larger, the same energy 15–60× more effective as topology; the pre-registered composite claim is not made because its thermometer clause failed (the vortex arm is colder, read post hoc as the topology drawing heat from the bath, a sign that cannot explain the effect); eight imprinted vortices survive 1500 time units with zero annihilations; a heating ladder locates the stiffness jump at TBKT = 0.821 (L = 64) with η = 0.31, confirms η·nsλ2 = 1 to 12–27% on eleven energies in two boxes, and shows a quench state with the same vortex count as an equilibrated one at half the stiffness (round 1's TBKT withdrawn). Topological charge as a measurement principle for astrophysical U(1) phase fields (paper/astro_topological_measurement.pdf): a methods paper — the chain as five measurement principles each with its hypothesis and named diagnostic, three settings (strings in simulations, neutron-star glitches, condensate dark matter), a protocol, a pre-registration template for the causal step with a matched control arm; no astrophysical number is claimed and the gauged-U(1) case is stated as not covered. Also new: QHFricke (the Fricke involution fixes the quantum Hall critical orbit but maps every plateau off the odd-denominator class). Library: 215 theorems in 25 modules, all accepted by two independent kernels. New in v1.11.0. Proposal paper Topological sectors carry their own temperature (paper/sector_temperature.pdf): the reading of v1.10.0's failed thermometer clause as Onsager's two-temperature picture (vortex gas and phonon bath weakly coupled; established by Gauthier et al. and Johnstone et al., Science 2019, and Groszek et al., PRL 2018 — no novelty claimed); its combinatorial core machine-checked in SectorTemperature (8 theorems: the global inverse-temperature factor is a mediant of the sector factors, so equal energy does not imply equal temperature once a conserved label exists; sectors invariant under no-slip evolution); a torus point-vortex thermometer (Weiss–McWilliams 1991) with its published known answers and a canonical Metropolis calibration; and two external tests whose predictions were written before the data were read: on the public vortex-position data of Gauthier et al. (Zenodo 2548958) the lifetime of the clustered configuration falls with the condensate fraction (direction confirmed, pre-set ratio threshold failed),