clampI32_pos_of_ge_one
plain-language theorem explainer
clampI32_pos_of_ge_one shows that clamping any integer x at least 1 to the signed 32-bit range produces a strictly positive integer. Workers on the 2D Galerkin fluid simulation cite it to maintain positivity of coefficient magnitudes after each fold-plus-one update. The proof first derives non-negativity of x, rules out the lower saturation branch by transitivity and sign of the bound, then splits on upper saturation and concludes positivity by direct comparison in each case.
Claim. Let $x$ be an integer with $x$ at least 1. Then the saturation of $x$ to the interval $[-2^{31},2^{31}-1]$ is strictly positive.
background
The module states the one-step simulation bridge between the discrete 2D Galerkin model and spatial LNAL execution semantics applied to an encoded field. At milestone M3 the analytic correctness of the simulation is packaged as an explicit SimulationHypothesis rather than an axiom. clampI32 saturates its integer argument to the signed 32-bit range with lower bound -2147483648 and upper bound 2147483648. The lemma relies on the transitivity property le_trans imported from ArithmeticFromLogic to obtain 0 ≤ x from 0 ≤ 1 and the given lower bound.
proof idea
The proof first obtains 0 ≤ x by le_trans applied to the decidable fact 0 ≤ 1. It then shows x cannot satisfy x ≤ -i32Bound by deriving that the bound is negative and applying lt_of_lt_of_le, followed by a simpa to numeral form. After dsimp on clampI32 and rewriting the lower-branch negation, it cases on whether x meets the upper bound 2147483648. The positive branch uses linarith with the decidable fact 1 < 2147483648; the negative branch uses lt_of_lt_of_le with 0 < 1 and the hypothesis x ≥ 1.
why it matters
The lemma feeds directly into coeffMag_foldPlusOneStep, coeffSign_foldPlusOneStep and decide_lt_zero_foldPlusOneStep inside the same module. These three results together close the positivity and sign invariants required by the fold-plus-one program that implements the one-step bridge. It therefore supplies a concrete, proved fragment of the SimulationHypothesis at the M3 milestone without invoking any analytic fluid equations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.