pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D

show as:
view Lean formalization →

Simulation2D supplies the concrete one-step LNAL simulation for the 2D Galerkin fluid model by defining a program that increments nuPhi by +1 at every instruction pointer. It sits between the M1 state encoding and M2 semantics on one side and the M6 composition on the other. Researchers tracing the discrete-to-continuum fluid pipeline in Recognition Science cite this module for the explicit voxel-step definitions. The module is purely definitional, introducing named programs and step functions without theorems.

claimThe module defines an LNAL program $P$ on an LNALField such that each instruction pointer advances the field by incrementing the nuPhi component by $+1$, together with the associated voxel-step and fold functions that realize one simulation tick.

background

The module operates inside the ClassicalBridge.Fluids hierarchy. Galerkin2D (M1) supplies the finite-dimensional Fourier-mode truncation of 2D incompressible Navier-Stokes on the torus together with the basic algebraic energy identity for the inviscid case. LNALSemantics (M2) gives the spatial semantics that run an LNAL program over an Array (Reg6 × Aux5) and the explicit encoding that maps a Galerkin2D state into LNAL voxels; the present module is intentionally minimal and omits neighbor graphs and inter-voxel coupling.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

Simulation2D provides the one-step simulation (M3) required by the top-level composition theorem in Regularity2D (M6). That theorem assembles Galerkin2D (M1) + LNAL encoding/semantics (M2) + one-step simulation (M3) + CPM instantiation (M4) + continuum-limit packaging (M5) into an abstract existence statement for continuum solutions.

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)