pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.LNALSemantics

show as:
view Lean formalization →

The LNALSemantics module supplies the bridge-local spatial semantics for LNAL, defining one-voxel execution on (Reg6 × Aux5) voxels and related functions such as voxelStep and independent. Researchers assembling the 2D fluids pipeline cite it when linking the Galerkin model to discrete LNAL steps. The module consists entirely of definitions with no theorems or proofs.

claimThe module defines LNAL spatial semantics on arrays of $(Reg_6 × Aux_5)$ voxels, with the one-voxel step operation and the independent execution map.

background

Galerkin2D introduces a finite-dimensional Fourier-mode truncated model for 2D incompressible Navier-Stokes on the torus, with the goal of obtaining a concrete discrete state space and the basic algebraic energy identity for the inviscid case. LNAL supplies the single-voxel VM; the present module extends it to a spatial interface whose state is an array of (Reg6 × Aux5) voxels. The module therefore sits between the Galerkin truncation and the one-step simulation layer.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the LNAL encoding and semantics (M2) required by Simulation2D (Milestone M3) for the one-step simulation bridge and by Regularity2D (Milestone M6) for the top-level composition theorem that concludes an abstract continuum solution exists. It therefore closes the discrete-state portion of the 2D pipeline.

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)