Requested precision for external decimal text

The digit grid and decade carry depend only on an exact decimal value. A caller supplies the signed magnitude-to-integer rounding function; this module makes no choice of source format, exponent bounds, cohort policy, or exception handling. It applies equally to decimal datums and terminating decimal expansions of dyadics.

Requested precision has no width cap. Zero uses adjusted exponent zero, hence quantum 1-p at precision p. Sign preservation includes signed zero.

inductive FloatLib.Numerics.DecimalText.Precision : Type

Exact representation and a requested significant-digit count are distinct output modes.

• exact : Precision
• significant (digits : ℕ+) : Precision

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

Decimal position of the last requested digit.

def FloatLib.Numerics.DecimalText.roundDecimal (roundMagnitude : Bool → ℚ → ℕ) (value : Decimal) (quantum : ℤ) : Decimal

Round on a decimal grid with the caller's magnitude-to-integer rounding function.

def FloatLib.Numerics.DecimalText.carryDecimal (digits : ℕ+) (value : Decimal) : Decimal

Carry into a new decade without adding an extra significant digit.

def FloatLib.Numerics.DecimalText.significantDecimal (roundMagnitude : Bool → ℚ → ℕ) (value : Decimal) (digits : ℕ+) : Decimal

One rounding at the requested significant-digit grid, followed by a value-preserving carry.