pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics

show as:
view Lean formalization →

This module defines the LNAL spatial semantics for the 2D fluids bridge, centering on one-voxel execution of a single LNAL step applied to (Reg6 × Aux5) states together with supporting encoding and independence functions. Researchers assembling the discrete Navier-Stokes pipeline cite it as the M2 interface layer imported by Simulation2D and Regularity2D. The module consists entirely of definitions with no theorems or proofs.

claimvoxelStep : (Reg_6 × Aux_5) → (Reg_6 × Aux_5) implements one LNAL step on a voxel; independent : array of voxels → array of voxels applies the step uniformly across the spatial field.

background

The module sits inside the ClassicalBridge.Fluids layer and imports the single-voxel LNAL VM together with the finite-dimensional Galerkin2D model of 2D incompressible Navier-Stokes on the torus. LNAL supplies the core (Reg6 × Aux5) voxel type; Galerkin2D supplies the truncated Fourier-mode state space. The supplied LNAL doc states that the file defines a minimal bridge-local interface whose spatial state is an array of (Reg6 × Aux5) voxels.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the LNAL semantics required by Simulation2D (M3), which packages the one-step simulation hypothesis, and by Regularity2D (M6), which states the top-level composition theorem for the full 2D pipeline: Galerkin2D (M1) + LNAL encoding/semantics (M2) + one-step simulation (M3) + CPM instantiation (M4) + continuum limit packaging (M5).

scope and limits

used by (2)

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 (9)