run
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not define or constrain the concrete step function beyond the interface signature.
- Does not establish any invariants, convergence, or boundedness properties of the iteration.
- Does not handle program errors or invalid voxel states.
- Does not relate the iteration count to physical time or the eight-tick octave.
formal statement (Lean)
33def run (sem : SpatialSemantics) (P : IndisputableMonolith.LNAL.LProgram) : LNALField → Nat → LNALField
34 | s, 0 => s
35 | s, Nat.succ n => run sem P (sem.step P s) n
36
37end SpatialSemantics
38
39end Fluids
40end ClassicalBridge
41end IndisputableMonolith