SpatialSemantics
plain-language theorem explainer
SpatialSemantics supplies a structure with a single step operation that evolves an LNALField under a given LProgram. Fluids-bridge authors cite it when they need a minimal spatial update rule without committing to neighbor coupling or the full multi-voxel VM. The declaration is a bare structure definition whose only content is the type signature of step.
Claim. A structure consisting of a function $step : LProgram → LNALField → LNALField$, where $LNALField ≔ Array(LNALVoxel)$.
background
The module supplies a bridge-local spatial interface for LNAL so that fluids models can evolve an array of voxels without importing experimental multi-voxel infrastructure. LNALField is the abbreviation Array LNALVoxel. The upstream CellularAutomata.step applies a local rule globally to produce a successor tape; the UniversalForcingSelfReference.for structure records the structural properties required of a meta-realization.
proof idea
Structure definition; no lemmas or tactics are applied.
why it matters
RSNSBridgeSpec, run, and independent all depend on SpatialSemantics. It supplies the one-step spatial update required by the fluids bridge, allowing discrete approximations to be stated before any concrete neighbor rule is chosen. The module doc notes that this separation keeps the bridge free to evolve independently of the LNAL multi-voxel VM.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.