P3109 block square roots and norms

Block roots normalize the exact root at the result scale before rounding. A finite nonzero scale s turns sqrt(q) / s into the signed root of q / s². Exact square comparisons then perform one destination rounding, including negative scales and lane-specific stochastic words. The zero, infinite, and NaN scale rules are those of ordinary block projection.

structure FloatLib.Floats.Formats.P3109.BlockRoot : Type

An exact signed root of a closed rational radicand, before destination rounding.

• negative : Bool

  Sign of the result after normalization at a possibly negative scale.

• radicand : Numerics.NumericalValue ℚ

  Squared magnitude. Square-root rounding sends a negative finite radicand to NaN.

def FloatLib.Floats.Formats.P3109.instDecidableEqBlockRoot.decEq (x✝ x✝¹ : BlockRoot) : Decidable (x✝ = x✝¹)

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instDecidableEqBlockRoot : DecidableEq BlockRoot

@[instance_reducible]

instance FloatLib.Floats.Formats.P3109.instReprBlockRoot : Repr BlockRoot

def FloatLib.Floats.Formats.P3109.instReprBlockRoot.repr : BlockRoot → ℕ → Std.Format

def FloatLib.Floats.Formats.P3109.BlockRoot.normalize (scale radicand : Numerics.NumericalValue ℚ) : BlockRoot

Normalize an exact square root under the special scale rules of §5.4.2.

def FloatLib.Floats.Formats.P3109.BlockRoot.magnitudeMode (negative : Bool) : RoundingMode → RoundingMode

Directed rounding of a negative root reverses the direction on its positive magnitude.

def FloatLib.Floats.Formats.P3109.BlockRoot.applySign (negative : Bool) : Numerics.NumericalValue Numerics.Dyadic → Numerics.NumericalValue Numerics.Dyadic

Apply a root's sign after magnitude rounding, retaining the closed exceptional rules.

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

Round the normalized signed root once to the destination precision by exact square tests.

def FloatLib.Floats.Formats.P3109.BlockRoot.value (format : Format) (policy : ProjectionPolicy) (root : BlockRoot) : Numerics.NumericalValue Numerics.Dyadic

Saturate the rounded signed root in the requested direction, not the magnitude direction.

def FloatLib.Floats.Formats.P3109.BlockRoot.project (format : Format) (policy : ProjectionPolicy) (root : BlockRoot) : ExecFloat.P3109 format

Encode a normalized root after its single precision rounding and saturation.

def FloatLib.Floats.Formats.P3109.Block.projectRoots {length : ℕ+} {ResultScale ResultScaleExact : Type} [ExecFloat.ExactDecoder ResultScale ResultScaleExact] [ExecFloat.ExactMap ResultScaleExact ℚ] (format : Format) (policy : BlockPolicy length) (scale : ResultScale) (radicands : Vector (Numerics.NumericalValue ℚ) ↑length) : Block ResultScale (ExecFloat.P3109 format) length

Project exact root radicands at a shared result scale, with independent lane rounding words.

def FloatLib.Floats.Formats.P3109.Block.sqrt {length : ℕ+} {Scale ScaleExact Source SourceExact ResultScale ResultScaleExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] [ExecFloat.ExactDecoder ResultScale ResultScaleExact] [ExecFloat.ExactMap ResultScaleExact ℚ] (format : Format) (policy : BlockPolicy length) (block : Block Scale Source length) (resultScale : ResultScale) : Block ResultScale (ExecFloat.P3109 format) length

Elementwise square root, normalized before the single final destination rounding.

def FloatLib.Floats.Formats.P3109.Block.rsqrt {length : ℕ+} {Scale ScaleExact Source SourceExact ResultScale ResultScaleExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] [ExecFloat.ExactDecoder ResultScale ResultScaleExact] [ExecFloat.ExactMap ResultScaleExact ℚ] (format : Format) (policy : BlockPolicy length) (block : Block Scale Source length) (resultScale : ResultScale) : Block ResultScale (ExecFloat.P3109 format) length

Elementwise reciprocal square root with the report's nonpositive-domain rule.

def FloatLib.Floats.Formats.P3109.Block.hypot {length : ℕ+} {Scale ScaleExact Source SourceExact ResultScale ResultScaleExact : Type} [ExecFloat.ExactDecoder Scale ScaleExact] [ExecFloat.ExactMap ScaleExact ℚ] [ExecFloat.ExactDecoder Source SourceExact] [ExecFloat.ExactMap SourceExact ℚ] [ExecFloat.ExactDecoder ResultScale ResultScaleExact] [ExecFloat.ExactMap ResultScaleExact ℚ] {RightScale RightScaleExact Right RightExact : Type} [ExecFloat.ExactDecoder RightScale RightScaleExact] [ExecFloat.ExactMap RightScaleExact ℚ] [ExecFloat.ExactDecoder Right RightExact] [ExecFloat.ExactMap RightExact ℚ] (format : Format) (policy : BlockPolicy length) (left : Block Scale Source length) (right : Block RightScale Right length) (resultScale : ResultScale) : Block ResultScale (ExecFloat.P3109 format) length

Elementwise hypotenuse of independently scaled sources, retaining the exact sum of squares.