💡 Open Challenges — The Thermodynamic Censorship Conjecture

[xaviercallens]

Open Research Challenges

The epistemic audit poses several open formal and computational challenges. This thread collects community ideas and proposed approaches.

---

Formal Lean 4 Challenges

1. Thermodynamic Censorship Theorem: Prove (or disprove) that under the UniformBoundedEnstrophy axiom, the Gevrey-2 collapsing-vortex construction is impossible. Template in 03_Lean4_Topological_Censorship/src/ThermodynamicCensorship.lean.

2. BKM Challenge Rework: The current bkm_regularity_censorship formalization is trivially provable. Can you write a non-trivial Lean 4 proposition that correctly captures the physical constraint?

3. Dual-Scale Regularization: Formalize the k_eff = min(|k|, 1/(α'|k|)) cutoff as a Lean 4 type constraint on the Euler frequency tower.

---

Computational Challenges

4. 3D Mach Trajectory Simulation: Extend directive5_mach_divergence.py to full 3D compressible NSE and verify the 67-femtosecond threshold.

5. Stochastic Reynolds-Stress Decoupling: Monte Carlo simulation at thermal equilibrium — at what noise amplitude does the Reynolds-stress cancellation fail for each X_R?

---

Theoretical Questions

6. Does the Thermodynamic Censorship Principle follow from known regularity theory? Connection to Caffarelli-Kohn-Nirenberg partial regularity?

7. What is the correct physical reformulation of the Clay Prize? Should it require bounded enstrophy, compressibility, or molecular discreteness?

Post your ideas, partial results, or literature pointers as replies.