floor_abs_intCast
plain-language theorem explainer
The lemma asserts that the floor of the absolute value of an integer cast to the reals equals the integer absolute value. It is invoked inside magnitude-update steps for discrete 2D Galerkin states. The tactic proof reduces the cast absolute value by simplification then applies the standard floor-of-integer-cast identity.
Claim. For every integer $z$, $⌊|z|_ℝ⌋ = |z|$.
background
The lemma sits inside Simulation2D, the module that packages the one-step bridge between the discrete 2D Galerkin model (Galerkin2D) and LNAL execution semantics (LNALSemantics). At milestone M3 the module states an explicit SimulationHypothesis rather than proving analytic correctness of the simulation. The lemma supplies a pure-arithmetic identity required when coefficient magnitudes are updated under the foldPlusOneStep operation.
proof idea
A local hypothesis equates the absolute value of the cast real to the cast of the integer absolute value (simp). The rewrite substitutes this equality, after which simpa invokes Int.floor_intCast on the absolute-value integer.
why it matters
The result is used by coeffMag_foldPlusOneStep to justify the non-negativity step inside the magnitude clamp for the updated GalerkinState. It therefore contributes to the SimulationHypothesis that encodes the one-step classical bridge. No direct link to the T0-T8 forcing chain or Recognition constants appears; the lemma closes a numerical gap inside the fluid-simulation scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.