foldPlusOneStep
plain-language theorem explainer
This definition supplies the discrete one-step update for Galerkin states by incrementing each coefficient's quantized magnitude by one while keeping its sign. Researchers building the 2D fluid simulation bridge cite it as the concrete step map inside the SimulationHypothesis. It is realized by a direct functional composition of the magnitude and sign extractors with clamping.
Claim. For a Galerkin state $u$ indexed by the finite set of truncated modes and two velocity components, the updated state satisfies $u'_i = s_i · clamp(⌊|u_i|⌋ + 1)$ where $s_i$ is the sign of $u_i$ and clamp maps to the 32-bit integer range.
background
GalerkinState is the Euclidean space of real velocity coefficients indexed by the product of the finite mode set (modes N, the integer grid from -N to N in each direction) and the two components. The helper coeffMag extracts the floor of the absolute value while coeffSign returns -1 or +1 according to the sign of the input real. The Simulation2D module at milestone M3 packages the discrete Galerkin dynamics as an explicit hypothesis for later commutation with LNAL voxel execution semantics.
proof idea
Direct definition that maps each coefficient independently: extract its magnitude via coeffMag, add one, clamp the result, multiply by the original sign via coeffSign, and cast back to real.
why it matters
This definition supplies the concrete step function required by the SimulationHypothesis structure, which asserts exact commutation between LNAL program execution and the discrete Galerkin update. It is used to establish the supporting lemmas coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep, decide_lt_zero_foldPlusOneStep and the voxelStep commutation lemma. In the framework it realizes the classical fluid simulation bridge at the M3 milestone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.