 292-/
 293
 294/-- Hypothesis: one LNAL spatial step simulates one discrete Galerkin step **after decoding**. -/
 295structure DecodedSimulationHypothesis (N : ℕ) where
 296  /-- The LNAL program used for the simulation. -/
 297  P : LProgram
 298  /-- The discrete (time-stepping) map on Galerkin states (on decoded/quantized coefficients). -/
 299  step : GalerkinState N → GalerkinState N
 300  /-- One-step commutation after decoding. -/
 301  comm :
 302      ∀ u : GalerkinState N,
 303        decodeGalerkin2D (N := N)
 304          (field := independent.step P (encodeGalerkin2D u))
 305          (hsize := by simp [LNALSemantics.independent, encodeGalerkin2D])
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.