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 TorchLean.Floats.NeuralInbetweenInt (m : ℤ) (x : ℝ) (location : NeuralLocation) : Prop

Unit-interval specialization of NeuralInbetween.

noncomputable def TorchLean.Floats.neuralIntegerLocation (x : ℝ) : NeuralLocation

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

theorem TorchLean.Floats.neuralIntegerLocation_spec (x : ℝ) : NeuralInbetweenInt ⌊x⌋ x (neuralIntegerLocation x)

Every real value satisfies its canonical floor bracket.

def TorchLean.Floats.neuralConditionalIncrement (increment : Bool) (m : ℤ) : ℤ

Increment an integer when the supplied decision is true.

theorem TorchLean.Floats.neuralConditionalIncrement_bounds (increment : Bool) (m : ℤ) : m ≤ neuralConditionalIncrement increment m ∧ neuralConditionalIncrement increment m ≤ m + 1

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

def TorchLean.Floats.neuralRoundUpLocation : NeuralLocation → Bool

Upward rounding increments exactly when the location is inexact.

def TorchLean.Floats.neuralRoundNearestLocation (chooseUp : ℤ → Bool) (m : ℤ) : NeuralLocation → Bool

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

def TorchLean.Floats.neuralNearestEvenChoice (m : ℤ) : Bool

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

theorem TorchLean.Floats.neuralNearestChoice_even_eq (x : ℝ) : neuralNearestChoice neuralNearestEvenChoice x = neuralNearestEven x

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

theorem TorchLean.Floats.neuralInbetweenInt_floor {m : ℤ} {x : ℝ} {location : NeuralLocation} (hl : NeuralInbetweenInt m x location) : neuralFloorRound x = m

A certified unit bracket determines floor exactly.

theorem TorchLean.Floats.neuralInbetweenInt_ceil {m : ℤ} {x : ℝ} {location : NeuralLocation} (hl : NeuralInbetweenInt m x location) : neuralCeilRound x = neuralConditionalIncrement (neuralRoundUpLocation location) m

A certified unit bracket determines ceiling from exactness alone.

theorem TorchLean.Floats.neuralInbetweenInt_nearestChoice (chooseUp : ℤ → Bool) {m : ℤ} {x : ℝ} {location : NeuralLocation} (hl : NeuralInbetweenInt m x location) : neuralNearestChoice chooseUp x = neuralConditionalIncrement (neuralRoundNearestLocation chooseUp m location) m

A certified unit bracket computes arbitrary-tie nearest rounding.

theorem TorchLean.Floats.neuralInbetweenInt_nearestEven {m : ℤ} {x : ℝ} {location : NeuralLocation} (hl : NeuralInbetweenInt m x location) : neuralNearestEven x = neuralConditionalIncrement (neuralRoundNearestLocation neuralNearestEvenChoice m location) m

A certified unit bracket computes nearest-even rounding.

Mantissa truncation

structure TorchLean.Floats.NeuralTruncationState : Type

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

• mantissa : ℤ

  Lower-endpoint mantissa.

• exponent : ℤ

  Shared radix exponent.

• location : NeuralLocation

  Input location within the represented unit interval.

@[implicit_reducible]

instance TorchLean.Floats.instDecidableEqNeuralTruncationState : DecidableEq NeuralTruncationState

def TorchLean.Floats.instDecidableEqNeuralTruncationState.decEq (x✝ x✝¹ : NeuralTruncationState) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance TorchLean.Floats.instReprNeuralTruncationState : Repr NeuralTruncationState

def TorchLean.Floats.instReprNeuralTruncationState.repr : NeuralTruncationState → ℕ → Std.Format

@[reducible, inline]

abbrev TorchLean.Floats.NeuralTruncationState.Brackets (β : NeuralRadix) (state : NeuralTruncationState) (x : ℝ) : Prop

Real interval and location denoted by a truncation state.

