Grid Invariants for NF

NF permits raw real-valued construction for approximation proofs, while its smart constructor and primitive arithmetic round onto the declared format. This file proves the corresponding NF.IsRepresentable closure properties without adding generic-format theory to the core scalar module's import surface.

theorem FloatLib.Floats.Formats.Flocq.NF.isRepresentable_ofReal {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] [ValidRnd rnd] (x : ℝ) : (ofReal x).IsRepresentable

The smart constructor rounds its input onto the declared format grid.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.isRepresentable_neg {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] [ValidRnd rnd] (a : NF β fexp rnd) : (-a).IsRepresentable

Negation through the smart constructor remains on the declared format grid.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.isRepresentable_add {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] [ValidRnd rnd] (a b : NF β fexp rnd) : (a + b).IsRepresentable

Addition through the smart constructor remains on the declared format grid.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.isRepresentable_sub {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] [ValidRnd rnd] (a b : NF β fexp rnd) : (a - b).IsRepresentable

Subtraction through the smart constructor remains on the declared format grid.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.isRepresentable_mul {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] [ValidRnd rnd] (a b : NF β fexp rnd) : (a * b).IsRepresentable

Multiplication through the smart constructor remains on the declared format grid.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.NF.isRepresentable_div {β : Numerics.Radix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} [ValidExp fexp] [ValidRnd rnd] (a b : NF β fexp rnd) : (a / b).IsRepresentable

Division through the smart constructor remains on the declared format grid.