cast_lt_zero_iff
plain-language theorem explainer
The lemma equates negativity of an integer with negativity of its real cast. It is invoked inside sign-tracking steps of the 2D Galerkin fluid simulation. The proof splits the biconditional, derives a contradiction from the forward direction via non-negativity and casting, and applies exact_mod_cast on the reverse.
Claim. For every integer $z$, $(z : ℝ) < 0$ if and only if $z < 0$.
background
Module Simulation2D packages the one-step bridge between the discrete 2D Galerkin model and LNAL execution semantics; analytic correctness is deferred to an explicit SimulationHypothesis. The lemma supplies a casting fact required when deciding coefficient signs after each foldPlusOneStep. No upstream lemmas are referenced.
proof idea
Constructor splits the biconditional. Forward direction assumes the cast is negative, obtains a contradiction by applying le_of_not_gt to produce a non-negative integer, casts that inequality to reals, and invokes not_lt_of_ge. Reverse direction applies exact_mod_cast directly.
why it matters
The result is used by coeffSign_foldPlusOneStep and decide_lt_zero_foldPlusOneStep, which establish that foldPlusOneStep preserves both the sign of each coefficient and the decide predicate on negativity. These steps belong to the one-step simulation bridge inside the ClassicalBridge domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.