Executable exact-dyadic comparison

The general comparator aligns significands at a common exponent. The Internal.compareScalable variants first compare leading binary positions, avoiding shifts proportional to a potentially huge exponent gap. Comparison.Proof connects the field-level entry points and normalization tests to the general comparator; rational ordering laws are in Dyadic.Order.

@[inline]

def FloatLib.Numerics.Dyadic.Internal.compareNonzeroMagnitudes (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : Ordering

Compare two nonzero dyadic magnitudes without allocating across the full exponent gap.

Different leading binary positions decide the result immediately. Equal leading positions imply that exponent alignment shifts by no more than the difference between the two significand widths, even when the stored exponents themselves are enormous.

@[inline]

def FloatLib.Numerics.Dyadic.Internal.compareScalableFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Ordering

Compare exact dyadic fields with alignment shifts bounded by significand widths.

Zero and opposite-sign cases need no magnitude comparison. Same-sign nonzero inputs use their leading binary positions before any bounded alignment.

@[inline]

def FloatLib.Numerics.Dyadic.Internal.compareScalable (left right : Dyadic) : Ordering

Record-based entry point for exponent-scalable exact-dyadic comparison.

@[inline]

def FloatLib.Numerics.Dyadic.compareFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Ordering

Compare exact dyadic scalar fields without first allocating either Dyadic record.

Format-specific decoders often already expose sign, significand, and exponent separately. This entry point preserves that flattened representation through exact comparison.

@[inline]

def FloatLib.Numerics.Dyadic.compare (left right : Dyadic) : Ordering

Compare two exact dyadic values.

The comparison aligns only to the smaller of the two exponents and then compares signed integers; it never converts through a host floating-point value.

@[inline]

def FloatLib.Numerics.Dyadic.compareNonnegativeFields (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : Ordering

Compare two nonnegative significand/exponent pairs without constructing signed integers.

Posit and unsigned binary rounding spend most comparisons in this domain. Because the common exponent is always one of the two input exponents, only the significand at the larger exponent needs shifting.

@[inline]

def FloatLib.Numerics.Dyadic.isLess (left right : Dyadic) : Bool

Executable strict comparison without conversion to Rat or a host floating-point value.

@[inline]

def FloatLib.Numerics.Dyadic.isLessFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Bool

Executable strict comparison on flattened exact-dyadic fields.

@[inline]

def FloatLib.Numerics.Dyadic.isLessNonnegativeFields (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : Bool

Strict comparison specialized to known-nonnegative scalar fields.

@[inline]

def FloatLib.Numerics.Dyadic.isLessPowerOfTwoAtLeading (significand : ℕ) (exponent : ℤ) (leading : ℕ) (power : ℤ) : Bool

Test whether a nonnegative dyadic is strictly below an integral power of two when the caller already knows the significand's leading-bit index.

Rounding kernels compute this index to normalize their result fields. Reusing it here avoids an alignment shift whose temporary size is proportional to the exponent gap.

@[inline]

def FloatLib.Numerics.Dyadic.isLessOrEqual (left right : Dyadic) : Bool

Executable non-strict comparison, derived from the exact strict comparator.

@[inline]

def FloatLib.Numerics.Dyadic.isEqual (left right : Dyadic) : Bool

Executable numerical equality for possibly unnormalized dyadics.

Structural equality is intentionally unsuitable here because the same number may have several significand/exponent pairs.

@[inline]

def FloatLib.Numerics.Dyadic.isLessOrEqualFields (leftNegative : Bool) (leftSignificand : ℕ) (leftExponent : ℤ) (rightNegative : Bool) (rightSignificand : ℕ) (rightExponent : ℤ) : Bool

Executable non-strict comparison on flattened exact-dyadic fields.

@[inline]

def FloatLib.Numerics.Dyadic.isLessOrEqualNonnegativeFields (leftSignificand : ℕ) (leftExponent : ℤ) (rightSignificand : ℕ) (rightExponent : ℤ) : Bool

Non-strict comparison specialized to known-nonnegative scalar fields.