coeffMag_foldPlusOneStep
The lemma establishes that the magnitude quantizer applied to a Galerkin coefficient after one fold-plus-one update equals the 32-bit clamped value of the prior magnitude plus one. Researchers checking discrete consistency in 2D fluid simulations within the Recognition Science bridge would cite it to confirm that LNAL voxel encodings remain invariant under the increment operation. The proof expands definitions of coeffMag and foldPlusOneStep, proves positivity via an auxiliary clamp lemma, then reduces the equality through floor of absolute int
claimLet $u$ be a Galerkin state over $N$ modes. For each mode-component index $i$, the quantized magnitude of the updated coefficient satisfies $m( (foldPlusOneStep u)_i ) = clamp_{32}( m(u_i) + 1 )$, where $m(x) = floor(|x|)$ and $clamp_{32}$ saturates to the signed 32-bit integer range.
background
The module Simulation2D implements the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics at milestone M3; it packages required claims explicitly under SimulationHypothesis rather than asserting analytic correctness. GalerkinState N is the Euclidean space of real velocity coefficients indexed by the finite set of truncated modes (integer pairs from -N to N) and the two components. coeffMag x is defined as floor of the absolute value of x; coeffSign x returns -1 when x is negative and 1 otherwise. foldPlusOneStep encodes the new real value as sign times the clamped magnitude after incrementing by one. Upstream lemmas supply clampI32_pos_of_ge_one, which guarantees the clamped result stays positive when the input is at least 1, and floor_abs_intCast, which equates floor of the absolute value of an integer cast to the absolute value itself.
proof idea
The tactic proof begins by setting x to u i and establishing that coeffMag x plus one is at least 1 via floor nonnegativity and linarith. It introduces m as the clamped magnitude and z as sign times m, then invokes clampI32_pos_of_ge_one to obtain positivity of m. A core simp reduces coeffMag of the updated coefficient to floor of the absolute value of z. The final calc applies floor_abs_intCast to reach the absolute value of z, then splits on the sign of x to show that z equals plus or minus m and therefore its absolute value equals m.
why it matters in Recognition Science
The lemma is invoked inside voxelStep_foldPlusOne_encodeIndex to equate the voxel execution of the fold-plus-one program with the encoding of the updated Galerkin state. It supplies a concrete consistency fact for the simulation bridge in ClassicalBridge.Fluids, ensuring the magnitude encoding survives the discrete update step. The result sits downstream of the GalerkinState and LNALSemantics definitions and upstream of the full voxel-step encoding lemma; it closes one link in the M3 simulation hypothesis without touching the phi-ladder or forcing chain.
scope and limits
- Does not prove that the discrete simulation converges to continuous Navier-Stokes solutions.
- Does not incorporate external forcing or boundary conditions.
- Applies exclusively to the fold-plus-one increment operation.
- Restricted to the 2D truncated Galerkin basis.
- Does not address floating-point rounding or numerical stability.
Lean usage
simp [voxelStep_foldPlusOneProgram, encodeIndex, coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep]formal statement (Lean)
94lemma coeffMag_foldPlusOneStep {N : ℕ} (u : GalerkinState N) (i : (modes N) × Fin 2) :
95 coeffMag ((foldPlusOneStep u) i) = clampI32 (coeffMag (u i) + 1) := by
proof body
Tactic-mode proof.
96 classical
97 set x : ℝ := u i
98 have hx1 : (1 : Int) ≤ coeffMag x + 1 := by
99 have hx0 : (0 : Int) ≤ coeffMag x := (Int.floor_nonneg (a := |x|)).2 (abs_nonneg x)
100 linarith
101 -- Let `m` be the (positive) clamped magnitude and `z` the signed integer we encode as a real.
102 set m : Int := clampI32 (coeffMag x + 1)
103 set z : Int := coeffSign x * m
104 have hmpos : 0 < m := by
105 simpa [m] using (clampI32_pos_of_ge_one (x := coeffMag x + 1) hx1)
106 have hm0 : 0 ≤ m := le_of_lt hmpos
107 -- Expand `coeffMag` and reduce to a floor/abs fact on an integer cast.
108 -- `foldPlusOneStep u i` is literally `(z : ℝ)`.
109 have hcore :
110 coeffMag ((foldPlusOneStep u) i) = Int.floor (|((z : ℝ))|) := by
111 simp [coeffMag, foldPlusOneStep, x, m, z, -clampI32]
112 -- Now compute the floor of the abs cast and simplify `|z|`.
113 calc
114 coeffMag ((foldPlusOneStep u) i)
115 = Int.floor (|((z : ℝ))|) := hcore
116 _ = |z| := floor_abs_intCast z
117 _ = m := by
118 by_cases hx : x < 0
119 · have hz : z = -m := by simp [z, coeffSign, hx]
120 rw [hz]
121 -- `| -m | = |m| = m` since `m ≥ 0`.
122 simp [abs_of_nonneg hm0]
123 · have hz : z = m := by simp [z, coeffSign, hx]
124 rw [hz]
125 simp [abs_of_nonneg hm0]
126