theorem TorchLean.Floats.NeuralTruncationState.mantissa_nonneg_of_brackets (β : NeuralRadix) (state : NeuralTruncationState) {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 TorchLean.Floats.neuralCexp_eq_fexp_digits_of_brackets {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (state : NeuralTruncationState) {x : ℝ} (hx : 0 < x) (hl : NeuralTruncationState.Brackets β state x) (hexp : state.exponent ≤ neuralCexp β fexp x ∨ state.exponent ≤ fexp (↑(neuralDigits β state.mantissa) + state.exponent)) : neuralCexp β fexp x = fexp (↑(neuralDigits β state.mantissa) + state.exponent)

A positive bracket determines the canonical exponent from the lower mantissa's digit count. This is the representation-level counterpart of Flocq's cexp_inbetween_float.

theorem TorchLean.Floats.NeuralTruncationState.scaledBrackets_of_exponent_eq {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (state : NeuralTruncationState) {x : ℝ} (hl : Brackets β state x) (hexponent : state.exponent = neuralCexp β fexp x) : NeuralInbetweenInt state.mantissa (neuralScaledMantissa β fexp x) state.location

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

noncomputable def TorchLean.Floats.neuralTruncateAux (β : NeuralRadix) (state : NeuralTruncationState) (shift : ℤ) : NeuralTruncationState

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 TorchLean.Floats.neuralIntPower_one_lt (β : NeuralRadix) {shift : ℤ} (hshift : 0 < shift) : 1 < neuralIntPower β shift

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

theorem TorchLean.Floats.neuralTruncateAux_remainder_bounds (β : NeuralRadix) (state : NeuralTruncationState) {shift : ℤ} (hshift : 0 < shift) : have power := neuralIntPower β shift; 0 ≤ state.mantissa % power ∧ state.mantissa % power < power

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

theorem TorchLean.Floats.neuralTruncateAux_mantissa_decomposition (β : NeuralRadix) (state : NeuralTruncationState) {shift : ℤ} (hshift : 0 < shift) : state.mantissa = state.mantissa % neuralIntPower β shift + neuralIntPower β shift * (neuralTruncateAux β state shift).mantissa

Mantissa reconstruction after one truncation step.

theorem TorchLean.Floats.neuralTruncateAux_brackets (β : NeuralRadix) (state : NeuralTruncationState) {shift : ℤ} (hshift : 0 < shift) {x : ℝ} (hl : NeuralTruncationState.Brackets β state x) : NeuralTruncationState.Brackets β (neuralTruncateAux β state shift) x

One positive truncation step preserves the represented real bracket and its refined location.

def TorchLean.Floats.neuralTruncationShift (β : NeuralRadix) (fexp : ℤ → ℤ) (state : NeuralTruncationState) : ℤ

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

noncomputable def TorchLean.Floats.neuralTruncate (β : NeuralRadix) (fexp : ℤ → ℤ) (state : NeuralTruncationState) : NeuralTruncationState

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

theorem TorchLean.Floats.neuralTruncate_brackets (β : NeuralRadix) (fexp : ℤ → ℤ) (state : NeuralTruncationState) {x : ℝ} (hl : NeuralTruncationState.Brackets β state x) : NeuralTruncationState.Brackets β (neuralTruncate β fexp state) x

Format-driven truncation preserves the represented real bracket.

theorem TorchLean.Floats.neuralTruncate_brackets_and_exponent {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (state : NeuralTruncationState) {x : ℝ} (hx : 0 < x) (hl : NeuralTruncationState.Brackets β state x) (hexp : state.exponent ≤ neuralCexp β fexp x ∨ state.exponent ≤ fexp (↑(neuralDigits β state.mantissa) + state.exponent)) : NeuralTruncationState.Brackets β (neuralTruncate β fexp state) x ∧ (neuralTruncate β fexp state).exponent = neuralCexp β fexp x

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

noncomputable def TorchLean.Floats.neuralRoundTruncatedNearestEven (β : NeuralRadix) (fexp : ℤ → ℤ) (state : NeuralTruncationState) : NeuralFloat β

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

@[simp]

theorem TorchLean.Floats.neuralTruncate_zero_mantissa (β : NeuralRadix) (fexp : ℤ → ℤ) (exponent : ℤ) (location : NeuralLocation) : (neuralTruncate β fexp { mantissa := 0, exponent := exponent, location := location }).mantissa = 0

Truncation never changes a zero mantissa into a nonzero one.

noncomputable def TorchLean.Floats.neuralRoundedFloat {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) : NeuralFloat β

Canonical mantissa/exponent representation produced by a rounding mode.

theorem TorchLean.Floats.neuralRound_eq_toReal_of_scaled_round_eq {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (rnd : ℝ → ℤ) (x : ℝ) (mantissa : ℤ) (hmantissa : rnd (neuralScaledMantissa β fexp x) = mantissa) : neuralRound rnd x = neuralToReal { mantissa := mantissa, exponent := neuralCexp β fexp x }

If a finite decision procedure computes the rounded scaled mantissa, neuralRound is exactly the real value of the corresponding mantissa/exponent pair.

theorem TorchLean.Floats.neuralRound_floor_of_scaledBracket {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) {m : ℤ} {location : NeuralLocation} (hl : NeuralInbetweenInt m (neuralScaledMantissa β fexp x) location) : neuralRound neuralFloorRound x = neuralToReal { mantissa := m, exponent := neuralCexp β fexp x }

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

theorem TorchLean.Floats.neuralRound_ceil_of_scaledBracket {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) {m : ℤ} {location : NeuralLocation} (hl : NeuralInbetweenInt m (neuralScaledMantissa β fexp x) location) : neuralRound neuralCeilRound x = neuralToReal { mantissa := neuralConditionalIncrement (neuralRoundUpLocation location) m, exponent := neuralCexp β fexp x }

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

theorem TorchLean.Floats.neuralRound_nearestEven_of_scaledBracket {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) {m : ℤ} {location : NeuralLocation} (hl : NeuralInbetweenInt m (neuralScaledMantissa β fexp x) location) : neuralRound neuralNearestEven x = neuralToReal { mantissa := neuralConditionalIncrement (neuralRoundNearestLocation neuralNearestEvenChoice m location) m, exponent := neuralCexp β fexp x }

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

noncomputable def TorchLean.Floats.neuralNearestEvenMantissa (x : ℝ) : ℤ

Canonical mantissa selected by effective nearest-even rounding.

theorem TorchLean.Floats.neuralRound_nearestEven_computed {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (x : ℝ) : neuralRound neuralNearestEven x = neuralToReal { mantissa := neuralNearestEvenMantissa (neuralScaledMantissa β fexp x), exponent := neuralCexp β fexp x }

Every nearest-even format rounding has a canonical computed mantissa/exponent representation.

theorem TorchLean.Floats.neuralRoundTruncatedNearestEven_correct {β : NeuralRadix} {fexp : ℤ → ℤ} [NeuralValidExp fexp] (state : NeuralTruncationState) {x : ℝ} (hx : 0 < x) (hl : NeuralTruncationState.Brackets β state x) (hexp : state.exponent ≤ neuralCexp β fexp x ∨ state.exponent ≤ fexp (↑(neuralDigits β state.mantissa) + state.exponent)) : neuralToReal (neuralRoundTruncatedNearestEven β fexp state) = neuralRound neuralNearestEven x

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