floor_abs_intCast
plain-language theorem explainer
This lemma establishes that the floor of the absolute value of an integer cast to the reals equals the integer's absolute value. It is used inside the coefficient magnitude update for the one-step 2D fluid simulation bridge. The proof is a short tactic sequence that reduces the claim via absolute-value casting identities to the standard floor-of-integer-cast result.
Claim. For any integer $z$, $⌊|(z : ℝ)|⌋ = |z|$.
background
The Simulation2D module states the one-step simulation bridge between the discrete 2D Galerkin model and LNAL execution semantics. At Milestone M3 the analytic correctness of the simulation is packaged as an explicit SimulationHypothesis rather than proved. This lemma supplies the elementary identity relating floor to absolute value after integer-to-real casting, which is required for magnitude handling inside the discrete step.
proof idea
The proof first uses simp to obtain |((z : ℝ))| = ((|z| : Int) : ℝ). It then rewrites the goal and finishes with simpa applied to Int.floor_intCast.
why it matters
The lemma is invoked by coeffMag_foldPlusOneStep, which computes the updated magnitude after one fold step in the simulation. It therefore supports the classical bridge packaged in Simulation2D at Milestone M3. The result ensures that integer floor arithmetic aligns with the discrete Galerkin model without introducing sorries or axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.