Shared finite-prefix proof helpers

These lemmas describe sticky-bit jamming independently of the operation that generated the prefix. Quotient and square-root kernels share this proof layer.

theorem FloatLib.Floats.Formats.Posit.Model.StickyPrefix.lor_one_eq (value : ℕ) : value ||| 1 = if value % 2 = 0 then value + 1 else value

Setting the low bit either preserves an odd value or increments an even value.

theorem FloatLib.Floats.Formats.Posit.Model.StickyPrefix.jamRemainder_eq (value remainder : ℕ) : jamRemainder value remainder = if remainder = 0 then value else if value % 2 = 0 then value + 1 else value

Jamming preserves an exact prefix and otherwise sets precisely its low bit.

theorem FloatLib.Floats.Formats.Posit.Model.StickyPrefix.jamRemainder_congr (value first second : ℕ) (hzero : first = 0 ↔ second = 0) : jamRemainder value first = jamRemainder value second

Jamming depends only on whether the remainder is zero.