structure
definition
def or abbrev
SimulationHypothesis
show as:
view Lean formalization →
formal statement (Lean)
240structure SimulationHypothesis (N : ℕ) where
241 /-- The LNAL program used for the simulation. -/
242 P : LProgram
243 /-- The discrete (time-stepping) map on Galerkin states. -/
244 step : GalerkinState N → GalerkinState N
245 /-- One-step commutation: execute then encode = encode then step. -/
246 comm :
247 ∀ u : GalerkinState N,
248 (independent.step P (encodeGalerkin2D u)) = encodeGalerkin2D (step u)
249
250/-- Trivial simulation: use the `LISTEN noop` LNAL program and take the discrete step as `id`. -/
251@[simp] def SimulationHypothesis.trivial (N : ℕ) : SimulationHypothesis N :=
proof body
Definition body.
252 { P := listenNoopProgram
253 step := id
254 comm := by
255 intro u
256 simp }
257
258/-- A concrete, nontrivial simulation instance: `FOLD 1` corresponds to `foldPlusOneStep`. -/
259noncomputable def SimulationHypothesis.foldPlusOne (N : ℕ) : SimulationHypothesis N :=
260 { P := foldPlusOneProgram
261 step := foldPlusOneStep
262 comm := by
263 intro u
264 classical
265 -- Prove array equality by pointwise equality.
266 refine Array.ext (by simp [LNALSemantics.independent, encodeGalerkin2D]) ?_
267 intro j hj₁ hj₂
268 have hj : j < Fintype.card ((modes N) × Fin 2) := by
269 simpa [encodeGalerkin2D] using hj₂
270 let jFin : Fin (Fintype.card ((modes N) × Fin 2)) := ⟨j, hj⟩
271 -- Reduce to the single-voxel commutation lemma.
272 simpa [LNALSemantics.independent, encodeGalerkin2D, foldPlusOneProgram] using
273 (show voxelStep foldPlusOneProgram (encodeIndex u ((Fintype.equivFin ((modes N) × Fin 2)).symm jFin))
274 = encodeIndex (foldPlusOneStep u) ((Fintype.equivFin ((modes N) × Fin 2)).symm jFin) from by
275 simpa using
276 (voxelStep_foldPlusOne_encodeIndex (u := u)
277 (i := (Fintype.equivFin ((modes N) × Fin 2)).symm jFin))) }
278
279/-- The one-step simulation lemma (directly from `SimulationHypothesis.comm`). -/