Laws of significant-digit rounding in any radix

The caller supplies integer rounding. These laws establish the grid, coefficient bounds and value-preserving carry independently of decimal or binary descriptors.

theorem FloatLib.Numerics.RadixText.carry_value (radix : ℕ) (hradix : 0 < radix) (digits : ℕ+) (coefficient : ℕ) (quantum : ℤ) : ↑(carry radix digits coefficient quantum).1 * ↑radix ^ (carry radix digits coefficient quantum).2 = ↑coefficient * ↑radix ^ quantum

Carry changes the written scale without changing the numerical value.

theorem FloatLib.Numerics.RadixText.significant_value (radix : ℕ) (hradix : 0 < radix) (roundMagnitude : Bool → ℚ → ℕ) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : ↑(significant radix roundMagnitude negative coefficient quantum digits).1 * ↑radix ^ (significant radix roundMagnitude negative coefficient quantum digits).2 = ↑(roundCoefficient radix roundMagnitude negative coefficient quantum (significantQuantum radix coefficient quantum digits)) * ↑radix ^ significantQuantum radix coefficient quantum digits

The written result denotes precisely the caller's integer rounding on the selected grid.

theorem FloatLib.Numerics.RadixText.scaled_lt (radix : ℕ) (hradix : 1 < radix) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : ↑coefficient * ↑radix ^ quantum / ↑radix ^ significantQuantum radix coefficient quantum digits < ↑radix ^ ↑digits

The coefficient before rounding is strictly smaller than the radix to the requested precision.

theorem FloatLib.Numerics.RadixText.scaled_lower (radix : ℕ) (hradix : 1 < radix) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) (hc : coefficient ≠ 0) : ↑radix ^ (↑digits - 1) ≤ ↑coefficient * ↑radix ^ quantum / ↑radix ^ significantQuantum radix coefficient quantum digits

A nonzero coefficient scaled to its requested grid has the expected leading digit.

theorem FloatLib.Numerics.RadixText.significant_coefficient_bounds (radix : ℕ) (hradix : 1 < radix) (roundMagnitude : Bool → ℚ → ℕ) (hlower : ∀ (sign : Bool) (x : ℚ), ⌊x⌋₊ ≤ roundMagnitude sign x) (hupper : ∀ (sign : Bool) (x : ℚ) (n : ℕ), 0 ≤ x → x ≤ ↑n → roundMagnitude sign x ≤ n) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) (hc : coefficient ≠ 0) : radix ^ (↑digits - 1) ≤ (significant radix roundMagnitude negative coefficient quantum digits).1 ∧ (significant radix roundMagnitude negative coefficient quantum digits).1 < radix ^ ↑digits

For a nonzero input, a rounder between floor and ceiling emits the requested digit count.

theorem FloatLib.Numerics.RadixText.significant_exact (radix : ℕ) (hradix : 1 < radix) (roundMagnitude : Bool → ℚ → ℕ) (hexact : ∀ (sign : Bool) (n : ℕ), roundMagnitude sign ↑n = n) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) (hc : coefficient < radix ^ ↑digits) : ↑(significant radix roundMagnitude negative coefficient quantum digits).1 * ↑radix ^ (significant radix roundMagnitude negative coefficient quantum digits).2 = ↑coefficient * ↑radix ^ quantum

Enough requested digits preserve value whenever integer inputs are fixed by the rounder.

theorem FloatLib.Numerics.RadixText.significant_error (radix : ℕ) (hradix : 0 < radix) (roundMagnitude : Bool → ℚ → ℕ) (error : ℚ) (herror : ∀ (sign : Bool) (x : ℚ), 0 ≤ x → |↑(roundMagnitude sign x) - x| ≤ error) (negative : Bool) (coefficient : ℕ) (quantum : ℤ) (digits : ℕ+) : |↑(significant radix roundMagnitude negative coefficient quantum digits).1 * ↑radix ^ (significant radix roundMagnitude negative coefficient quantum digits).2 - ↑coefficient * ↑radix ^ quantum| ≤ error * ↑radix ^ significantQuantum radix coefficient quantum digits

An integer rounding error bound scales by the requested external grid unit.