pith. machine review for the scientific record. sign in
structure definition def or abbrev

DecodedSimulationHypothesis

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)

 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)

proof body

Definition body.

 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`). -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (27)

Lean names referenced from this declaration's body.