Normalization and correctness of direct quotient prefixes

The direct quotient kernel normalizes significands, emits a bounded quotient window, and records any nonzero discarded suffix with a sticky bit. This module follows those stages: common-leading normalization, retained-prefix bounds, recovery of the input dyadic ratio, and the final prefixAtLeading correctness theorems.

Direct.Jamming proves the exact-fraction comparison lemmas shared by these stages. Posit layout and final rounding refinement remain in Direct.Proof; the results here are uniform in width.

Common-leading normalization

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.shiftToCommon_bounds (value common : ℕ) (hvalue : value ≠ 0) (hleading : value.log2 ≤ common) : 2 ^ common ≤ value <<< (common - value.log2) ∧ value <<< (common - value.log2) < 2 ^ (common + 1)

Shifting a nonzero integer from its leading bit to a larger common position normalizes it.

structure FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.NormalizedSignificands.Spec (normalized : NormalizedSignificands) (numerator denominator : ℕ) : Prop

Proof facts carried by a pair of significands after common-leading normalization.

The executable record deliberately stores only values needed by the quotient kernel. These facts live in Prop, so proofs can name the common bounds without enlarging runtime data.

• numeratorLeading_eq : normalized.numeratorLeading = numerator.log2

  The recorded numerator leading position is exact.

• denominatorLeading_eq : normalized.denominatorLeading = denominator.log2

  The recorded denominator leading position is exact.

• numerator_eq : normalized.numerator = numerator * 2 ^ (max numerator.log2 denominator.log2 - numerator.log2)

  The numerator is shifted to the common leading position.

• denominator_eq : normalized.denominator = denominator * 2 ^ (max numerator.log2 denominator.log2 - denominator.log2)

  The denominator is shifted to the common leading position.

• numerator_lower : 2 ^ max numerator.log2 denominator.log2 ≤ normalized.numerator

  The normalized numerator reaches the common leading bit.

• numerator_upper : normalized.numerator < 2 ^ (max numerator.log2 denominator.log2 + 1)

  The normalized numerator has no bit above the common leading bit.

• denominator_lower : 2 ^ max numerator.log2 denominator.log2 ≤ normalized.denominator

  The normalized denominator reaches the common leading bit.

• denominator_upper : normalized.denominator < 2 ^ (max numerator.log2 denominator.log2 + 1)

  The normalized denominator has no bit above the common leading bit.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.normalizeSignificands_spec (numerator denominator : ℕ) (hnumerator : numerator ≠ 0) (hdenominator : denominator ≠ 0) : (normalizeSignificands numerator denominator).Spec numerator denominator

Common-leading normalization records exact positions, values, and bounds.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.shiftedRatio_eq (numerator denominator commonLeading : ℕ) (hnumeratorLeading : numerator.log2 ≤ commonLeading) (hdenominatorLeading : denominator.log2 ≤ commonLeading) : ↑(numerator * 2 ^ (commonLeading - numerator.log2)) / ↑(denominator * 2 ^ (commonLeading - denominator.log2)) = ↑numerator / ↑denominator * 2 ^ (Int.ofNat denominator.log2 - Int.ofNat numerator.log2)

Common-leading normalization changes a ratio only by the recorded leading-position offset.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.normalizedQuotient_bounds (leading common numerator denominator : ℕ) (hnumeratorLower : 2 ^ common ≤ numerator) (hnumeratorUpper : numerator < 2 ^ (common + 1)) (hdenominatorLower : 2 ^ common ≤ denominator) (hdenominatorUpper : denominator < 2 ^ (common + 1)) : have steps := if numerator < denominator then leading + 1 else leading; 2 ^ leading ≤ numerator * 2 ^ steps / denominator ∧ numerator * 2 ^ steps / denominator < 2 ^ (leading + 1)

The quotient selected from two equally normalized integers has the requested leading position.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.jamRemainder_bounds (leading quotient remainder : ℕ) (hlower : 2 ^ leading ≤ quotient) (hupper : quotient < 2 ^ (leading + 1)) : 2 ^ leading ≤ StickyPrefix.jamRemainder quotient remainder ∧ StickyPrefix.jamRemainder quotient remainder < 2 ^ (leading + 1)

Jamming a normalized quotient preserves its leading position without overflowing it.

