decodeCoeff_voxelStep_foldMinusOne_encodeIndex
Researchers verifying one-step commutation between LNAL voxel execution and discrete Galerkin decay cite this lemma. It shows that decoding a coefficient after the FOLD(-1) program runs on its encoded voxel recovers the result of the matching discrete decay step. The proof is a direct simplification that reduces both sides to identical signed-integer expressions.
claimLet $u$ be a vector of velocity coefficients over the truncated 2D Fourier modes and velocity components. For each mode-component index $i$, the real number obtained by encoding the coefficient at $i$ into an LNAL voxel, executing one step of the fold-minus-one program on that voxel, and decoding the coefficient equals the value produced by the fold-minus-one decoded step applied to $u$ at $i$.
background
GalerkinState N is the Euclidean space of velocity coefficients indexed by the finite set of truncated modes and the two velocity components. The modes function returns the finite grid of integer wavevectors from -N to N in each coordinate. encodeIndex packs one coefficient's magnitude (via coeffMag) together with its mode into a single LNAL voxel. voxelStep executes a given LNAL program on one voxel in isolation. decodeCoeff recovers the signed real coefficient from the voxel's sigma sign bit and nuPhi magnitude register. The module states the one-step simulation bridge between the discrete 2D Galerkin model and LNAL spatial semantics, packaging the required commutation as an explicit hypothesis rather than an axiom.
proof idea
The proof opens with the classical tactic and then applies a single simp that unfolds decodeCoeff, foldMinusOneDecodedStep, decodeMag, voxelStep_foldMinusOneProgram, and encodeIndex while excluding the clamp definition. Both sides thereby reduce to the same signed-integer expression.
why it matters in Recognition Science
The lemma supplies the pointwise coefficient equality used inside the proof of DecodedSimulationHypothesis for the fold-minus-one case, where it establishes commutation after decoding. It fills the concrete one-step bridge required by the ClassicalBridge.Fluids module at milestone M3. The result supports the broader Recognition Science program of realizing discrete dynamics directly from LNAL execution semantics without claiming analytic correctness of the fluid equations.
scope and limits
- Does not prove analytic correctness of the LNAL simulation for fluid equations.
- Does not address interactions between neighboring voxels.
- Does not extend to continuous time or multi-step evolution.
- Applies only to the specific fold-minus-one program and its decoded counterpart.
Lean usage
ext i; simp [decodeCoeff_voxelStep_foldMinusOne_encodeIndex]formal statement (Lean)
337lemma decodeCoeff_voxelStep_foldMinusOne_encodeIndex {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
338 decodeCoeff (voxelStep foldMinusOneProgram (encodeIndex u i)) = (foldMinusOneDecodedStep u) i := by
proof body
Tactic-mode proof.
339 classical
340 -- both sides reduce to the same signed-integer expression
341 simp [decodeCoeff, foldMinusOneDecodedStep, decodeMag, voxelStep_foldMinusOneProgram, encodeIndex, -clampI32]
342
343/-- A concrete, proved decay-step simulation instance (after decoding). -/
344noncomputable def DecodedSimulationHypothesis.foldMinusOne (N : ℕ) : DecodedSimulationHypothesis N :=
345 { P := foldMinusOneProgram
346 step := foldMinusOneDecodedStep
347 comm := by
348 intro u
349 classical
350 -- Prove equality of Galerkin states by pointwise equality of coefficients.
351 ext i
352 -- Reduce to the single-voxel lemma `decodeCoeff_voxelStep_foldMinusOne_encodeIndex`.
353 simp [decodeGalerkin2D, LNALSemantics.independent, encodeGalerkin2D,
354 decodeCoeff_voxelStep_foldMinusOne_encodeIndex] }
355
356end Simulation2D
357
358end IndisputableMonolith.ClassicalBridge.Fluids