Refinement of P3109 block roots

A finite nonzero result scale normalizes the exact real root before precision rounding. The executable square comparisons agree with the real-root reference in every rounding mode, and the final encoder preserves the signed, rounded, and saturated datum.

@[simp]

theorem FloatLib.Floats.Formats.P3109.BlockRoot.normalize_finite (scale radicand : ℚ) (hscale : scale ≠ 0) (hrad : 0 ≤ radicand) : normalize (Numerics.NumericalValue.finite scale) (Numerics.NumericalValue.finite radicand) = { negative := decide (scale < 0), radicand := Numerics.NumericalValue.finite (radicand / (scale * scale)) }

Exact normalization of a valid finite root by a finite nonzero scale.

theorem FloatLib.Floats.Formats.P3109.BlockRoot.normalize_finite_real (scale radicand : ℚ) (hscale : scale ≠ 0) (hrad : 0 ≤ radicand) : (if scale < 0 then -1 else 1) * √↑(radicand / (scale * scale)) = √↑radicand / ↑scale

The exact normalized root denotes sqrt(q) / s, including negative scales.

noncomputable def FloatLib.Floats.Formats.P3109.BlockRoot.roundedReal (format : Format) (mode : RoundingMode) (root : BlockRoot) : Numerics.NumericalValue Numerics.Dyadic

Reference signed-root rounding through the real square root.

theorem FloatLib.Floats.Formats.P3109.BlockRoot.rounded_eq_real (format : Format) (mode : RoundingMode) (root : BlockRoot) : rounded format mode root = roundedReal format mode root

Executable signed-root rounding agrees with the real-root reference for every policy.

theorem FloatLib.Floats.Formats.P3109.BlockRoot.rounded_fitsPrecisionGrid (format : Format) (mode : RoundingMode) (root : BlockRoot) : match rounded format mode root with | Numerics.NumericalValue.finite value => format.FitsPrecisionGrid value | x => True

Signed-root precision rounding always lands on the destination's precision grid.

theorem FloatLib.Floats.Formats.P3109.BlockRoot.decode_project (format : Format) (policy : ProjectionPolicy) (root : BlockRoot) : Format.SameDatum (project format policy root).decode (value format policy root)

Final P3109 encoding preserves the root's single rounded and saturated result.