Real-valued posit rounding specification

The exact rational posit rounding specification has a noncomputable interpretation in ℝ. This interpretation belongs to the semantic proof layer: executable arithmetic continues to use the rational, dyadic, native-word, and fixed-limb kernels.

The real specification lets refinement theorems state correctness against conventional analytic operations such as Real.sqrt, without adding real-number evaluation to a runtime dependency.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.nonnegativeRealAt (format : Format) (code : ℕ) : ℝ

Real value of the posit word with unsigned code code.

The intended domain is code < format.signMaskNat. In general the code is reduced modulo the format's modulus before decoding; zero and NaR map to zero, and other words retain their sign.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.lowerCode (format : Format) (target : ℝ) : ℕ

For a nonnegative target, the greatest code whose real denotation does not exceed it.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.minPositive (format : Format) : ℝ

Exact smallest positive real value of a posit format.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.roundingThreshold (format : Format) (lowerCode : ℕ) : ℝ

Exact appended-bit rounding threshold interpreted in the reals.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode (format : Format) (target : ℝ) : ℕ

Round a real to a nonnegative posit code, sending nonpositive targets to zero.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositive (format : Format) (target : ℝ) : Model format

Model-valued rounding of a nonnegative real target.

noncomputable def FloatLib.Floats.Formats.Posit.Model.RealRounding.round (format : Format) (target : ℝ) : Model format

Round a signed real by the standard whole-word negation symmetry.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.lowerCode_ratCast (format : Format) (target : ℚ) : lowerCode format ↑target = lowerCodeForPositive format target

Real lower-code search agrees with rational lower-code search after exact coercion.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.lowerCode_mono (format : Format) : Monotone (lowerCode format)

Real lower-code search is monotone in its target.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.lowerCode_minPositive (format : Format) : lowerCode format (minPositive format) = 1

The minimum positive value has lower code one.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode_bounds (format : Format) (target : ℝ) (hpositive : 0 < target) (hminimum : minPositive format ≤ target) : lowerCode format target ≤ roundPositiveCode format target ∧ roundPositiveCode format target ≤ lowerCode format target + 1

Interior positive rounding selects either its lower code or its immediate successor.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode_eq_lower_of_lt_threshold (format : Format) (target : ℝ) (hpositive : 0 < target) (hminimum : minPositive format ≤ target) (hupper : lowerCode format target + 1 < format.signMaskNat) (hbelow : target < roundingThreshold format (lowerCode format target)) : roundPositiveCode format target = lowerCode format target

An interior target below its appended-bit boundary selects the lower code.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode_eq_succ_of_threshold_lt (format : Format) (target : ℝ) (hpositive : 0 < target) (hminimum : minPositive format ≤ target) (hupper : lowerCode format target + 1 < format.signMaskNat) (habove : roundingThreshold format (lowerCode format target) < target) : roundPositiveCode format target = lowerCode format target + 1

An interior target above its appended-bit boundary selects the successor code.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode_eq_lower_of_not_succ_lt (format : Format) (target : ℝ) (hpositive : 0 < target) (hminimum : minPositive format ≤ target) (hupper : ¬lowerCode format target + 1 < format.signMaskNat) : roundPositiveCode format target = lowerCode format target

A saturated interior lower code is already the final rounded code.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode_mono (format : Format) : Monotone (roundPositiveCode format)

Exact real-valued positive rounding is monotone.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositiveCode_ratCast (format : Format) (target : ℚ) : roundPositiveCode format ↑target = Model.roundPositiveCode format target

Real rounding agrees with rational rounding after exact coercion.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.roundPositive_ratCast (format : Format) (target : ℚ) : roundPositive format ↑target = roundPositiveRat format target

Model-valued real rounding agrees with rational rounding after exact coercion.

theorem FloatLib.Floats.Formats.Posit.Model.RealRounding.round_ratCast (format : Format) (target : ℚ) : round format ↑target = roundRat format target

Signed real rounding extends the executable exact-rational specification.