4 ms·

Is everything in NavierStokesAndEuler/NavierStokes [1] precedent to the derivations? How to tree shake Lean4? (Edit: `lake shake`,) [1] https://github.com/ope

• westurner 16d ago
  (I am again posting this comment, which was certainly censored in error: https://news.ycombinator.com/item?id=49605915#49633297 https://news.ycombinator.com/item?id=49605915#49633297 ) What about compressible fluids? Existing Navier-Stokes models for compressible fluids: "On the implosion of a compressible fluid II: Singularity formation" (2022) https://projecteuclid.org/journals/annals-of-mathematics/vol https://projecteuclid.org/journals/annals-of-mathematics/vol... "Blow-up of the 3-D compressible Navier-Stokes equations for monatomic gases" (2025) https://arxiv.org/html/2501.15701v2 https://arxiv.org/html/2501.15701v2 ... From https://news.ycombinator.com/item?id=49389524#49404787 https://news.ycombinator.com/item?id=49389524#49404787: > "I/Q Sampling for Signal Phase" (2026-08) https://share.gemini.google/rDVcVwDnWPTc https://share.gemini.google/rDVcVwDnWPTc : >> It's a Twistor-Grassmanian mapping? From "Navier-Stokes Breakthrough, FTLE, and SQG" (2026-09) https://share.gemini.google/sq2XmhphMFWE https://share.gemini.google/sq2XmhphMFWE : > The Mathematical Formulation: Because SQS is explicitly a superfluid Bose–Einstein condensate, treating it purely as a classical Navier–Stokes fluid misses quantized vorticity. The full formulation maps to the Gross–Pitaevskii (Euler–Korteweg) equations via the Madelung transformation ... > To adapt the Córdoba–Martínez-Zoroa (CMZ) / Buckmaster / OpenAI Lean cascade to Euler–Korteweg, three core structural adjustments must be made: > - Irrotationality Constraint > - Third-Order Dispersion > - Hydrodynamic Energy Functional