decide_lt_zero_foldPlusOneStep
plain-language theorem explainer
The lemma shows that each Galerkin coefficient keeps its sign under the one-step update map. Workers on the discrete fluid bridge in Recognition Science cite it to confirm that LNAL encoding preserves negativity data across steps. The proof splits on the sign of the input coefficient, invokes the magnitude and sign quantizers, then applies the clamp positivity and cast lemmas to equate the two decide predicates.
Claim. Let $u$ be a vector of real coefficients indexed by the truncated modes and the two velocity components. For every index $i$, the Boolean decision that the updated coefficient at $i$ is negative equals the decision that the original coefficient at $i$ is negative.
background
GalerkinState N is the Euclidean space of real velocity coefficients over the finite set of truncated modes (modes N) crossed with the two components. The one-step update (foldPlusOneStep) encodes each coefficient via its magnitude (floor of absolute value) and sign (minus one if negative, otherwise one), then reconstructs a new real value after clamping. The module Simulation2D supplies the explicit bridge between the discrete Galerkin model and the LNAL voxel semantics without claiming analytic correctness of the fluid equations.
proof idea
The tactic proof sets x to the coefficient at i, establishes that coeffMag x plus one is at least one, then obtains positivity of the clamped integer via clampI32_pos_of_ge_one. It performs case analysis on whether x is negative. In the negative case it rewrites coeffSign to minus one, shows the product is negative, casts to reals via cast_lt_zero_iff, and concludes the updated value is negative. The non-negative case shows the product is non-negative and therefore the updated value is non-negative. Both branches finish with simp.
why it matters
The result is invoked inside voxelStep_foldPlusOne_encodeIndex to equate the voxel execution of the fold-plus-one program on an encoded index with the encoding of the updated Galerkin state. It therefore supplies one of the concrete sign-preservation facts needed to discharge the SimulationHypothesis stated in the module. The surrounding ClassicalBridge work packages the required claim as an explicit hypothesis rather than an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.