Exact quotient comparisons preserved by jamming

Jamming a nonzero discarded suffix into the low bit relates the retained prefix to the original Euclidean quotient and remainder. The comparison lemmas show that the exact fraction and its jammed prefix make the same comparisons at the even boundaries used by posit rounding, including scaled tails and stream midpoints.

These lemmas concern the exact quotient and retained prefix, independently of storage width. Direct.PrefixProof uses them after normalizing significands to prove the executable prefix correct; Direct.Proof then connects that prefix to the posit encoding and final rounding.

Quotient fractions and jamming

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_bounds (quotient remainder denominator : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) : ↑quotient ≤ ↑quotient + ↑remainder / ↑denominator ∧ ↑quotient + ↑remainder / ↑denominator < ↑quotient + 1

A Euclidean quotient plus its proper remainder lies in its unit interval.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotient_lt_quotientFraction (quotient remainder denominator : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder ≠ 0) : ↑quotient < ↑quotient + ↑remainder / ↑denominator

A nonzero Euclidean remainder places the exact quotient strictly above its prefix.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_lt_natCast_iff (quotient remainder denominator boundary : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) : ↑quotient + ↑remainder / ↑denominator < ↑boundary ↔ quotient < boundary

A Euclidean quotient plus its proper remainder lies below a natural boundary exactly when the quotient does.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.natCast_lt_quotientFraction_iff (quotient remainder denominator boundary : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) : ↑boundary < ↑quotient + ↑remainder / ↑denominator ↔ boundary < quotient ∨ boundary = quotient ∧ remainder ≠ 0

A natural boundary lies below a Euclidean quotient plus its proper remainder exactly when it lies below the quotient, or equals the quotient and the remainder is nonzero.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_lt_even_iff_jam_lt (quotient remainder denominator boundary : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hboundary : boundary % 2 = 0) : ↑quotient + ↑remainder / ↑denominator < ↑boundary ↔ StickyPrefix.jamRemainder quotient remainder < boundary

Jamming and the exact quotient fraction lie on the same lower side of every even integer boundary. A stream threshold with at least one zero padding bit has this form.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.even_lt_quotientFraction_iff_lt_jam (quotient remainder denominator boundary : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hboundary : boundary % 2 = 0) : ↑boundary < ↑quotient + ↑remainder / ↑denominator ↔ boundary < StickyPrefix.jamRemainder quotient remainder

Jamming and the exact quotient fraction lie on the same upper side of every even integer boundary.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.exactTailRaw_jamRemainder (exponentField quotient remainder leading : ℕ) (hleading : 0 < leading) (hlower : 2 ^ leading ≤ quotient) : GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading = StickyPrefix.jamRemainder (GuardStickyRounding.exactTailRaw exponentField quotient leading) remainder

Jamming a normalized significand is the same operation as jamming its complete exponent/fraction tail. The leading bit position is positive for every Posit payload, so the exponent contribution and removed hidden bit are both even.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.streamMidpointRaw_mod_two (raw width retained : ℕ) (hpadding : retained + 1 < width) : GuardStickyRounding.streamMidpointRaw raw width retained % 2 = 0

A zero-padded midpoint is even whenever at least one padding bit remains.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.paddedStreamPrefix_jamRemainder_le (quotient remainder width retained : ℕ) (hretained : retained < width) : GuardStickyRounding.streamPrefix (StickyPrefix.jamRemainder quotient remainder) width retained * 2 ^ (width - retained) ≤ quotient

Padding a retained jammed prefix back to the complete stream width never exceeds the unjammed integer prefix.

The only nontrivial case is a nonzero remainder after an even quotient. Jamming then adds one, but the padded retained prefix is even, so it cannot equal that odd successor.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_lt_paddedStreamPrefix_jamRemainder_succ (quotient remainder denominator width retained : ℕ) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hretained : retained < width) : ↑quotient + ↑remainder / ↑denominator < ↑((GuardStickyRounding.streamPrefix (StickyPrefix.jamRemainder quotient remainder) width retained + 1) * 2 ^ (width - retained))

The exact quotient fraction lies strictly below the successor of its retained jammed prefix.

This is the upper half of the general local bracket. It needs only a proper Euclidean remainder and discards at least one stream bit; no Posit width, storage tier, or candidate decoder appears.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientTailFraction_lt_midpoint_iff_jammed (exponentField quotient remainder denominator leading retained : ℕ) (hleading : 0 < leading) (hlower : 2 ^ leading ≤ quotient) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hpadding : retained + 1 < leading + 2) : ↑(GuardStickyRounding.exactTailRaw exponentField quotient leading) + ↑remainder / ↑denominator < ↑(GuardStickyRounding.streamMidpointRaw (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained) ↔ GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading < GuardStickyRounding.streamMidpointRaw (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained

An exact quotient fraction and its jammed finite tail lie on the same lower side of every zero-padded stream midpoint.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.midpoint_lt_quotientTailFraction_iff_jammed (exponentField quotient remainder denominator leading retained : ℕ) (hleading : 0 < leading) (hlower : 2 ^ leading ≤ quotient) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hpadding : retained + 1 < leading + 2) : ↑(GuardStickyRounding.streamMidpointRaw (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained) < ↑(GuardStickyRounding.exactTailRaw exponentField quotient leading) + ↑remainder / ↑denominator ↔ GuardStickyRounding.streamMidpointRaw (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained < GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading

An exact quotient fraction and its jammed finite tail lie on the same upper side of every zero-padded stream midpoint.

Interpreting finite stream words

The unjammed quotient is an integer tail word followed by one proper rational remainder. The closing lemmas quotientFraction_lt_trailingRat_iff and trailingRat_lt_quotientFraction_iff compare that fractional position with any bounded integer tail boundary. They use only monotonicity of trailingRat, so quotient rounding does not duplicate Posit regime layout or decoder proofs.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.trailingRat_exactTailRaw_succ (exponentField significand leading : ℕ) (hexponent : exponentField < 4) (hlower : 2 ^ leading ≤ significand) (hupper : significand < 2 ^ (leading + 1)) (hsuccessor : GuardStickyRounding.exactTailRaw exponentField significand leading + 1 < 2 ^ (leading + 2)) : trailingRat (leading + 2) (GuardStickyRounding.exactTailRaw exponentField significand leading + 1) = (↑significand + 1) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField

Advancing one finite tail word advances a normalized significand by one unit in its stored leading position, including a carry into the next exponent within the bounded tail.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_lt_trailingRat_iff (exponentField quotient remainder denominator leading boundary : ℕ) (hexponent : exponentField < 4) (hlower : 2 ^ leading ≤ quotient) (hupper : quotient < 2 ^ (leading + 1)) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hboundary : boundary < 2 ^ (leading + 2)) : (↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField < trailingRat (leading + 2) boundary ↔ ↑(GuardStickyRounding.exactTailRaw exponentField quotient leading) + ↑remainder / ↑denominator < ↑boundary

A quotient plus proper remainder is below a bounded finite-stream word exactly when its normalized rational value is below the value denoted by that word.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.trailingRat_lt_quotientFraction_iff (exponentField quotient remainder denominator leading boundary : ℕ) (hexponent : exponentField < 4) (hlower : 2 ^ leading ≤ quotient) (hupper : quotient < 2 ^ (leading + 1)) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hboundary : boundary < 2 ^ (leading + 2)) : trailingRat (leading + 2) boundary < (↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField ↔ ↑boundary < ↑(GuardStickyRounding.exactTailRaw exponentField quotient leading) + ↑remainder / ↑denominator

The reverse bounded finite-stream comparison has the corresponding fractional meaning.