Hexadecimal character preservation

The shared positional scanner recovers the printed hexadecimal coefficient; the decimal integer scanner recovers the binary exponent. The result preserves the entire dyadic record, including the sign of zero.

@[simp]

theorem FloatLib.Numerics.HexText.digitValue?_digitChar {digit : ℕ} (hdigit : digit < 16) : digitValue? digit.digitChar = some digit

A printed hexadecimal digit decodes to its original value.

theorem FloatLib.Numerics.HexText.scanDigits_naturalDigits (value : ℕ) (tail : List Char) (htail : ∀ character ∈ tail.head?, digitValue? character = none) : RadixText.scanDigits (RadixText.naturalDigits value 16 ++ tail) 0 16 digitValue? = (value, (RadixText.naturalDigits value 16).length, tail)

Scanning a printed hexadecimal coefficient recovers the coefficient and its suffix.

theorem FloatLib.Numerics.HexText.parseMagnitude_hexadecimal (significand : ℕ) (exponent : ℤ) : RadixText.parseMagnitude (RadixText.naturalDigits significand 16 ++ 'p' :: DecimalText.integerDigits exponent) 16 digitValue? parseExponent 4 = some (significand, exponent)

The complete hexadecimal magnitude, including its mandatory exponent, parses exactly.

@[simp]

theorem FloatLib.Numerics.HexText.parseCharacters_characters (value : Dyadic) : parseCharacters (characters value) = some value

Reading the printed characters preserves every dyadic field, with no width assumption.

@[simp]

theorem FloatLib.Numerics.HexText.parse_format (value : Dyadic) : parse (format value) = some value

Exact hexadecimal string output and input preserve the full dyadic representation.

theorem FloatLib.Numerics.HexText.sixteen_zpow (exponent : ℤ) : 16 ^ exponent = 2 ^ (4 * exponent)

A hexadecimal power is a binary power at four times the exponent.

theorem FloatLib.Numerics.HexText.radixPair_value (value : Dyadic) : ↑(radixPair value).1 * 16 ^ (radixPair value).2 = ↑value.significand * 2 ^ value.exponent

Moving a dyadic to a hexadecimal grid does not change its magnitude.

@[simp]

theorem FloatLib.Numerics.HexText.significant_negative (roundMagnitude : Bool → ℚ → ℕ) (value : Dyadic) (digits : ℕ+) : (significant roundMagnitude value digits).negative = value.negative

Hexadecimal precision output preserves the sign, even if the coefficient is zero.

theorem FloatLib.Numerics.HexText.significant_value (roundMagnitude : Bool → ℚ → ℕ) (value : Dyadic) (digits : ℕ+) : (significant roundMagnitude value digits).toRat = (if value.negative = true then -1 else 1) * ↑(RadixText.roundCoefficient 16 roundMagnitude value.negative (radixPair value).1 (radixPair value).2 (RadixText.significantQuantum 16 (radixPair value).1 (radixPair value).2 digits)) * 16 ^ RadixText.significantQuantum 16 (radixPair value).1 (radixPair value).2 digits

The hexadecimal output value is one integer rounding on the requested hexadecimal grid.

theorem FloatLib.Numerics.HexText.significant_exact (roundMagnitude : Bool → ℚ → ℕ) (hexact : ∀ (sign : Bool) (n : ℕ), roundMagnitude sign ↑n = n) (value : Dyadic) (digits : ℕ+) (hc : (radixPair value).1 < 16 ^ ↑digits) : (significant roundMagnitude value digits).toRat = value.toRat

Enough requested hexadecimal digits preserve the exact value in every integer-exact rounder.