Rounded-Real Scalars As Specification Contexts

FloatLib's NF models a real value rounded onto a selected radix/exponent grid. This adapter supplies TorchLean's specification dictionary for that same carrier; it is noncomputable. Executable configured binary tensors use NN.Spec.Core.FloatInstances instead.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instAtan2 {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Atan2 (NF β fexp rnd)

Evaluate the principal polar angle in the reals, then round onto the selected grid.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.natCast_eq_ofReal {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] (n : ℕ) : ↑n = ofReal ↑n

Unfold the natural-number cast into the rounded real it denotes.

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.NF.instContext {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] : Context (NF β fexp rnd)

Use rounded-real NF arithmetic as a TorchLean specification scalar.

The general scalar interface requires a total α ^ α. Its adapter uses NF.checkedRealPow, which handles arbitrary exponents on positive bases, integer exponents on negative bases, and positive exponents at zero. The adapter selects its rounded-zero fallback only when checkedRealPow rejects the domain, such as a negative base with a noninteger exponent or zero with a negative exponent; an accepted computation can independently round to zero. Direct numerical code should inspect the checked result, or use the unambiguous NF.powNat, rather than relying on that compatibility fallback.

Rational casts round the exact real fraction once. The default safeguard rounds 1e-6 onto the chosen grid and can be zero: a general exponent function and rounding rule do not supply the smallest-positive-value contract of a configured binary format. This dictionary supplies no LawfulContext or positive-tolerance theorem.