Executable floating-point powers

Model.pow provides one deterministic power policy for every FloatFormat. Small nonnegative integer exponents use a linear sequence of rounded multiplications. Small negative integer exponents of finite nonzero bases use an exact scaled rational and round once, avoiding intermediate overflow or underflow before inversion. Larger integer exponents and non-integer exponents use the generic exp and log kernels.

Integer exponents are classified directly from their dyadic representation. The classifier records sign, parity, and an optional bounded magnitude without constructing an integer whose bit length is controlled by the floating-point exponent field. This is essential for formats with wide exponent fields.

The general exp/log path is approximate; this module does not prove correct rounding for real exponentiation.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.smallPowLimit : ℕ

Largest integer magnitude evaluated directly rather than through exp and log.

structure FloatLib.Floats.Formats.BinaryInterchange.Model.Power.IntegerExponent : Type

Information needed to evaluate a finite integral floating-point exponent.

smallMagnitude? is populated exactly when the magnitude is at most smallPowLimit.

• negative : Bool

  Whether the nonzero integer is negative.

• odd : Bool

  Whether its magnitude is odd.

• smallMagnitude? : Option ℕ

  Its magnitude when small enough for direct evaluation.

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprIntegerExponent : Repr IntegerExponent

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instReprIntegerExponent.repr : IntegerExponent → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqIntegerExponent : DecidableEq IntegerExponent

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.instDecidableEqIntegerExponent.decEq (x✝ x✝¹ : IntegerExponent) : Decidable (x✝ = x✝¹)

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.smallMagnitude (magnitude : ℕ) : Option ℕ

Return a magnitude when it is within the direct evaluation limit.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.classifyIntegerDyadic? (value : Numerics.Dyadic) : Option IntegerExponent

Classify a finite dyadic as an integer.

For a nonnegative dyadic exponent, the left shift is bounded by log₂ smallPowLimit; the shifted magnitude is then checked against the limit. For a negative exponent, divisibility is checked only when the right shift is no greater than the significand's leading bit index.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.classifyInteger? {fmt : FloatFormat} (value : Model fmt) : Option IntegerExponent

Classify an executable finite value as an integer exponent.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.powNatLinear {fmt : FloatFormat} (base : Model fmt) : ℕ → Model fmt

Repeated rounded multiplication with recurrence p₀ = 1, pₙ₊₁ = base * pₙ.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.powSmallInteger {fmt : FloatFormat} (base : Model fmt) (metadata : IntegerExponent) (magnitude : ℕ) : Model fmt

Evaluate the direct integer-power path. Callers select magnitudes at most smallPowLimit.

For a finite nonzero base s * 2^e, a negative exponent of magnitude n is rounded from (1 / s^n) * 2^(-e*n). Only the significand is raised to a power, so the denominator's size is bounded by the input precision and smallPowLimit, independently of the exponent range. Exceptional bases retain the division and multiplication policies of the format.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Power.powIntegerDet {fmt : FloatFormat} (base exponent : Model fmt) (metadata : IntegerExponent) : Model fmt

Evaluate the integer-power branch before pow applies the negative-base sign rule.

Large magnitudes use the deterministic general path exp (b * log |a|).

def FloatLib.Floats.Formats.BinaryInterchange.Model.pow {fmt : FloatFormat} (base exponent : Model fmt) : Model fmt

Deterministic executable floating-point exponentiation.

The special cases and branch order are explicit:

• x^(+-0) = 1, including a NaN base;
• 1^y = 1 except for a signaling-NaN exponent;
• infinite exponents are classified by |x| relative to one;
• finite negative bases require an integral exponent;
• signed zero and negative infinity retain a negative result exactly for odd integer exponents.