pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D

show as:
view Lean formalization →

The Simulation2D module supplies the one-step simulation for a nontrivial LNAL program that increments nuPhi by +1 at every instruction pointer. It forms the M3 link in the 2D fluid pipeline connecting discrete state updates to the Galerkin encoding. Researchers in discrete Navier-Stokes modeling cite it for the explicit voxel-step definitions. The module consists of program definitions together with supporting lemmas for folding and coefficient handling.

claimThe central object is the LNAL program $P$ that increments the variable $nu_φ$ by $+1$ at every instruction pointer, together with the associated step map $S$ that applies $P$ to the LNALField encoding of the 2D Galerkin Fourier state.

background

The module operates in the setting of the 2D incompressible Navier-Stokes equations discretized via Fourier modes on the torus. Galerkin2D introduces this finite-dimensional model: 'This file introduces a finite-dimensional (Fourier-mode truncated) model for 2D incompressible Navier–Stokes on the torus.' LNALSemantics supplies the minimal spatial semantics and encoding: 'This file provides a minimal spatial semantics for running an LNAL program over an LNALField (an Array (Reg6 × Aux5)), and an explicit encoding of the 2D Galerkin Fourier state (Galerkin2D) into LNAL voxels.' The present module adds the concrete simulation step that executes the increment program over those voxels.

proof idea

This is a definition module, no proofs. It introduces foldPlusOneProgram as the increment program and defines the voxel step via voxelStep_foldPlusOneProgram together with auxiliary functions such as foldPlusOneStep, coeffMag_foldPlusOneStep, decodeMag, and decodeCoeff. Helper lemmas including floor_abs_intCast, cast_lt_zero_iff, and clampI32_pos_of_ge_one support the integer arithmetic of the step.

why it matters in Recognition Science

This module supplies the one-step simulation (M3) required by the top-level composition theorem in Regularity2D. The downstream doc-comment states: 'This file provides the top-level composition theorem for the 2D pipeline: Galerkin2D (M1) + LNAL encoding/semantics (M2) + one-step simulation (M3) + CPM instantiation (M4) + continuum limit packaging (M5) ⇒ an abstract “continuum solution exists” conclusion.' It therefore closes the discrete dynamics segment of the classical bridge.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (21)