clampI32_pos_of_ge_one
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove analytic correctness of the 2D fluid simulation.
- Applies only when the input integer satisfies x ≥ 1.
- Does not address real-valued or floating-point saturation.
- Limited to the specific i32 bounds 2147483648 and -2147483648.
Lean usage
have hpos : 0 < clampI32 x := clampI32_pos_of_ge_one hxformal statement (Lean)
74lemma clampI32_pos_of_ge_one {x : Int} (hx : 1 ≤ x) : 0 < clampI32 x := by
proof body
Tactic-mode proof.
75 -- From `x ≥ 1`, the negative-saturation branch is impossible; then either we saturate high,
76 -- or we return `x` itself. In both cases the result is positive.
77 have hx0 : (0 : Int) ≤ x := le_trans (by decide : (0 : Int) ≤ 1) hx
78 have hnot : ¬ x ≤ (-i32Bound) := by
79 have hi : (-i32Bound : Int) < 0 := by
80 have : (0 : Int) < i32Bound := by decide
81 linarith
82 exact not_le_of_gt (lt_of_lt_of_le hi hx0)
83 -- Convert `hnot` to the numeral form used by definitional unfolding of `i32Bound`.
84 have hnot' : ¬ x ≤ (-2147483648 : Int) := by simpa using hnot
85 dsimp [clampI32]
86 rw [if_neg hnot']
87 by_cases h₂ : (2147483648 : Int) ≤ x
88 · rw [if_pos h₂]
89 have : (1 : Int) < (2147483648 : Int) := by decide
90 linarith
91 · rw [if_neg h₂]
92 exact lt_of_lt_of_le (by decide : (0 : Int) < 1) hx
93