Correctness of configured shared-scale blocks

Wrapping and unwrapping preserve the complete block code. quantizesAt_quantizeAt lifts the model's lane-wise nearest-even rounding theorem to configured blocks, at the exponent supplied by the caller.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.toCode_ofCode {lanes : ℕ} (code : Formats.Block.SharedScaleCode lanes) : (ofCode code).toCode = code

Unwrapping a freshly wrapped shared-scale block returns the original code.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.ofCode_toCode {lanes : ℕ} (value : SharedScale lanes) : ofCode value.toCode = value

Rewrapping the code of a shared-scale block returns the original value.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.exponent_quantizeAt {lanes : ℕ} (exponent : ℤ) (input : Vector ℚ lanes) : (quantizeAt exponent input).exponent = exponent

Quantization records exactly the shared exponent supplied by the caller.

@[simp]

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

Each decoded quantized lane is its nearest-even integer multiple of the shared scale.

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

The configured wrapper preserves relational contextual quantization.