 237    decodeCoeff (field[(Fin.cast hsize.symm j)]))
 238
 239/-- Hypothesis: one LNAL spatial step simulates one discrete Galerkin step (exactly). -/
 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 :=
 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⟩

papers checked against this theorem

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