coeffSign_foldPlusOneStep
plain-language theorem explainer
The lemma shows that the sign encoding of each coefficient in a Galerkin state is preserved after one fold-plus-one update step. Workers on the discrete-to-LNAL bridge in 2D fluid simulation would cite it to maintain consistent sign information across simulation steps. The tactic proof splits on the sign of the input coefficient and applies magnitude clamping together with casting lemmas to verify the updated value keeps the original sign.
Claim. Let $u$ be a Galerkin state with $N$ modes. For each mode-component index $i$, the sign encoding of the updated coefficient equals the original: $s( (F u)_i ) = s( u_i )$, where $s$ denotes the sign encoding and $F$ the fold-plus-one update.
background
Module Simulation2D implements the one-step simulation bridge at milestone M3 between the discrete 2D Galerkin model and LNAL voxel semantics, packaging required claims explicitly as SimulationHypothesis without axioms. GalerkinState N is the Euclidean space of velocity coefficients indexed by the product of modes N and Fin 2. The set modes N consists of all integer pairs from -N to N in each coordinate. coeffSign x returns -1 when x is negative and 1 otherwise; coeffMag x returns the floor of the absolute value. The proof also invokes cast_lt_zero_iff, which equates negativity after casting from Int to real, and clampI32_pos_of_ge_one, which guarantees a positive result once the input integer is at least 1.
proof idea
The tactic proof begins with classical, sets x to the coefficient u i, and derives that the clamped magnitude plus one is positive via clampI32_pos_of_ge_one. It then performs by_cases on whether x is negative. In the negative branch it rewrites coeffSign, computes the product with the clamped magnitude, casts to real via cast_lt_zero_iff, and shows the updated coefficient remains negative. In the nonnegative branch it shows the product is nonnegative and concludes the updated coefficient is nonnegative. Both branches finish with simp using the definitions of coeffSign and foldPlusOneStep.
why it matters
The result is invoked inside the simp call of voxelStep_foldPlusOne_encodeIndex, which itself forms part of the one-step simulation encoding. It therefore contributes directly to the SimulationHypothesis that packages the discrete-to-LNAL bridge at milestone M3. Within the Recognition framework the lemma supplies an elementary invariance needed for the classical fluids layer; it does not engage the forcing chain T0-T8, the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.