Rounding from a Certified Bracket

The effective calculation layer identifies a unit interval [m, m + 1) and a location inside it. This file turns that finite location data into the integer selected by directed or nearest rounding and proves agreement with the rounded-real definitions.

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.InbetweenInt (m : ℤ) (x : ℝ) (location : Location) : Prop

Unit-interval specialization of Inbetween.

noncomputable def FloatLib.Floats.Formats.Flocq.integerLocation (x : ℝ) : Location

Canonical location obtained from the floor bracket of a real value.

theorem FloatLib.Floats.Formats.Flocq.integerLocation_spec (x : ℝ) : InbetweenInt ⌊x⌋ x (integerLocation x)

Every real value satisfies its canonical floor bracket.

def FloatLib.Floats.Formats.Flocq.conditionalIncrement (increment : Bool) (m : ℤ) : ℤ

Increment an integer when the supplied decision is true.

theorem FloatLib.Floats.Formats.Flocq.conditionalIncrement_bounds (increment : Bool) (m : ℤ) : m ≤ conditionalIncrement increment m ∧ conditionalIncrement increment m ≤ m + 1

A conditional increment always selects one of the two bracket endpoints.

def FloatLib.Floats.Formats.Flocq.roundUpLocation : Location → Bool

Upward rounding increments exactly when the location is inexact.

def FloatLib.Floats.Formats.Flocq.roundNearestLocation (chooseUp : ℤ → Bool) (m : ℤ) : Location → Bool

Nearest rounding increments above the midpoint and delegates exact ties to chooseUp.

def FloatLib.Floats.Formats.Flocq.nearestEvenChoice (m : ℤ) : Bool

Tie decision used by nearest-even rounding: increment exactly when the lower integer is odd.

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_even_eq (x : ℝ) : nearestChoice nearestEvenChoice x = nearestEven x

