decodeGalerkin2D
decodeGalerkin2D converts an LNALField of matching length into a GalerkinState by reindexing voxels with Fintype.equivFin and recovering each coefficient via decodeCoeff. Researchers stating the one-step LNAL-to-Galerkin commutation at milestone M3 cite it when packaging the decoded simulation hypothesis. The body is a direct term-mode construction that builds the EuclideanSpace from the decoded array entries.
claimFor $N$ a natural number and an LNALField whose length equals the cardinality of (modes $N$) times 2, decodeGalerkin2D returns the GalerkinState whose coefficients are the decoded reals obtained by applying decodeCoeff after mapping each mode-component index to the corresponding field position.
background
Module Simulation2D states the one-step simulation bridge at milestone M3 between the discrete 2D Galerkin model and spatial LNAL execution semantics. The claim is packaged as an explicit hypothesis rather than proved analytically. GalerkinState $N$ is the Euclidean space of real coefficients indexed by the product of the truncated modes set with Fin 2. The modes function returns the finite set of integer pairs with each component ranging from $-N$ to $N$. LNALField is an array of LNALVoxels, each carrying a sign bit and a magnitude value. decodeCoeff extracts the real coefficient as the product of the sign and the decoded magnitude.
proof idea
The definition is a direct term that applies WithLp.toLp 2 to a lambda expression. For each index $i$ in (modes $N$) times Fin 2 the term computes the corresponding linear index $j$ via Fintype.equivFin, casts it back using the supplied size hypothesis, and feeds the voxel to decodeCoeff. No tactics are used; the construction is purely functional.
why it matters in Recognition Science
decodeGalerkin2D supplies the decoding map required by DecodedSimulationHypothesis, which asserts that one LNAL spatial step commutes with the discrete Galerkin step after decoding. It completes the left-inverse direction (up to quantization) for the encode-decode pair used in decoded_simulation_one_step. The definition supports the M3 goal of stating the simulation hypothesis explicitly without axioms or sorries inside the ClassicalBridge.Fluids module.
scope and limits
- Does not establish that decodeGalerkin2D is an exact left inverse of encodeGalerkin2D.
- Does not extend the map to continuous or infinite-dimensional fields.
- Does not verify numerical stability under the coarse quantization of coeffMag.
- Does not prove the full one-step commutation, only supplies the decoder.
formal statement (Lean)
233noncomputable def decodeGalerkin2D {N : ℕ} (field : LNALField)
234 (hsize : field.size = Fintype.card ((modes N) × Fin 2)) : GalerkinState N :=
proof body
Definition body.
235 WithLp.toLp 2 (fun i : ((modes N) × Fin 2) =>
236 let j : Fin (Fintype.card ((modes N) × Fin 2)) := (Fintype.equivFin ((modes N) × Fin 2)) i
237 decodeCoeff (field[(Fin.cast hsize.symm j)]))
238
239/-- Hypothesis: one LNAL spatial step simulates one discrete Galerkin step (exactly). -/