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. Every named rounding mode is covered: floor, ceiling, truncation, rounding away from zero, and nearest rounding with any tie choice.

Nearest rounding with ties away from zero differs from every other nearest rounding only at an exact midpoint, where it agrees with awayRound.

Source counterparts are in Flocq 4.2.2, src/Calc/Round.v: inbetween_int_NE for nearest-even selection, truncate_correct for the canonical bracket after truncation, and round_trunc_NE_correct for agreement with real-valued rounding. Release source: https://flocq.gitlabpages.inria.fr/releases/flocq-4.2.2.tar.gz.

@[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.nearestChoice_eq_of_fract_ne_half (chooseUp chooseUp' : ℤ → Bool) {x : ℝ} (hx : Int.fract x ≠ 1 / 2) : nearestChoice chooseUp x = nearestChoice chooseUp' x

Away from a midpoint, nearest rounding does not depend on the tie choice.

theorem FloatLib.Floats.Formats.Flocq.nearestChoice_tieAway_eq_awayRound_of_fract_eq_half {x : ℝ} (hx : Int.fract x = 1 / 2) : nearestChoice nearestAwayChoice x = awayRound x

At a midpoint, nearest rounding with ties away from zero is rounding away from zero.

theorem FloatLib.Floats.Formats.Flocq.negRound_nearestChoice (chooseUp : ℤ → Bool) : negRound (nearestChoice chooseUp) = nearestChoice fun (f : ℤ) => !chooseUp (-f - 1)

Conjugating nearest rounding by negation mirrors its tie choice.

theorem FloatLib.Floats.Formats.Flocq.negRound_nearestChoice_tieAway : negRound (nearestChoice nearestAwayChoice) = nearestChoice nearestAwayChoice

Nearest rounding with ties away from zero commutes with negation.

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

A certified unit bracket determines the floor.

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.

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_bounds {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : ↑m ≤ x ∧ x < ↑m + 1

A certified unit bracket places its input in [m, m + 1).

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_trunc {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : truncRound x = if m < 0 then conditionalIncrement (roundUpLocation location) m else m

A certified unit bracket computes toward-zero rounding: floor when the lower integer is nonnegative and ceiling when it is negative.

theorem FloatLib.Floats.Formats.Flocq.inbetweenInt_away {m : ℤ} {x : ℝ} {location : Location} (hl : InbetweenInt m x location) : awayRound x = if m < 0 then m else conditionalIncrement (roundUpLocation location) m

A certified unit bracket computes rounding away from zero: ceiling when the lower integer is nonnegative and floor when it is negative.

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, and the correctness theorems assume 0 < shift.

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.

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

A scaled-mantissa bracket computes format-level nearest rounding with any tie choice.

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

A scaled-mantissa bracket computes format-level rounding toward zero.

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

A scaled-mantissa bracket computes format-level rounding away from zero.

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. The input must be positive, and hexp requires sufficient precision in the initial bracket. truncate_brackets alone does not establish the canonical-exponent condition.