SimulationHypothesis
plain-language theorem explainer
SimulationHypothesis packages the exact one-step commutation between LNAL program execution on an encoded Galerkin field and the discrete map on the Galerkin state. Researchers citing the M3 milestone of the ClassicalBridge fluids bridge would invoke this structure to state simulation assumptions without axioms. The definition supplies two concrete instances whose commutation properties are discharged by simplification and reduction to a voxel-level lemma.
Claim. A simulation hypothesis for truncation level $N$ consists of an LNAL program $P$, a discrete map step from the space of Galerkin states (velocity coefficients over the finite mode set) to itself, and the commutation property asserting that the independent execution step of $P$ on the encoded state equals the encoding of the image under step.
background
GalerkinState N is the Euclidean space of real coefficients indexed by the finite set of modes (product of intervals from -N to N) times two velocity components. The map encodeGalerkin2D converts such a state into an LNALField array by deterministic indexing via Fintype.equivFin. The module states the one-step simulation bridge at milestone M3 between the discrete Galerkin model and the independent spatial LNAL execution semantics, packaging the required claim explicitly as a structure with no axiom or sorry.
proof idea
The structure itself is introduced by direct field declaration. Its trivial instance sets the program to listenNoopProgram and the step to the identity map, discharging commutation by a single simp tactic. The foldPlusOne instance sets the program to foldPlusOneProgram and the step to foldPlusOneStep; commutation is obtained by Array.ext, reduction to pointwise equality, and appeal to the upstream voxelStep_foldPlusOne_encodeIndex lemma.
why it matters
The structure is the direct input to the downstream theorem simulation_one_step, which extracts the commutation property as a standalone lemma. It supplies the explicit hypothesis required by the M3 milestone statement in the module documentation. The construction closes the one-step bridge between Galerkin2D and LNALSemantics without invoking Recognition Science constants or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.