cast_lt_zero_iff
The equivalence establishes that an integer z is negative exactly when its canonical embedding into the reals is negative. Fluid simulation code in the ClassicalBridge layer cites this fact when deciding signs of Galerkin coefficients after each foldPlusOneStep update. The tactic proof splits the biconditional with constructor, dispatches the forward direction by contradiction on nonnegativity after casting, and handles the reverse by direct exact_mod_cast.
claimFor every integer $z$, the real number obtained by casting $z$ satisfies $(z : ℝ) < 0$ if and only if $z < 0$.
background
The lemma resides in Simulation2D, the module that packages the one-step simulation bridge between the discrete 2D Galerkin model (Galerkin2D) and the LNAL execution semantics (LNALSemantics.independent) applied to an encoded field. At milestone M3 the module states required claims explicitly as SimulationHypothesis without analytic correctness proofs or axioms. The result supplies the sign decision primitive used by the downstream lemmas coeffSign_foldPlusOneStep and decide_lt_zero_foldPlusOneStep that track coefficient signs across updates to a GalerkinState.
proof idea
The proof opens with constructor to split the biconditional. The left-to-right direction assumes the cast is negative, derives a contradiction from the assumption that z is nonnegative by applying le_of_not_gt followed by exact_mod_cast to obtain a real nonnegativity statement, and closes with not_lt_of_ge. The right-to-left direction applies exact_mod_cast directly to the hypothesis.
why it matters in Recognition Science
The lemma supplies the sign-preservation fact required by coeffSign_foldPlusOneStep and decide_lt_zero_foldPlusOneStep, which maintain coefficient signs under the foldPlusOneStep update inside the one-step simulation. It therefore supports the M3 milestone claim that discrete LNAL semantics can be applied to the encoded Galerkin field while preserving sign information. The result closes a small but necessary gap between integer-based LNAL decisions and real-valued Galerkin coefficients without introducing new hypotheses.
scope and limits
- Does not address sign or ordering for non-integer real numbers.
- Does not extend to other type coercions or embeddings beyond Int to Real.
- Does not supply magnitude or absolute-value information.
- Does not interact with the phi-ladder or J-cost definitions used elsewhere in Recognition Science.
formal statement (Lean)
64lemma cast_lt_zero_iff {z : Int} : ((z : ℝ) < 0) ↔ z < 0 := by
proof body
Tactic-mode proof.
65 constructor
66 · intro hz
67 by_contra h
68 have : (0 : Int) ≤ z := le_of_not_gt h
69 have : (0 : ℝ) ≤ (z : ℝ) := by exact_mod_cast this
70 exact (not_lt_of_ge this) hz
71 · intro hz
72 exact_mod_cast hz
73