decodeCoeff_voxelStep_foldMinusOne_encodeIndex
plain-language theorem explainer
The lemma shows that decoding a coefficient after one fold-minus-one LNAL voxel step recovers the matching discrete step on the Galerkin coefficient. Researchers verifying one-step commutation in the discrete-to-LNAL fluid bridge would cite it when building simulation hypotheses. The proof is a classical simplification that equates both sides to the same signed-integer expression via the shared decode and encode definitions.
Claim. Let $u$ be a Galerkin state over $N$ modes. For each mode-component pair $i$, the real coefficient recovered by decoding the LNAL voxel after one execution of the fold-minus-one program on the encoded index equals the value of the fold-minus-one decoded step applied to $u$ at $i$.
background
GalerkinState is the Euclidean space of velocity coefficients indexed by the finite set of truncated modes (modes N) and two components. encodeIndex packs a single coefficient into an LNAL voxel via its magnitude (coeffMag) and sign. voxelStep executes one LNAL program step on a voxel, returning the updated (Reg6, Aux5) pair. decodeCoeff recovers the real value from the voxel sign and nuPhi register, while decodeMag maps the register to a nonnegative integer by saturating negatives at zero (Int.toNat).
proof idea
The proof opens with classical and applies a single simp that unfolds decodeCoeff, foldMinusOneDecodedStep, decodeMag, voxelStep_foldMinusOneProgram, and encodeIndex (suppressing clampI32) to equate both sides.
why it matters
This supplies the pointwise equality required to construct the DecodedSimulationHypothesis structure, whose commutation field asserts that one LNAL spatial step simulates one discrete Galerkin step after decoding. It completes the fold-minus-one case inside the M3 milestone of Simulation2D, which packages the required claim explicitly without axioms. The result advances the ClassicalBridge goal of linking the discrete Galerkin model to independent LNAL semantics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.