run
plain-language theorem explainer
The run definition iterates the step operation of a SpatialSemantics n times on an LNALField under a fixed LProgram. Fluid dynamics and cosmology researchers cite it to obtain the state after any number of spatial updates in the LNAL bridge. The definition is supplied directly by pattern matching on the step count, with the zero case returning the input field and the successor case applying one step before recursing.
Claim. Let SpatialSemantics be a structure whose sole field is a step function $step : LProgram → LNALField → LNALField$, where LNALField is an array of LNAL voxels. The iterator run(sem, P) is the map $LNALField → ℕ → LNALField$ given by run(sem, P)(s, 0) := s and run(sem, P)(s, n+1) := run(sem, P)(sem.step(P, s), n).
background
The module supplies a minimal spatial interface for LNAL programs inside the fluids bridge. LNALField is the type alias Array LNALVoxel, representing a whole field of voxels. SpatialSemantics is the structure that packages a single step function taking an LProgram and returning the updated field; the run definition lives inside its namespace.
proof idea
The definition is given by direct pattern matching on the second argument. The base case (zero steps) returns the input field unchanged. The successor case applies sem.step once to the current field and recurses on the predecessor count.
why it matters
This iterator supplies the multi-step execution primitive required by downstream results including r_prediction in Cosmology.PrimordialSpectrum and kernel_perturbation_ge_one in ILG.Kernel. It closes the gap between the single-voxel LNAL VM and field-level dynamics, supporting the eight-tick octave and spatial updates needed for fluid and cosmological models in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.