pith. machine review for the scientific record. sign in
theorem proved term proof

simulation_one_step

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 280theorem simulation_one_step {N : ℕ} (H : SimulationHypothesis N) (u : GalerkinState N) :
 281    independent.step H.P (encodeGalerkin2D u) = encodeGalerkin2D (H.step u) :=

proof body

Term-mode proof.

 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**. -/

depends on (19)

Lean names referenced from this declaration's body.