floor_abs_intCast
plain-language theorem explainer
The lemma states that for any integer z the floor of its absolute value after casting to the reals equals the integer absolute value. Workers on the 2D Galerkin-to-LNAL simulation bridge cite it when computing coefficient magnitudes during one-step updates. The proof is a short tactic sequence that rewrites the absolute-value cast and invokes the standard floor-of-integer-cast fact.
Claim. For any integer $z$, $⌊|(z:ℝ)|⌋ = |z|$.
background
The Simulation2D module bridges the discrete 2D Galerkin model (Galerkin2D) with LNAL execution semantics (LNALSemantics.independent) at milestone M3. It packages the required simulation claim as an explicit SimulationHypothesis without axioms or sorries. The lemma supplies an elementary identity used when coefficient magnitudes are extracted from real-valued field entries.
proof idea
Tactic proof: simp establishes that the absolute value of the cast real equals the cast of the integer absolute value; rw replaces the left-hand side; simpa then applies Int.floor_intCast.
why it matters
The lemma is invoked inside coeffMag_foldPlusOneStep, which itself forms part of the one-step simulation bridge packaged as SimulationHypothesis. It supplies the integer-arithmetic identity needed to keep magnitude tracking exact inside the ClassicalBridge.Fluids domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.