coeffSign_foldPlusOneStep
The lemma establishes invariance of the coefficient sign encoding under the one-step fold-plus-one update for Galerkin states. Researchers bridging discrete 2D fluid modes to LNAL voxel semantics cite it to confirm that sign parity survives magnitude increments in the simulation step. The proof proceeds by case analysis on the sign of the input coefficient, using positivity of the clamped incremented magnitude together with integer-to-real casting lemmas to show the updated value retains the original sign.
claimLet $u$ be a Galerkin state over $N$ modes. For any mode-component index $i$, the sign encoding of the coefficient at $i$ after the one-step update equals the sign encoding of the original coefficient at $i$.
background
In the Simulation2D module at milestone M3, the one-step simulation bridge connects the discrete 2D Galerkin model to LNAL execution semantics without claiming analytic correctness of the fluid dynamics. GalerkinState is the Euclidean space of real velocity coefficients indexed by the finite set of truncated modes. The coefficient sign function returns -1 on negative inputs and 1 otherwise, while coeffMag returns the floor of the absolute value as an integer. The fold-plus-one-step function performs the discrete update by incrementing the quantized magnitude and re-encoding the sign. This lemma depends on the GalerkinState and modes definitions from Galerkin2D, the sign and magnitude functions from LNALSemantics, and local lemmas for clamping and casting between integers and reals.
proof idea
The tactic proof sets the local coefficient to the input value at index i. It first proves the clamped magnitude after increment is positive via clampI32_pos_of_ge_one. Case analysis on whether the input is negative follows. When negative, the product of sign and clamped magnitude is shown negative, then cast to reals to conclude the updated coefficient is negative. When nonnegative, the product is shown nonnegative and cast to conclude the updated coefficient is nonnegative. Both branches finish by simplification with the sign definition.
why it matters in Recognition Science
This lemma is invoked inside voxelStep_foldPlusOne_encodeIndex to equate the LNAL voxel step under the fold-plus-one program with the encoding of the updated Galerkin state. It supplies the sign-invariance piece required for the discrete dynamics in the ClassicalBridge.Fluids module at milestone M3. Within the Recognition framework it supports the simulation bridge between Galerkin truncation and LNAL semantics while leaving analytic correctness and continuous limits as separate hypotheses.
scope and limits
- Does not prove convergence of the discrete simulation to continuous Navier-Stokes equations.
- Does not extend to three spatial dimensions or to mode truncations beyond the given N.
- Does not establish invariance under iterated steps or under other update programs.
- Does not address numerical stability, floating-point rounding, or quantization error bounds.
Lean usage
simp [voxelStep_foldPlusOneProgram, encodeIndex, coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep, decide_lt_zero_foldPlusOneStep]formal statement (Lean)
127lemma coeffSign_foldPlusOneStep {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
128 coeffSign ((foldPlusOneStep u) i) = coeffSign (u i) := by
proof body
Tactic-mode proof.
129 classical
130 set x : ℝ := u i
131 have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
132 have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
133 linarith
134 have hmpos : 0 < clampI32 (coeffMag x + 1) :=
135 clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1
136 by_cases hx : x < 0
137 ·
138 -- `x < 0` ⇒ `coeffSign x = -1`, and the step coefficient is negative (since the magnitude is positive).
139 have hzInt : (coeffSign x) * clampI32 (coeffMag x + 1) < 0 := by
140 have hneg : -(clampI32 (coeffMag x + 1)) < 0 := neg_neg_of_pos hmpos
141 calc
142 (coeffSign x) * clampI32 (coeffMag x + 1)
143 = (-1) * clampI32 (coeffMag x + 1) := by simp [coeffSign, hx]
144 _ = -(clampI32 (coeffMag x + 1)) := by ring
145 _ < 0 := hneg
146 have hzReal :
147 (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) < 0 :=
148 (cast_lt_zero_iff (z := (coeffSign x) * clampI32 (coeffMag x + 1))).2 hzInt
149 have hy : (foldPlusOneStep u) i < 0 := by
150 simpa [foldPlusOneStep, x] using hzReal
151 simp [coeffSign, hx, hy, x]
152 ·
153 -- `¬ x < 0` ⇒ `coeffSign x = 1`, and the step coefficient is nonnegative.
154 have hzInt : (0 : Int) ≤ (coeffSign x) * clampI32 (coeffMag x + 1) := by
155 have hm0 : (0 : Int) ≤ clampI32 (coeffMag x + 1) := le_of_lt hmpos
156 simpa [coeffSign, hx] using hm0
157 have hzReal :
158 (0 : ℝ) ≤ (((coeffSign x) * clampI32 (coeffMag x + 1) : Int) : ℝ) := by
159 exact_mod_cast hzInt
160 have hy : ¬ (foldPlusOneStep u) i < 0 := by
161 have hy0 : (0 : ℝ) ≤ (foldPlusOneStep u) i := by
162 simpa [foldPlusOneStep, x] using hzReal
163 exact not_lt_of_ge hy0
164 simp [coeffSign, hx, hy, x]
165