Choice-based nearest rounding with the parity decision is FloatLib's nearest-even mode.

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_floor {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : floorRound x = m

A certified unit bracket determines floor exactly.

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_ceil {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : ceilRound x = conditionalIncrement (roundUpLocation location) m

A certified unit bracket determines ceiling from exactness alone.

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_nearestChoice (chooseUp : ℤ → Bool) {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : nearestChoice chooseUp x = conditionalIncrement (roundNearestLocation chooseUp m location) m

A certified unit bracket computes arbitrary-tie nearest rounding.

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_nearestEven {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : nearestEven x = conditionalIncrement (roundNearestLocation nearestEvenChoice m location) m

A certified unit bracket computes nearest-even rounding.

Mantissa truncation

structure FloatLib.Floats.Formats.Flocq.TruncationState : Type

Mantissa, exponent, and location carried by an effective rounding calculation.

• mantissa : ℤ

  Lower-endpoint mantissa.

• exponent : ℤ

  Shared radix exponent.

• location : Location

  Input location within the represented unit interval.

@[instance_reducible]

instance FloatLib.Floats.Formats.Flocq.instDecidableEqTruncationState : DecidableEq TruncationState

def FloatLib.Floats.Formats.Flocq.instDecidableEqTruncationState.decEq (x✝ x✝¹ : TruncationState) : Decidable (x✝ = x✝¹)

def FloatLib.Floats.Formats.Flocq.instReprTruncationState.repr : TruncationState → ℕ → Std.Format

@[instance_reducible]

instance FloatLib.Floats.Formats.Flocq.instReprTruncationState : Repr TruncationState

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.TruncationState.Brackets (β : Numerics.Radix) (state : TruncationState) (x : ℝ) : Prop

Real interval and location denoted by a truncation state.

theorem FloatLib.Floats.Formats.Flocq.TruncationState.mantissa_nonneg_of_brackets (β : Numerics.Radix) (state : TruncationState) {x : ℝ} (hx : 0 < x) (hl : Brackets β state x) : 0 ≤ state.mantissa

A positive value bracketed by a truncation state forces a nonnegative lower mantissa.

theorem FloatLib.Floats.Formats.Flocq.cexp_eq_fexp_digits_of_brackets {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (state : TruncationState) {x : ℝ} (hx : 0 < x) (hl : TruncationState.Brackets β state x) (hexp : state.exponent ≤ cexp β fexp x ∨ state.exponent ≤ fexp (↑(digits β state.mantissa) + state.exponent)) : cexp β fexp x = fexp (↑(digits β state.mantissa) + state.exponent)

For a positive input and a bracket with sufficient precision, the lower mantissa's digit count determines the canonical exponent. This is the representation-level counterpart of Flocq's cexp_inbetween_float.

theorem FloatLib.Floats.Formats.Flocq.TruncationState.scaledBrackets_of_exponent_eq {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (state : TruncationState) {x : ℝ} (hl : Brackets β state x) (hexponent : state.exponent = cexp β fexp x) : InbetweenInt state.mantissa (scaledMantissa β fexp x) state.location

A bracket stored at the canonical exponent is a unit bracket for the scaled mantissa.

def FloatLib.Floats.Formats.Flocq.truncateAux (β : Numerics.Radix) (state : TruncationState) (shift : ℤ) : TruncationState

Discard shift low radix digits and transfer their information into the refined location. Positive shifts are the intended use; correctness theorems state that premise explicitly.

theorem FloatLib.Floats.Formats.Flocq.intPower_one_lt (β : Numerics.Radix) {shift : ℤ} (hshift : 0 < shift) : 1 < intPower β shift

A positive shift produces a radix power strictly larger than one.

theorem FloatLib.Floats.Formats.Flocq.truncateAux_remainder_bounds (β : Numerics.Radix) (state : TruncationState) {shift : ℤ} (hshift : 0 < shift) : have power := intPower β shift; 0 ≤ state.mantissa % power ∧ state.mantissa % power < power

The truncated remainder is a valid cell index in the discarded radix block.

theorem FloatLib.Floats.Formats.Flocq.truncateAux_mantissa_decomposition (β : Numerics.Radix) (state : TruncationState) {shift : ℤ} (hshift : 0 < shift) : state.mantissa = state.mantissa % intPower β shift + intPower β shift * (truncateAux β state shift).mantissa

Mantissa reconstruction after one truncation step.

theorem FloatLib.Floats.Formats.Flocq.truncateAux_brackets (β : Numerics.Radix) (state : TruncationState) {shift : ℤ} (hshift : 0 < shift) {x : ℝ} (hl : TruncationState.Brackets β state x) : TruncationState.Brackets β (truncateAux β state shift) x

After a positive truncation step, the enlarged bracket still contains the input.

def FloatLib.Floats.Formats.Flocq.truncationShift (β : Numerics.Radix) (fexp : ℤ → ℤ) (state : TruncationState) : ℤ

Number of low radix digits discarded to reach the exponent selected by fexp.

def FloatLib.Floats.Formats.Flocq.truncate (β : Numerics.Radix) (fexp : ℤ → ℤ) (state : TruncationState) : TruncationState

Truncate only when the target exponent lies strictly above the stored exponent.

theorem FloatLib.Floats.Formats.Flocq.truncate_brackets (β : Numerics.Radix) (fexp : ℤ → ℤ) (state : TruncationState) {x : ℝ} (hl : TruncationState.Brackets β state x) : TruncationState.Brackets β (truncate β fexp state) x

Format-driven truncation preserves the bracketing relation for the input.

theorem FloatLib.Floats.Formats.Flocq.truncate_brackets_and_exponent {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (state : TruncationState) {x : ℝ} (hx : 0 < x) (hl : TruncationState.Brackets β state x) (hexp : state.exponent ≤ cexp β fexp x ∨ state.exponent ≤ fexp (↑(digits β state.mantissa) + state.exponent)) : TruncationState.Brackets β (truncate β fexp state) x ∧ (truncate β fexp state).exponent = cexp β fexp x

For a positive input with sufficient initial precision, truncation both preserves the bracket and selects the canonical format exponent.

def FloatLib.Floats.Formats.Flocq.roundTruncatedNearestEven (β : Numerics.Radix) (fexp : ℤ → ℤ) (state : TruncationState) : FloatRep β

Nearest-even result selected from a format-truncated bracket.

@[simp]

theorem FloatLib.Floats.Formats.Flocq.truncate_zero_mantissa (β : Numerics.Radix) (fexp : ℤ → ℤ) (exponent : ℤ) (location : Location) : (truncate β fexp { mantissa := 0, exponent := exponent, location := location }).mantissa = 0

Truncation never changes a zero mantissa into a nonzero one.

noncomputable def FloatLib.Floats.Formats.Flocq.roundedFloat {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) : FloatRep β

Rounded mantissa paired with the input's canonical exponent.

theorem FloatLib.Floats.Formats.Flocq.round_eq_toReal_of_scaled_round_eq {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) (mantissa : ℤ) (hmantissa : rnd (scaledMantissa β fexp x) = mantissa) : round rnd x = toReal { mantissa := mantissa, exponent := cexp β fexp x }

A rounded scaled mantissa and the input's canonical exponent represent the rounded real value.

theorem FloatLib.Floats.Formats.Flocq.round_floor_of_scaledBracket {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) {m : ℤ} {location : Location} (hl : InbetweenInt m (scaledMantissa β fexp x) location) : round floorRound x = toReal { mantissa := m, exponent := cexp β fexp x }

A scaled-mantissa bracket computes format-level downward rounding.

theorem FloatLib.Floats.Formats.Flocq.round_ceil_of_scaledBracket {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) {m : ℤ} {location : Location} (hl : InbetweenInt m (scaledMantissa β fexp x) location) : round ceilRound x = toReal { mantissa := conditionalIncrement (roundUpLocation location) m, exponent := cexp β fexp x }

A scaled-mantissa bracket computes format-level upward rounding.

theorem FloatLib.Floats.Formats.Flocq.round_nearestEven_of_scaledBracket {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) {m : ℤ} {location : Location} (hl : InbetweenInt m (scaledMantissa β fexp x) location) : round nearestEven x = toReal { mantissa := conditionalIncrement (roundNearestLocation nearestEvenChoice m location) m, exponent := cexp β fexp x }

A scaled-mantissa bracket computes format-level nearest-even rounding.

noncomputable def FloatLib.Floats.Formats.Flocq.nearestEvenMantissa (x : ℝ) : ℤ

Nearest-even integer selected from the real input's floor bracket.

theorem FloatLib.Floats.Formats.Flocq.round_nearestEven_computed {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (x : ℝ) : round nearestEven x = toReal { mantissa := nearestEvenMantissa (scaledMantissa β fexp x), exponent := cexp β fexp x }

Nearest-even format rounding agrees with selection from the scaled input's floor bracket.

theorem FloatLib.Floats.Formats.Flocq.roundTruncatedNearestEven_correct {β : Numerics.Radix} {fexp : ℤ → ℤ} [ValidExp fexp] (state : TruncationState) {x : ℝ} (hx : 0 < x) (hl : TruncationState.Brackets β state x) (hexp : state.exponent ≤ cexp β fexp x ∨ state.exponent ≤ fexp (↑(digits β state.mantissa) + state.exponent)) : toReal (roundTruncatedNearestEven β fexp state) = round nearestEven x

Nearest-even selection after canonical truncation agrees with generic rounded-real semantics.