decide_lt_zero_foldPlusOneStep
The lemma establishes that the sign decision for each Galerkin coefficient is invariant under the fold-plus-one update. Researchers verifying discrete dynamics in the 2D fluid simulation bridge cite it to confirm that LNAL encoding preserves negativity. The proof proceeds by case analysis on the input sign, after establishing positivity of the clamped magnitude via auxiliary lemmas.
claimLet $u$ be a Galerkin state over $N$ modes. For any mode-component pair $i$, the sign decision after the one-step fold update equals the original: decide$((foldPlusOneStep u)_i < 0)$ = decide$(u_i < 0)$.
background
In the Simulation2D module (Milestone M3), the one-step simulation bridge connects the discrete 2D Galerkin model to LNAL execution semantics without axioms or sorries. GalerkinState is the Euclidean space of real velocity coefficients indexed by the finite set of truncated modes (Icc from -N to N in each direction) and two components. The fold-plus-one update encodes each coefficient via coeffMag (floor of absolute value) and coeffSign (-1 if negative, else +1), followed by clamping to an i32 range.
proof idea
The tactic proof sets x := u i, proves 1 ≤ coeffMag x + 1, then obtains 0 < clampI32 (coeffMag x + 1) from clampI32_pos_of_ge_one. Case analysis on x < 0 follows. When negative, coeffSign yields -1 so the updated integer is negative; casting via cast_lt_zero_iff gives the real inequality, and simpa closes the branch. When non-negative, the updated value is shown non-negative by the same lemmas and not_lt_of_ge finishes the case.
why it matters in Recognition Science
The result is used by voxelStep_foldPlusOne_encodeIndex to equate the LNAL voxel step under foldPlusOneProgram with the encoding of the updated Galerkin state. It supplies a required sign-preservation fact inside the ClassicalBridge.Fluids one-step simulation package at milestone M3. No direct link to the T0-T8 forcing chain or Recognition Composition Law appears; the lemma closes a discrete-dynamics interface in the classical fluid layer.
scope and limits
- Does not prove analytic correctness or convergence of the simulation.
- Does not extend the update rule to three spatial dimensions.
- Does not incorporate boundary conditions or external forcing.
- Does not address stability of the discrete flow under repeated steps.
Lean usage
simp [voxelStep_foldPlusOneProgram, decide_lt_zero_foldPlusOneStep]formal statement (Lean)
166lemma decide_lt_zero_foldPlusOneStep {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
167 decide ((foldPlusOneStep u) i < 0) = decide (u i < 0) := by
proof body
Tactic-mode proof.
168 classical
169 set x : ℝ := u i
170 have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
171 have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
172 linarith
173 have hmpos : 0 < clampI32 (coeffMag x + 1) :=
174 clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1
175 by_cases hx : x < 0
176 ·
177 have hzInt : (coeffSign x) * clampI32 (coeffMag x + 1) < 0 := by
178 have hneg : -(clampI32 (coeffMag x + 1)) < 0 := neg_neg_of_pos hmpos
179 calc
180 (coeffSign x) * clampI32 (coeffMag x + 1)
181 = (-1) * clampI32 (coeffMag x + 1) := by simp [coeffSign, hx]
182 _ = -(clampI32 (coeffMag x + 1)) := by ring
183 _ < 0 := hneg
184 have hzReal :
185 (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) < 0 :=
186 (cast_lt_zero_iff (z := (coeffSign x) * clampI32 (coeffMag x + 1))).2 hzInt
187 have hy : (foldPlusOneStep u) i < 0 := by
188 simpa [foldPlusOneStep, x] using hzReal
189 simp [x, hx, hy]
190 ·
191 have hzInt : (0 : Int) ≤ (coeffSign x) * clampI32 (coeffMag x + 1) := by
192 have hm0 : (0 : Int) ≤ clampI32 (coeffMag x + 1) := le_of_lt hmpos
193 simpa [coeffSign, hx] using hm0
194 have hzReal :
195 (0 : ℝ) ≤ (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) := by
196 exact_mod_cast hzInt
197 have hy : ¬ (foldPlusOneStep u) i < 0 := by
198 have hy0 : (0 : ℝ) ≤ (foldPlusOneStep u) i := by
199 simpa [foldPlusOneStep, x] using hzReal
200 exact not_lt_of_ge hy0
201 simp [x, hx, hy]
202