foldMinusOneDecodedStep
plain-language theorem explainer
foldMinusOneDecodedStep supplies the discrete update map on decoded Galerkin velocity coefficients that corresponds to a single FOLD (-1) operation on quantized magnitudes. Researchers verifying the LNAL-to-Galerkin commutation at milestone M3 would cite it when checking one-step equivalence after decoding. The definition is realized by extracting sign and magnitude, applying the clamped decrement, and reassembling via decodeMag inside the Euclidean space.
Claim. Let $u$ belong to the Galerkin state space for $N$ modes. For each mode-component index $i$, the updated coefficient is the product of the sign of $u_i$ and the decoded magnitude of the clamped value of (floor of absolute value of $u_i$ minus one). The resulting map sends the original state to the new state in the same Euclidean space.
background
GalerkinState is the Euclidean space of real coefficients indexed by the finite set of 2D Fourier modes (from -N to N in each coordinate) crossed with the two velocity components. coeffMag returns the floor of the absolute value of a real coefficient while coeffSign returns -1 or +1 according to its sign; decodeMag converts a possibly negative integer register back to a nonnegative integer by taking toNat and then ofNat. The module documentation states that Simulation2D packages the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics as an explicit hypothesis without axioms or sorries.
proof idea
The definition is a direct construction that applies WithLp.toLp 2 to the pointwise update function. For each index the body extracts the real coefficient, computes its magnitude and sign, adds -1 inside clampI32, decodes the result, multiplies by the preserved sign, and casts back to real.
why it matters
The definition is invoked inside the lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex that establishes decoding after an LNAL voxel step recovers the discrete update. It is also a field of the DecodedSimulationHypothesis structure that encodes the claim that one LNAL spatial step simulates one discrete Galerkin step after decoding. The construction supports the M3 milestone of stating the classical bridge without introducing axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.