The Cosmic No-Go

Under any contact-Hamiltonian flow with constant rotation, the transverse contraction rate is rigidly locked to the derivative of the cosmic expansion rate. Push the transverse rate toward a genuine attractor (μ → −2) and the expansion rate is forced unbounded below — a structural obstruction, not a gap waiting to be closed. The coupling that makes this model a faithful relaxation system is exactly what makes it a poor expansion model. The kinematic correspondence to de Sitter cosmology (ż = H, e^−z ∝ a⁻¹) is genuine but strictly kinematic: it has no matter or radiation era, and the correction it carries corresponds to an equation of state matching neither.

Where this sits in a wider effort

This chapter's formalization work is one small corner of a much larger, live effort to bring hard analysis into Lean 4. Worth knowing about independent of anything here: Scott Armstrong and Julia Kempe's 2026 formalization of De Giorgi–Nash–Moser elliptic regularity theory — the first proof-assistant Sobolev-space library built from weak derivatives at this scale, sorry-free and axiom-free beyond Lean and Mathlib itself. See arXiv:2604.05984 and github.com/scottnarmstrong/DeGiorgi. Where our differential-equations line and theirs overlap — weak derivatives, Sobolev witnesses, well-posedness on a domain — is a real seam worth watching, not a claim of collaboration.

In this chapter's corpus

• Formal Verification of the Heat Equation (monograph, Lax–Milgram → discretization → conditioning)
• A Contact-Geometric Toy Model on the Solid Cylinder (helix paper — source of this chapter's no-go theorem)
• HeatEquation_Step1.lean — axiom-tagged Lean scaffold
• HelixToyModel.lean — Lean scaffold with real proofs + tagged sorries