voxelStep_foldPlusOne_encodeIndex
plain-language theorem explainer
The lemma establishes exact commutation between one LNAL voxel step under the fold-plus-one program and the discrete Galerkin update at the level of encoded coefficients. Researchers constructing discrete-to-LNAL bridges for 2D fluid models would cite it when verifying one-step equivalence in the simulation hypothesis. The proof is a direct simplification that rewrites the voxel step and encoding using the closed-form magnitude and sign lemmas.
Claim. Let $u$ be a Galerkin state over $N$ modes. For each mode-component pair $i$, the LNAL voxel step under the fold-plus-one program applied to the encoding of $u$ at $i$ equals the encoding of the coefficient after one fold-plus-one update on $u$.
background
GalerkinState N is the Euclidean space of velocity coefficients indexed by the finite set of truncated modes (modes N) and the two components. encodeIndex maps one such coefficient into an LNAL voxel register containing magnitude, sign, and mode data. voxelStep executes one LProgram step on a voxel under the independent spatial semantics.
proof idea
The proof is a one-line wrapper that applies simp to voxelStep_foldPlusOneProgram, encodeIndex, coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep, and decide_lt_zero_foldPlusOneStep.
why it matters
This lemma supplies the encoding-level commutation required by the SimulationHypothesis structure, which packages the one-step bridge claim for milestone M3 without axioms or sorries. It sits in the classical bridge layer connecting the Galerkin truncation to LNAL spatial execution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.