SimulationHypothesis
The declaration defines a structure packaging an LNAL program P, a discrete step map on Galerkin states, and the exact commutation that one independent execution on the encoded field recovers the encoding of the stepped state. Researchers formalizing one-step bridges between discrete fluid models and LNAL semantics would cite it to state the simulation hypothesis without axioms. The definition supplies a trivial instance via noop program and identity map, proved by simplification, plus a fold-plus-one instance reduced via array extensionality.
claimA structure consisting of a program $P$, a map $s$ from the Galerkin state space (Euclidean space of coefficients over the truncated modes $N$ and two components) to itself, and the property that for every state $u$, the independent execution of $P$ on the encoded field equals the encoding of $s(u)$.
background
The Simulation2D module at milestone M3 states the one-step simulation bridge between the discrete 2D Galerkin model and LNAL spatial execution semantics, packaging the required claim explicitly without axioms or sorries. GalerkinState N is the EuclideanSpace of real coefficients indexed by modes N (the finite set of integer pairs from -N to N in each coordinate) times Fin 2 for the velocity components. encodeGalerkin2D converts such a state to an LNALField by deterministic indexing via Fintype.equivFin and per-voxel encodeIndex.
proof idea
The structure is introduced by definition. The trivial instance sets P to listenNoopProgram and step to id, with commutation following by simp. The foldPlusOne instance sets P to foldPlusOneProgram and step to foldPlusOneStep; commutation proceeds by Array.ext to reduce to pointwise equality, reindexes with Fintype.equivFin, and applies the voxelStep_foldPlusOne_encodeIndex lemma.
why it matters in Recognition Science
This supplies the hypothesis consumed directly by the downstream simulation_one_step theorem, which extracts the commutation as H.comm u. It realizes the M3 milestone requirement to state the exact one-step bridge between Galerkin discretization and LNAL semantics without hidden hypotheses. In the Recognition framework it provides the concrete interface connecting classical fluid models to spatial LNAL execution.
scope and limits
- Does not prove that the discrete Galerkin step approximates the continuous Navier-Stokes equations.
- Does not address multi-step iteration or convergence of the simulation.
- Does not validate physical accuracy of the LNAL program beyond commutation.
- Does not extend to three or more spatial dimensions.
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`). -/