floor_abs_intCast
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish analytic correctness of the full simulation.
- Applies only to integer inputs.
- Does not involve Recognition Science forcing chain or constants.
Lean usage
have h : Int.floor (|((z : ℝ))|) = |z| := floor_abs_intCast zformal statement (Lean)
58lemma floor_abs_intCast (z : Int) : Int.floor (|((z : ℝ))|) = |z| := by
proof body
Tactic-mode proof.
59 have habs : |((z : ℝ))| = ((|z| : Int) : ℝ) := by
60 simp
61 rw [habs]
62 simpa using (Int.floor_intCast (R := ℝ) (z := |z|))
63