coeffMag_foldPlusOneStep
plain-language theorem explainer
The lemma shows that incrementing a Galerkin coefficient via foldPlusOneStep and then extracting its magnitude yields exactly the clamped value of the original magnitude plus one. Workers on the LNAL semantics bridge in two-dimensional fluid models cite this result to confirm that the discrete update step preserves the intended magnitude shift. The argument proceeds by introducing the signed integer representation of the updated coefficient, invoking the positivity property of the clamp function, and reducing the absolute-value floor expression
Claim. Let $u$ be an element of the Galerkin state space for $N$ modes. For any index $i$ consisting of a mode pair and a component, the magnitude of the coefficient after one fold-plus-one update satisfies $coeffMag((foldPlusOneStep u)(i)) = clampI32(coeffMag(u(i)) + 1)$.
background
In the Simulation2D module the one-step simulation bridge connects the discrete Galerkin model to LNAL execution semantics. The GalerkinState N is the Euclidean space of real coefficients indexed by the finite set of modes (pairs of integers from -N to N) and the two velocity components. The function coeffMag quantizes a real value x to the integer floor of its absolute value, while coeffSign returns -1 or +1 according to the sign of x. The foldPlusOneStep operation encodes the updated coefficient as a real number whose magnitude has been incremented by one and clamped to the 32-bit integer range.
proof idea
The proof begins by setting x to the original coefficient and establishing that coeffMag x plus one is at least 1. It then defines m as the clamped magnitude and z as the signed integer coeffSign x times m. After confirming m is positive via clampI32_pos_of_ge_one, the argument shows that coeffMag of the updated coefficient equals the floor of the absolute value of z. The calculation then applies floor_abs_intCast to obtain the absolute value of z and finishes by case analysis on the sign of x, using the definition of coeffSign to conclude that the absolute value equals m.
why it matters
This lemma supports the voxelStep_foldPlusOne_encodeIndex result, which verifies that the LNAL voxel step on the encoded index reproduces the updated Galerkin state after folding. It forms part of the explicit SimulationHypothesis package in the ClassicalBridge.Fluids module at milestone M3, where analytic correctness is not yet claimed. Within the Recognition framework the construction contributes to the discrete dynamics layer that precedes any continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.