simulation_one_step

formal source

 277                (i := (Fintype.equivFin ((modes N) × Fin 2)).symm jFin))) }
 278
 279/-- The one-step simulation lemma (directly from `SimulationHypothesis.comm`). -/
 280theorem simulation_one_step {N : ℕ} (H : SimulationHypothesis N) (u : GalerkinState N) :
 281    independent.step H.P (encodeGalerkin2D u) = encodeGalerkin2D (H.step u) :=
 282  H.comm u
 283
 284/-!
 285## Decode-based simulation (weaker notion) and a diagonal decay step
 286
 287For some local operations (e.g. sign-preserving decay of a magnitude register), exact commutation
 288`encode(step u) = step(encode u)` can fail due to sign-bit conventions at `0`.
 289
 290We therefore also provide a **decode-based** simulation notion:
 291we compare decoded coefficients after executing the LNAL step.
 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)