Significant-digit rounding on an arbitrary radix grid

Decimal and hexadecimal output share the grid calculation, one integer rounding, and carry. The radix and rounding callback are explicit; there are no format widths or exponent limits here. Meaningful radix semantics require 1 < radix.

def FloatLib.Numerics.RadixText.significantQuantum (radix coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : ℤ

Exponent of the last requested radix digit, with adjusted exponent zero for zero.

def FloatLib.Numerics.RadixText.roundCoefficient (radix : ℕ) (roundMagnitude : Bool → ℚ → ℕ) (negative : Bool) (coefficient : ℕ) (quantum destination : ℤ) : ℕ

Round a coefficient onto another grid using an exact magnitude-rounding callback.

def FloatLib.Numerics.RadixText.carry (radix : ℕ) (digits : ℕ+) (coefficient : ℕ) (quantum : ℤ) : ℕ × ℤ

Carry a rounded coefficient into the next radix position without changing its value.

def FloatLib.Numerics.RadixText.significant (radix : ℕ) (roundMagnitude : Bool → ℚ → ℕ) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : ℕ × ℤ

One significant-digit rounding, followed by a value-preserving radix carry.