Shared-scale block conversion proofs

The principal result proves that direct block conversion satisfies the lane-wise nearest-even QuantizesAt relation at the caller-supplied shared exponent.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.Conversion.run_finite {lanes : ℕ} (exponent : ℤ) (exact : Vector ℚ lanes) : run exponent (Numerics.NumericalValue.finite exact) = have rounded := quantizeAt exponent exact; ConversionOutcome.success rounded (status exact rounded)

Finite vectors are quantized lane-wise at the explicitly supplied exponent.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.Conversion.run_infinity {lanes : ℕ} (exponent : ℤ) (negative : Bool) : run exponent (Numerics.NumericalValue.infinity negative) = ConversionOutcome.failure (ConversionFailure.infinity InputPosition.source negative)

The generic shared-scale block has no infinity encoding.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.Conversion.run_exceptional {lanes : ℕ} (exponent : ℤ) (exceptional : Numerics.ExceptionalValue) : run exponent (Numerics.NumericalValue.exceptional exceptional) = ConversionOutcome.failure (ConversionFailure.exceptional InputPosition.source exceptional)

The generic shared-scale block has no exceptional encoding.

theorem FloatLib.Floats.ExecFloat.SharedScale.Conversion.implements_run {lanes : ℕ} : Numerics.Quantization.Spec.Implements spec run

The direct configured block converter satisfies the lane-wise relational specification.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.Conversion.exactDecoder_run {lanes : ℕ} (value : SharedScale lanes) : ExactDecoder.run value = Numerics.NumericalValue.finite value.decode

The installed decoder exposes the exact decoded block.

@[simp]

theorem FloatLib.Floats.ExecFloat.SharedScale.Conversion.exponent_of_finite_run {lanes : ℕ} (exponent : ℤ) (exact : Vector ℚ lanes) : Option.map SharedScale.exponent (run exponent (Numerics.NumericalValue.finite exact)).value? = some exponent

The explicit exponent supplied to conversion is stored exactly.