decide_lt_zero_foldPlusOneStep
plain-language theorem explainer
The lemma shows that the sign decision for any Galerkin coefficient is invariant under the fold-plus-one update. Workers on discrete fluid bridges cite it to confirm that LNAL encoding preserves negativity when stepping the state. The proof splits on the sign of the coefficient, invokes the positive clamp lemma and the integer-to-real negativity equivalence, then simplifies both branches to equate the decides.
Claim. For any natural number $N$, Galerkin state $u$ and mode-component index $i$, the predicate that the updated coefficient after one fold-plus-one step is negative equals the predicate that the original coefficient is negative: decide$((foldPlusOneStep u)_i < 0)$ = decide$(u_i < 0)$.
background
Module Simulation2D packages the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics at milestone M3, without claiming analytic correctness. GalerkinState N is the Euclidean space of velocity coefficients indexed by truncated modes and two components. The set modes N consists of integer pairs from -N to N in each coordinate. coeffMag x returns the floor of |x| and coeffSign x returns -1 when x is negative and 1 otherwise. Upstream lemmas cast_lt_zero_iff equate integer and real negativity while clampI32_pos_of_ge_one guarantees positivity of the clamped magnitude plus one.
proof idea
The tactic proof opens with classical, sets x := u i, proves the clamped magnitude plus one is at least 1, then applies clampI32_pos_of_ge_one to obtain positivity. It splits by cases on x < 0. The negative branch uses coeffSign = -1 to show the integer product is negative, casts it to a negative real via cast_lt_zero_iff, concludes the updated coefficient is negative, and simplifies. The non-negative branch shows the integer product is non-negative, deduces the updated coefficient is non-negative, and simplifies the decides.
why it matters
The result is invoked inside voxelStep_foldPlusOne_encodeIndex to equate the LNAL voxel step on an encoded index with the encoded image of the updated Galerkin state. It therefore closes one link in the M3 simulation bridge that packages the SimulationHypothesis without axioms. Within the Recognition framework it maintains sign consistency for the classical fluid layer before any analytic Navier-Stokes correspondence is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.