Helium below 2.17 K behaves as two interpenetrating fluids at once: a normal component that carries entropy and viscosity, and a superfluid component that carries neither. Vortices in it are quantized — circulation comes in discrete units — and the force between a moving vortex line and the normal fluid has two parts. The longitudinal part is uncontroversial. The transverse part, written as the coefficient α′(T), has been argued over for more than half a century.
A sign nobody could settle.
Three positions have coexisted since the 1960s. Iordanskii (1965) derived a transverse force from the scattering of thermal excitations on the vortex. Thouless, Ao and Niu (1996) argued on topological grounds that no such force exists. Sonin (1997) defended a quasiclassical scattering picture with the opposite sign to what measurements near the lambda point appear to show. The experimental record — the classic Barenghi–Donnelly–Vinen tabulations — indicates that α′ changes sign at roughly 1.67 K, and no theory has produced that sign change from first principles.
If a controversy has stayed open for fifty years, the useful contribution is probably not one more candidate mechanism. It is a rigorous statement of which mechanisms are structurally incapable of producing the observed sign — decided against criteria fixed before the calculations were run.
Three parts, one method.
Part I reproduces the canonical unification of Landau–Khalatnikov two-fluid thermodynamics with Ginzburg–Pitaevskii–Sobyanin gradient theory, in the line running through Hills and Roberts (1977) and Geurst (1980): a nonlocal kernel, an Onsager dissipative extension, calibration against Donnelly–Barenghi (1998), a parameter-free microscopic check, and a 3D XY Monte Carlo determination of critical exponents. The Monte Carlo gives ν = 0.6749 ± 0.0060 against a theoretical 0.6717(1) and Lipa's calorimetric 0.6709(1) — a check with no free parameter left to tune. Three further branches were opened and closed with negative results, and they are reported as negative results.
Part II is the core: a pre-registered exclusion program for the sign of α′(T). The hypothesis that full coupled symmetric dissipative dynamics reproduces the sign is rejected by three independent routes — analytically, on calibration, and on 2D vortex simulations. Five classes of reactive mechanism are then tested against criteria written down in advance.
Part III formalizes the algebraic core of Parts I and II in Lean 4/Mathlib: 55 theorems, not one sorry, every theorem resting only on the standard axioms.
Four classes out, one boundary left standing.
| Theory class | Verdict | Why |
|---|---|---|
| Symmetric PSD hydrodynamics | Excluded | α′ = Γ²/(1+Γ²) ≥ 0 identically — the sign is unreachable by construction |
| Reactive Iordanskii-type extension | Partially excluded | Lifts the analytic ban, but hold-out data does not recover the sign near Tλ |
| Quasiclassical scattering (Sonin; Thouless–Ao–Niu) | Excluded on both sides | Sign is opposite at every temperature; the applicability condition fails universally |
| Kelvons and critical core | Excluded | Correct sign, but one to two orders of magnitude too small — the sum closes ≈1% of the gap |
| Critical order-parameter dynamics (model F) | Not structurally excluded | Right sign and right temperature trend by two independent methods; the quantitative link is missing |
Underneath all of it sits one algebraic fact. Whether the reactive physics is parametrized as a transverse friction coefficient, as an Iordanskii coupling, or as the imaginary part of a model-F kinetic coefficient, the negative sign is reachable if and only if Γ < 1/2. Three different physical stories, one boundary — and the boundary is a theorem, not a fit.
A negative result obtained under pre-fixed criteria carries the same evidentiary weight as a positive one.
The proof assistant found the mistakes.
The algebraic core was rewritten in Lean 4 against Mathlib and compiled — 55 theorems, zero sorry, axiom footprint checked theorem by theorem. That exercise was not ceremonial. It found two defects in the source analytics.
- A sign and exponent error in the stage-1 necessary condition. The original text required |Dt| ≳ κρs; the machine-checked statement is DtK > D² and K² > 4D², and an explicit counterexample (D = 1, Dt = 1, K = 2.1) satisfies the true condition while violating the claimed one. The conclusion survived; the argument for it did not.
- The two GENERIC degeneracy conditions govern energy conservation and entropy growth separately, not jointly as the source implied.
Formalization also draws a hard line around what cannot be checked: where a primary source never published its defining equations, the paper says so instead of reconstructing them and calling the reconstruction verified.
Why a markets company published superfluid physics.
The honest answer first: this paper is not about markets, and nothing in it is running inside the platform. Helium II is not a pricing model. What transfers is not the physics — it is the evidentiary discipline, and that discipline is exactly what quantitative finance is worst at.
A backtest is a machine for producing agreeable numbers. So is a calibration. In both fields the failure mode is identical: you run the model, you look at the output, you decide afterwards which criterion counts as success, and you publish the branch that worked. Superfluid hydrodynamics has half a century of that; finance has an industry of it. Three practices are what separates a result from a coincidence, and they are the same practices in both places.
- Criteria fixed before the run. In the paper, each theory class was given its exclusion criterion in advance, and four classes died against criteria their authors would have accepted beforehand. On the platform, the analogue is the run ledger: every analytic call records its author, a digest of its inputs, and its outcome — including the runs that failed. A calculation that crashed leaves a record instead of leaving nothing.
- An external check on the core. Lean does not care how convincing the derivation reads. Our market-side equivalent is differential testing: the tick engine is checked fill-by-fill against an independent reference implementation, and the fixed-income and vanilla-option pricers against QuantLib, in a separate interpreter so the two sides cannot share a dependency and agree by accident. That comparison has caught real defects — including a queue model that filled orders against volume that never traded.
- Negative results published as results. Three branches of Part I produced nothing and are written up as producing nothing. The platform rule is the same one pointed at data: when a source is missing or a key is absent, the answer is unavailable — never a plausible-looking number generated to fill the gap.
The Lean error was a wrong sign in a condition everybody had read and nobody had checked. Finance has precisely this bug, constantly: a downside-deviation denominator computed over losing periods only inflates or deflates a Sortino ratio by tens of percent, and the result still looks entirely reasonable. Reasonable-looking is not a check. Something has to be able to say no.
Three things that could undo this.
- The reference data has no error bars. No source in the programme tabulates uncertainties for α(T) and α′(T). The ±20% used here is a conservative assumption, not a measurement, and the sign-change temperature is robust only within 1.55–1.70 K under it. Without primary uncertainties, a physical sign change cannot be rigorously distinguished from noise inside the resolved window.
- One RG system was never published. The defining equations behind the surviving class exist only as citations, confirmed by three independent sources but not independently reproducible. Translating its renormalization charge into the observed vortex mobility is the single quantitative gap in the programme, and it is not closed here or, as far as we could check, anywhere in the open literature.
- The 2D magnitudes are provisional. Absolute values from vortex-pair simulations run systematically high against Oseen theory. They are used for signs and trends, not for magnitudes.
- The paper does not resolve the sign of transverse mutual friction — it maps what cannot produce it.
- Four of five reactive theory classes are excluded against pre-registered criteria; the fifth survives in sign and trend but not in magnitude.
- Every formulation tested collapses to one algebraic boundary, Γ < 1/2 — a theorem shared by three unrelated physical pictures.
- Machine-checking the algebra in Lean 4 found a wrong sign in the original analytic condition; the conclusion held, the stated argument did not.
- None of this is a market model. The transferable part is the method: criteria first, an independent check on the core, and negative results published as results.
Cite this work.
sorry; axiom footprint limited to propext, Classical.choice and Quot.sound.