SpatialSemantics
plain-language theorem explainer
SpatialSemantics is a structure supplying a one-step evolution map from an LNAL program and voxel field to a successor field. Bridge authors connecting Recognition Science to discrete fluid models cite it to fix the spatial update contract. The declaration is a bare structure with a single field and no proof obligations.
Claim. A structure equipped with a field $step : LProgram → LNALField → LNALField$, where $LNALField := Array LNALVoxel$.
background
The module supplies a minimal spatial interface for LNAL in the fluids bridge. LNALField is the abbreviation Array LNALVoxel, so the state is an array of per-voxel states. This interface is kept separate from the core single-voxel VM and from any experimental multi-voxel code.
proof idea
The declaration is a plain structure definition. It introduces the SpatialSemantics type by directly specifying its single field step of type LProgram → LNALField → LNALField.
why it matters
SpatialSemantics supplies the execution contract used by the run iterator and by the independent semantics. It is referenced inside RSNSBridgeSpec to link the discrete LNAL model to classical fluid requirements. The structure therefore closes the spatial-execution gap between the LNAL VM and the Recognition Science fluids bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.