voxelStep_foldPlusOne_encodeIndex

formal source

 200      exact not_lt_of_ge hy0
 201    simp [x, hx, hy]
 202
 203lemma voxelStep_foldPlusOne_encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
 204    voxelStep foldPlusOneProgram (encodeIndex u i) = encodeIndex (foldPlusOneStep u) i := by
 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. -/
 222def decodeMag (z : Int) : Int :=
 223  Int.ofNat (Int.toNat z)
 224
 225/-- Decode a single real coefficient from a voxel: sign from `sigma`, magnitude from `nuPhi`. -/
 226noncomputable def decodeCoeff (v : LNALVoxel) : ℝ :=
 227  ((v.1.sigma * decodeMag v.1.nuPhi : Int) : ℝ)
 228
 229/-- Decode an `LNALField` (of the expected Galerkin encoding length) back to a Galerkin state.
 230
 231This is a left-inverse of `encodeGalerkin2D` only up to the coarse quantization used by `coeffMag`.
 232-/
 233noncomputable def decodeGalerkin2D {N : ℕ} (field : LNALField)