independent
plain-language theorem explainer
The independent definition supplies the minimal spatial semantics for LNAL programs acting on a field of voxels. Researchers constructing the classical bridge to fluid models cite it when they need an uncoupled discrete evolution operator. The definition is realized by a direct record construction that applies the single-voxel step uniformly via Array.map.
Claim. The independent spatial semantics is the structure whose step operator sends an LNAL program $P$ and field $F$ to the field obtained by applying the single-voxel evolution map to every element of $F$ independently.
background
The LNALSemantics module supplies a minimal spatial interface for executing LNAL programs over an LNALField (an Array of (Reg6 × Aux5) voxels) as part of Milestone M2. SpatialSemantics is the structure that requires a single step function of type LProgram → LNALField → LNALField. voxelStep realizes one LNAL instruction on an isolated voxel by initializing an LState from the voxel's Reg6 and Aux5 components and then calling lStep. The module doc states that the construction is intentionally minimal and omits any neighbor graph or inter-voxel coupling.
proof idea
The definition is a direct record construction. The step field of SpatialSemantics is populated by the lambda that maps the already-defined voxelStep P across the input field.
why it matters
This supplies the base uncoupled spatial executor required by the classical bridge. It is invoked by the lemma independent_step_listenNoopProgram to show that listenNoopProgram acts as the identity. Downstream it supports RSNSBridgeSpec in the Fluids.Bridge module and DecodedSimulationHypothesis in Simulation2D. The definition therefore closes the minimal spatial-semantics slot in the LNAL-to-Navier-Stokes pathway before coupling or Galerkin encoding is added.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.