decodeCoeff_voxelStep_foldMinusOne_encodeIndex
plain-language theorem explainer
The lemma shows that decoding a Galerkin coefficient after one LNAL voxel execution under the fold-minus-one program recovers exactly the action of the corresponding discrete decoded step at that mode-component index. Researchers verifying the one-step LNAL-to-Galerkin commutation in the ClassicalBridge fluids milestone would cite it when assembling the DecodedSimulationHypothesis. The proof is a direct simplification that reduces both sides to the same signed-integer expression.
Claim. Let $u$ be a Galerkin state on $N$ modes. For each mode-component index $i$, the real coefficient recovered by decoding after one voxel execution of the fold-minus-one program on the encoded voxel of $u$ at $i$ 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 (Icc(-N,N) in each direction) and the two vector components. encodeIndex packs one such coefficient into an LNALVoxel by storing its magnitude via coeffMag and its mode indices. voxelStep runs a single LProgram step on an isolated voxel, returning the updated (Reg6, Aux5) pair. decodeCoeff extracts a real value by combining the sign register with decodeMag applied to the nuPhi register; decodeMag maps any integer to its nonnegative part, saturating negatives at zero.
proof idea
The tactic proof opens with classical, then applies simp to unfold decodeCoeff, foldMinusOneDecodedStep, decodeMag, voxelStep_foldMinusOneProgram and encodeIndex (while suppressing clampI32). Both sides collapse to the identical signed-integer expression, establishing the equality without further case analysis.
why it matters
The lemma supplies the pointwise commutation required to populate the comm field of DecodedSimulationHypothesis, the structure that packages the claim that one LNAL spatial step simulates one discrete Galerkin step after decoding. It completes the one-step bridge stated in the Simulation2D module at milestone M3, where the simulation hypothesis is asserted explicitly without axioms or sorry. The result sits inside the ClassicalBridge domain and does not invoke the Recognition Science forcing chain or RCL.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.