Correctness of shared-scale blocks

The direct vector kernel implements contextual quantization, and the format satisfies the generic block-scaled representation capability.

@[simp]

theorem FloatLib.Floats.Formats.Block.represents_iff {lanes : ℕ} (code : Numerics.FormatCode (SharedScale lanes)) (value : Vector ℚ lanes) : Numerics.FormatRepresents (SharedScale lanes) code value ↔ decode code = value

The common format represents exactly its vector-valued block denotation.

theorem FloatLib.Floats.Formats.Block.quantizesAt_quantizeAt {lanes : ℕ} (exponent : ℤ) (input : Vector ℚ lanes) : QuantizesAt exponent input (quantizeAt exponent input)

The direct vector kernel satisfies the contextual relational specification.

theorem FloatLib.Floats.Formats.Block.quantizeAt_refines (lanes : ℕ) : Numerics.Quantization.Spec.Implements QuantizesAt quantizeAt

quantizeAt implements shared-scale contextual quantization.

theorem FloatLib.Floats.Formats.Block.scale_pos (exponent : ℤ) : 0 < scale exponent

The shared binary scale is strictly positive.

theorem FloatLib.Floats.Formats.Block.blockScaled_sharedScale (lanes : ℕ) : Numerics.BlockScaled (Numerics.formatSystem (SharedScale lanes)) (Fin lanes) ℤ ℤ ℚ (fun (block : Vector ℚ lanes) (lane : Fin lanes) => block[↑lane]) (fun (code : SharedScaleCode lanes) => code.exponent) (fun (code : SharedScaleCode lanes) (lane : Fin lanes) => code.significands[↑lane]) fun (exponent significand : ℤ) => ↑significand * scale exponent

The proof-facing block-scaled capability for the unbounded shared-scale representation.

Executable decoding still projects the exponent and significands directly.

@[simp]

theorem FloatLib.Floats.Formats.Block.decode_quantizeAt_get {lanes : ℕ} (exponent : ℤ) (input : Vector ℚ lanes) (lane : Fin lanes) : (decode (quantizeAt exponent input))[↑lane] = ↑(Numerics.roundRatEven (input[↑lane] / scale exponent)) * scale exponent

Decoding a freshly quantized block exposes nearest-even reconstruction lane by lane.