cast_lt_zero_iff
plain-language theorem explainer
The lemma states that an integer z is negative precisely when its canonical embedding into the reals is negative. It is invoked inside the sign-preservation and decision lemmas that track coefficient signs under one-step Galerkin updates. The tactic proof splits the biconditional, derives a contradiction via non-negativity preservation on the forward direction, and applies exact_mod_cast on the reverse.
Claim. For every integer $z$, $z < 0$ if and only if the image of $z$ under the canonical embedding into the reals satisfies the same inequality.
background
The module packages the one-step simulation bridge between the discrete 2D Galerkin model (Galerkin2D) and LNAL execution semantics (LNALSemantics) at milestone M3, stating required claims explicitly as SimulationHypothesis rather than axioms. GalerkinState N holds real coefficients indexed by modes and spatial directions; foldPlusOneStep performs the discrete update whose sign behavior must be tracked. The present lemma supplies the elementary coercion fact needed to equate integer and real negativity tests inside those update lemmas.
proof idea
The tactic applies constructor to obtain the two directions. Forward: assume the real cast is negative, negate the integer non-negativity hypothesis, cast the resulting inequality, and obtain a contradiction with not_lt_of_ge. Reverse: apply exact_mod_cast directly to the integer hypothesis.
why it matters
The result is used by coeffSign_foldPlusOneStep and decide_lt_zero_foldPlusOneStep, which together guarantee that the one-step update preserves coefficient signs. These lemmas support the explicit SimulationHypothesis that encodes the discrete field execution without claiming analytic correctness. The lemma therefore closes a basic coercion gap inside the ClassicalBridge.Fluids layer at M3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.