Bracketing the retained quotient prefix

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.trailingRat_streamPrefix_jammed_le_quotientFraction (exponentField quotient remainder denominator leading retained : ℕ) (hleading : 0 < leading) (hexponent : exponentField < 4) (hlower : 2 ^ leading ≤ quotient) (hupper : quotient < 2 ^ (leading + 1)) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hretained : retained < leading + 2) : trailingRat retained (GuardStickyRounding.streamPrefix (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained) ≤ (↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField

The retained prefix of a normalized jammed quotient is at most the exact normalized quotient.

This is the representation-independent lower-bracket theorem used by Posit candidate proofs.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_lt_trailingRat_streamPrefix_jammed_succ (exponentField quotient remainder denominator leading retained : ℕ) (hleading : 0 < leading) (hexponent : exponentField < 4) (hlower : 2 ^ leading ≤ quotient) (hupper : quotient < 2 ^ (leading + 1)) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) (hretained : retained < leading + 2) (hsuccessor : GuardStickyRounding.streamPrefix (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained + 1 < 2 ^ retained) : (↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField < trailingRat retained (GuardStickyRounding.streamPrefix (GuardStickyRounding.exactTailRaw exponentField (StickyPrefix.jamRemainder quotient remainder) leading) (leading + 2) retained + 1)

The exact normalized quotient is below the successor of its retained jammed prefix.

The explicit successor bound is precisely the in-regime condition supplied by Posit layout.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.quotientFraction_normalized_lt_sixteen (exponentField quotient remainder denominator leading : ℕ) (hexponent : exponentField < 4) (hupper : quotient < 2 ^ (leading + 1)) (hdenominator : 0 < denominator) (hremainder : remainder < denominator) : (↑quotient + ↑remainder / ↑denominator) / ↑(2 ^ leading) * 2 ^ Int.ofNat exponentField < 16

Every normalized quotient tail is strictly below the next regime scale.

Recovering the input dyadic ratio

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.scaledRatio_eq_quotientFraction (numerator denominator steps : ℕ) (hdenominator : denominator ≠ 0) : ↑numerator * ↑(2 ^ steps) / ↑denominator = ↑(numerator * 2 ^ steps / denominator) + ↑(numerator * 2 ^ steps % denominator) / ↑denominator

Euclidean division exposes a scaled rational as its quotient plus proper remainder.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.dyadicRatio_eq_quotientFraction_mul_zpow (numerator denominator normalizedNumerator normalizedDenominator quotient remainder : ℕ) (numeratorExponent denominatorExponent : ℤ) (numeratorLeading denominatorLeading steps : ℕ) (hnormalized : ↑normalizedNumerator / ↑normalizedDenominator = ↑numerator / ↑denominator * 2 ^ (Int.ofNat denominatorLeading - Int.ofNat numeratorLeading)) (hquotient : ↑normalizedNumerator * ↑(2 ^ steps) / ↑normalizedDenominator = ↑quotient + ↑remainder / ↑normalizedDenominator) : ↑numerator * 2 ^ numeratorExponent / (↑denominator * 2 ^ denominatorExponent) = (↑quotient + ↑remainder / ↑normalizedDenominator) * 2 ^ (numeratorExponent - denominatorExponent + Int.ofNat numeratorLeading - Int.ofNat denominatorLeading - Int.ofNat steps)

Moving the normalization and quotient-digit scales into the result exponent recovers the exact dyadic ratio.

Executable prefix correctness

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.prefixAtLeading_quotient_spec (leading : ℕ) (numerator denominator : Numerics.Dyadic) (hnumerator : numerator.significand ≠ 0) (hdenominator : denominator.significand ≠ 0) : have normalized := normalizeSignificands numerator.significand denominator.significand; have steps := if normalized.numerator < normalized.denominator then leading + 1 else leading; have scaledNumerator := normalized.numerator * 2 ^ steps; 0 < normalized.denominator ∧ 2 ^ leading ≤ scaledNumerator / normalized.denominator ∧ scaledNumerator / normalized.denominator < 2 ^ (leading + 1) ∧ scaledNumerator % normalized.denominator < normalized.denominator

The quotient and remainder generated by an arbitrary-width prefix form a normalized Euclidean window at exactly the requested leading bit.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.prefixAtLeading_significand_bounds (leading : ℕ) (numerator denominator : Numerics.Dyadic) (hnumerator : numerator.significand ≠ 0) (hdenominator : denominator.significand ≠ 0) : 2 ^ leading ≤ (prefixAtLeading leading numerator denominator).significand ∧ (prefixAtLeading leading numerator denominator).significand < 2 ^ (leading + 1)

The executable arbitrary-width prefix is normalized at exactly the requested leading bit.

theorem FloatLib.Floats.Formats.Posit.Model.DirectDyadicQuotient.prefixAtLeading_exactFraction (leading : ℕ) (numerator denominator : Numerics.Dyadic) (hnumerator : numerator.significand ≠ 0) (hdenominator : denominator.significand ≠ 0) (hnumeratorNegative : numerator.negative = false) (hdenominatorNegative : denominator.negative = false) : have normalized := normalizeSignificands numerator.significand denominator.significand; have steps := if normalized.numerator < normalized.denominator then leading + 1 else leading; have scaledNumerator := normalized.numerator * 2 ^ steps; numerator.toRat / denominator.toRat = (↑(scaledNumerator / normalized.denominator) + ↑(scaledNumerator % normalized.denominator) / ↑normalized.denominator) * 2 ^ (numerator.exponent - denominator.exponent + Int.ofNat normalized.numeratorLeading - Int.ofNat normalized.denominatorLeading - Int.ofNat steps)

Before jamming, the generated quotient and exact Euclidean remainder denote the input dyadic ratio at the exponent stored in the executable prefix.