203lemma voxelStep_foldPlusOne_encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) : 204 voxelStep foldPlusOneProgram (encodeIndex u i) = encodeIndex (foldPlusOneStep u) i := by
proof body
Term-mode proof.
205 classical 206 -- use the closed-form voxel semantics for `FOLD 1`, then rewrite encoding fields 207 simp [voxelStep_foldPlusOneProgram, encodeIndex, coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep, 208 decide_lt_zero_foldPlusOneStep, -clampI32] 209 210/-! 211## Decoding the encoding (for weaker, decode-based simulation) 212 213Exact commutation at the *encoding* level is too strict for decay steps that can hit `0` and flip 214sign bits (`sigma/phiE`) when re-encoded. A practical workaround is to compare **decoded** 215coefficients after stepping. 216-/ 217 218/-- Decode a nonnegative magnitude from a register `nuPhi`. 219 220We interpret negative values as `0` (via `Int.toNat`) so that a decrement step can “saturate at 0” 221even if the underlying register becomes negative. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.