decoded_simulation_one_step

formal source

 306          = step u
 307
 308/-- The one-step decoded simulation lemma (directly from `DecodedSimulationHypothesis.comm`). -/
 309theorem decoded_simulation_one_step {N : ℕ} (H : DecodedSimulationHypothesis N) (u : GalerkinState N) :
 310    decodeGalerkin2D (N := N)
 311      (field := independent.step H.P (encodeGalerkin2D u))
 312      (hsize := by simp [LNALSemantics.independent, encodeGalerkin2D])
 313      = H.step u :=
 314  H.comm u
 315
 316/-- A constant LNAL program: decrement `nuPhi` by `1` (via `FOLD (-1)`). -/
 317@[simp] def foldMinusOneProgram : LProgram :=
 318  fun _ => LInstr.fold (-1)
 319
 320/-- One-voxel semantics for `foldMinusOneProgram`: decrement `nuPhi` by `1` (clamped); leave `aux5` unchanged. -/
 321lemma voxelStep_foldMinusOneProgram (v : LNALVoxel) :
 322    voxelStep foldMinusOneProgram v = ({ v.1 with nuPhi := clampI32 (v.1.nuPhi + (-1)) }, v.2) := by
 323  rcases v with ⟨r6, a5⟩
 324  simp [LNALSemantics.voxelStep, foldMinusOneProgram, lStep, -clampI32]
 325
 326/-- The corresponding discrete step on **decoded** Galerkin coefficients.
 327
 328We mimic the VM update on `nuPhi` (via `clampI32`) and then decode a nonnegative magnitude using `decodeMag`. -/
 329noncomputable def foldMinusOneDecodedStep {N : ℕ} (u : GalerkinState N) : GalerkinState N :=
 330  WithLp.toLp 2 (fun i : ((modes N) × Fin 2) =>
 331    let x : ℝ := u i
 332    let m : Int := decodeMag (clampI32 (coeffMag x + (-1)))
 333    let z : Int := (coeffSign x) * m
 334    (z : ℝ))
 335
 336/-- Decoding after a single `FOLD (-1)` step matches the corresponding decoded discrete step. -/
 337lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
 338    decodeCoeff (voxelStep foldMinusOneProgram (encodeIndex u i)) = (foldMinusOneDecodedStep u) i := by
 339  classical