pith. sign in
module module high

IndisputableMonolith.ClassicalBridge.Fluids.Simulation2D

show as:
view Lean formalization →

The module supplies a nontrivial LNAL program that increments nuPhi by +1 at every instruction pointer. Researchers composing the 2D fluid pipeline cite it as the explicit one-step simulation layer (M3). The module consists entirely of supporting definitions for folding, voxel encoding, and coefficient extraction with no theorem proofs.

claimThe central object is the LNAL program $P$ satisfying $P(ip) = +1$ increment on the nuPhi component for every instruction pointer $ip$.

background

The module operates in the setting of Milestone M3, bridging the finite Fourier truncation of 2D incompressible Navier-Stokes on the torus (Galerkin2D, M1) with the spatial LNAL semantics and voxel encoding (LNALSemantics, M2). Galerkin2D supplies a Finset of modes together with the basic algebraic energy identity for the inviscid case. LNALSemantics defines the LNALField as Array (Reg6 × Aux5) and the encoding map from Galerkin states into voxels without neighbor coupling.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module realizes the one-step simulation (M3) required by the top-level composition theorem in Regularity2D (M6), which assembles M1 through M5 into an abstract existence statement for a continuum solution.

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)