SimulationHypothesis
plain-language theorem explainer
The SimulationHypothesis structure packages the exact one-step commutation between an LNAL program and a discrete Galerkin map on 2D velocity fields. Workers on the classical bridge milestone cite it to state the simulation assumption without axioms. The structure is introduced directly; its two concrete instances are built by supplying a program and step map then discharging the commutation via simplification or reduction to a voxel-level lemma.
Claim. A SimulationHypothesis for natural number $N$ is a triple $(P, s, c)$ where $P$ is an LNAL program, $s$ maps GalerkinState$_N$ to itself, and $c$ asserts that for every state $u$, the independent step of $P$ on encodeGalerkin2D$(u)$ equals encodeGalerkin2D$(s(u))$. Here GalerkinState$_N$ denotes the Euclidean space of coefficients indexed by the finite mode set (modes $N$) times two components.
background
GalerkinState $N$ is the Euclidean space of real coefficients over the product of the truncated mode set (modes $N$) with Fin 2; modes $N$ is the finite set of integer pairs from $-N$ to $N$ in each coordinate. encodeGalerkin2D converts such a state into an LNALField by deterministic indexing via Fintype.equivFin and per-voxel encodeIndex. The module states the one-step simulation bridge between the discrete 2D Galerkin model and the spatial LNAL execution semantics, packaging the required claim as an explicit structure with no axiom or sorry.
proof idea
The structure itself is introduced by field declaration. The trivial instance supplies listenNoopProgram, the identity map, and discharges comm by a single simp. The foldPlusOne instance supplies foldPlusOneProgram and foldPlusOneStep, then uses Array.ext to reduce pointwise equality, followed by a call to the upstream voxelStep_foldPlusOne_encodeIndex lemma after index conversion.
why it matters
It supplies the hypothesis object consumed by the downstream simulation_one_step theorem, which extracts the commutation directly as H.comm u. The declaration fills the explicit packaging step required by the M3 milestone in the fluids module of the classical bridge; the module doc-comment notes that analytic correctness is left for later work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.