Fixed points are exactly the inviscid
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
Invariance holds exactly when ν = 0: the fixed points of T are the inviscid equations.
Proposition
(∀ v ∈ [(-2 : Int), -1, 1, 2], T ⟨1,1,1,v⟩ ≠ ⟨1,1,1,v⟩) ∧ T ⟨1,1,1,0⟩ = ⟨1,1,1,0⟩Proof
By by in navier-stokes.lean. The kernel reduces the proposition and reports no axiom dependency.
Sources and identifiers
- Lean source · src/pair/formal/proofs/navier-stokes.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
- Deposit record ·
navier-stokes--fixed_points_are_exactly_the_inviscid