Correctness of sums and dot products

Finite operands accumulate exactly as dyadics and undergo one final rounding. Semantics defines the rational list and array-slice specifications, and Internal proves that the accumulator preserves them. The final theorems connect these invariants to sum and dot.

The zero-result theorems preserve the signed-zero rules. The real-valued rounding theorems require a finite output, since overflow to infinity has no real denotation. Permutation invariance applies to the finite accumulator, while NaN selection can depend on traversal order.

Nonempty sums of same-sign zeros preserve that sign in every rounding mode. Generated invalid indicators survive later dot-product terms, including NaNs. Infinite singleton sums agree with casts, including the destination's conversion status.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteContribution {format : FloatFormat} (value : Model format) : ℚ

Exact rational contribution to the accumulator. Exceptional encodings contribute zero.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteSum {format : FloatFormat} (values : List (Model format)) : ℚ

Exact sum of the finite contributions.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteDot {leftFormat rightFormat : FloatFormat} (left : List (Model leftFormat)) (right : List (Model rightFormat)) : Except Numerics.ReductionError ℚ

Exact sum of pairwise products, with an error for unequal lengths.

@[irreducible]

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteDotSlice {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (index remaining : ℕ) (hleft : index + remaining ≤ left.size) (hright : index + remaining ≤ right.size) : ℚ

Exact dot product of remaining pairs from index, with bounds for both arrays.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteDotSlice_eq_zipWith_sum {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (index remaining : ℕ) (hleft : index + remaining ≤ left.size) (hright : index + remaining ≤ right.size) : finiteDotSlice left right index remaining hleft hright = (List.zipWith (fun (x : Model leftFormat) (y : Model rightFormat) => finiteContribution x * finiteContribution y) (List.take remaining (List.drop index left.toList)) (List.take remaining (List.drop index right.toList))).sum

The bounded Array specification is the corresponding list dot product over the same slice.

This bridge lets the kernel traverse indexed arrays while public theorems use ordinary list operations. The bounds ensure that drop and take select exactly remaining pairs.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteDot_toList_eq_slice {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (hsize : left.size = right.size) : finiteDot left.toList right.toList = Except.ok (finiteDotSlice left right 0 left.size ⋯ ⋯)

On equal-sized arrays, the list and bounded-Array dot specifications agree.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteSum_eq_of_perm {format : FloatFormat} {left right : List (Model format)} (hperm : left.Perm right) : finiteSum left = finiteSum right

The finite-sum specification is independent of traversal order.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Semantics.finiteDot_singleton {leftFormat rightFormat : FloatFormat} (left : Model leftFormat) (right : Model rightFormat) : finiteDot [left] [right] = Except.ok (finiteContribution left * finiteContribution right)

A one-pair finite dot product is the product of the two contributions.

def FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.HasOnlyFiniteTerms {destination : FloatFormat} (state : State destination) : Prop

Finite-only accumulator states contain no exceptional value or generated invalid operation.

The finite sum proofs use this predicate to discharge every exceptional branch in State.finish at once.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.hasOnlyFiniteTerms_empty (destination : FloatFormat) : { }.HasOnlyFiniteTerms

The empty reduction state contains only finite terms.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.HasOnlyFiniteTerms.pushExact {destination : FloatFormat} {state : State destination} (hstate : state.HasOnlyFiniteTerms) (value : Numerics.Dyadic) : (state.pushExact value).HasOnlyFiniteTerms

Adding an exact dyadic preserves the finite-only state invariant.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushValue_eq_pushExact {destination source : FloatFormat} (state : State destination) (value : Model source) (hfinite : value.isFinite = true) : state.pushValue value = state.pushExact (value.finiteDyadic hfinite)

A finite encoded value takes the pushExact branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.HasOnlyFiniteTerms.pushValue {destination source : FloatFormat} {state : State destination} (hstate : state.HasOnlyFiniteTerms) (value : Model source) (hfinite : value.isFinite = true) : (state.pushValue value).HasOnlyFiniteTerms

Consuming a finite encoded value preserves the finite-only state invariant.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushProduct_eq_pushExact {destination leftFormat rightFormat : FloatFormat} (state : State destination) (left : Model leftFormat) (right : Model rightFormat) (hleft : left.isFinite = true) (hright : right.isFinite = true) : state.pushProduct left right = state.pushExact ((left.finiteDyadic hleft).mul (right.finiteDyadic hright))

A finite pair takes the exact-product branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.HasOnlyFiniteTerms.pushProduct {destination leftFormat rightFormat : FloatFormat} {state : State destination} (hstate : state.HasOnlyFiniteTerms) (left : Model leftFormat) (right : Model rightFormat) (hleft : left.isFinite = true) (hright : right.isFinite = true) : (state.pushProduct left right).HasOnlyFiniteTerms

Consuming two finite factors preserves the finite-only state invariant.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.foldl_pushValue_hasOnlyFiniteTerms {destination source : FloatFormat} (state : State destination) (values : List (Model source)) (hstate : state.HasOnlyFiniteTerms) (hfinite : ∀ value ∈ values, value.isFinite = true) : (List.foldl State.pushValue state values).HasOnlyFiniteTerms

Folding a list of finite values preserves the finite-only state invariant.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.captureNaN_exact {destination source : FloatFormat} (state : State destination) (value : Model source) : (state.captureNaN value).exact = state.exact

Recording a NaN leaves the exact finite accumulator unchanged.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.captureNaN_generatedInvalid {destination source : FloatFormat} (state : State destination) (value : Model source) : (state.captureNaN value).generatedInvalid = state.generatedInvalid

Recording a NaN preserves an invalid operation generated by an earlier product.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushInfinity_exact {destination : FloatFormat} (state : State destination) (negative : Bool) : (state.pushInfinity negative).exact = state.exact

Recording an infinity leaves the exact finite accumulator unchanged.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushProduct_generatedInvalid {destination leftFormat rightFormat : FloatFormat} (state : State destination) (left : Model leftFormat) (right : Model rightFormat) (hinvalid : state.generatedInvalid = true) : (state.pushProduct left right).generatedInvalid = true

Every subsequent product preserves a previously generated invalid operation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.finish_invalid {destination : FloatFormat} (state : State destination) (mode : IEEERoundingMode) (hinvalid : (state.generatedInvalid || state.positiveInfinity && state.negativeInfinity) = true) : (state.finish mode).status.invalid = true

Generated invalid operations and opposing infinities raise invalid even in the NaN branches.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotStateLoop_generatedInvalid {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (state : State destination) (index remaining : ℕ) (hleft : index + remaining ≤ left.size) (hright : index + remaining ≤ right.size) (hinvalid : state.generatedInvalid = true) : (dotStateLoop left right state index remaining hleft hright).generatedInvalid = true

An arbitrary dot-product suffix cannot clear an invalid operation generated by its prefix.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushValue_exact_toRat {destination source : FloatFormat} (state : State destination) (value : Model source) : (state.pushValue value).exact.toRat = state.exact.toRat + Semantics.finiteContribution value

Consuming one value changes the exact field by its finite rational contribution.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.foldl_pushValue_exact_toRat {destination source : FloatFormat} (state : State destination) (values : List (Model source)) : (List.foldl State.pushValue state values).exact.toRat = state.exact.toRat + Semantics.finiteSum values

Folding values accumulates exactly the rational sum of their finite contributions.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.array_foldl_pushValue_exact_toRat {destination source : FloatFormat} (values : Array (Model source)) : (Array.foldl State.pushValue { } values).exact.toRat = Semantics.finiteSum values.toList

The Array summation kernel accumulates the exact rational finite sum.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.State.pushProduct_exact_toRat {destination leftFormat rightFormat : FloatFormat} (state : State destination) (left : Model leftFormat) (right : Model rightFormat) (hleft : left.isFinite = true) (hright : right.isFinite = true) : (state.pushProduct left right).exact.toRat = state.exact.toRat + Semantics.finiteContribution left * Semantics.finiteContribution right

Consuming one product adds exactly the product of its two finite rational contributions.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotStateLoop_exact_toRat {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (state : State destination) (index remaining : ℕ) (hleft : index + remaining ≤ left.size) (hright : index + remaining ≤ right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) : (dotStateLoop left right state index remaining hleft hright).exact.toRat = state.exact.toRat + Semantics.finiteDotSlice left right index remaining hleft hright

The indexed dot loop accumulates exactly the rational product sum of its Array slice.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotStateLoop_hasOnlyFiniteTerms {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (state : State destination) (index remaining : ℕ) (hleft : index + remaining ≤ left.size) (hright : index + remaining ≤ right.size) (hstate : state.HasOnlyFiniteTerms) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) : (dotStateLoop left right state index remaining hleft hright).HasOnlyFiniteTerms

Finite input pairs keep the indexed dot loop free of exceptional state.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotState_exact_toRat {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) : (dotState left right hsize).exact.toRat = Semantics.finiteDotSlice left right 0 left.size ⋯ ⋯

The complete finite dot kernel accumulates exactly its rational Array specification.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.Internal.dotState_hasOnlyFiniteTerms {destination leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) : (dotState left right hsize).HasOnlyFiniteTerms

The complete finite dot kernel cannot produce exceptional accumulator state.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sumAccumulator_toRat_eq_of_perm {destination source : FloatFormat} {left right : List (Model source)} (hperm : left.Perm right) : (List.foldl Internal.State.pushValue { } left).exact.toRat = (List.foldl Internal.State.pushValue { } right).exact.toRat

The executable sum accumulator has the same exact rational value after any permutation.

This theorem concerns the finite accumulator field, not the complete exceptional result. NaN selection depends on traversal order.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sumAccumulator_significand_ne_zero_of_finiteSum_ne_zero (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (hnonzero : Semantics.finiteSum values.toList ≠ 0) : (Array.foldl Internal.State.pushValue { } values).exact.significand ≠ 0

A mathematically nonzero finite sum gives a nonzero exact accumulator.

Callers can stay in the rational specification without seeing the dyadic accumulator's internal representation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dotAccumulator_significand_ne_zero_of_finiteDot_ne_zero (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) (hnonzero : Semantics.finiteDot left.toList right.toList ≠ Except.ok 0) : (Internal.dotState left right hsize).exact.significand ≠ 0

A mathematically nonzero finite dot product gives a nonzero exact accumulator.

The premise uses the public list specification, and equal array lengths rule out the error branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_eq_round_of_finite_nonzero (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode) (hfinite : ∀ value ∈ values.toList, value.isFinite = true) (hnonzero : Semantics.finiteSum values.toList ≠ 0) : sum destination values mode true = { value := Internal.Directed.roundDyadic destination mode (Array.foldl Internal.State.pushValue { } values).exact, status := dyadicRoundingStatus destination mode (Array.foldl Internal.State.pushValue { } values).exact (Internal.Directed.roundDyadic destination mode (Array.foldl Internal.State.pushValue { } values).exact), ternary := dyadicTernary (Array.foldl Internal.State.pushValue { } values).exact (Internal.Directed.roundDyadic destination mode (Array.foldl Internal.State.pushValue { } values).exact) }

A nonzero sum of finite inputs performs one final dyadic rounding and reports that rounding's status and ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_value_toReal_eq_roundAt_of_finite_nonzero (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (hfmt : destination.isIEEE = true) (hfinite : ∀ value ∈ values.toList, value.isFinite = true) (hnonzero : Semantics.finiteSum values.toList ≠ 0) (hresult : (sum destination values IEEERoundingMode.nearest true).value.isFinite = true) : (sum destination values IEEERoundingMode.nearest true).value.toReal = roundAt destination ↑(Semantics.finiteSum values.toList)

For finite inputs with a nonzero exact sum, the executable nearest-even reduction is the exact mathematical sum followed by one destination-format rounding.

The result-finiteness premise excludes overflow to infinity, whose encoding has no real denotation. Exact accumulation itself is established independently of this premise.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_eq_zero_of_finite (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode) (hfinite : ∀ value ∈ values.toList, value.isFinite = true) (hzero : (Array.foldl Internal.State.pushValue { } values).exact.significand = 0) : sum destination values mode true = { value := zero destination ((Array.foldl Internal.State.pushValue { } values).sawFiniteTerm && ((Array.foldl Internal.State.pushValue { } values).allTermsNegativeZero || !(Array.foldl Internal.State.pushValue { } values).allTermsPositiveZero && mode == IEEERoundingMode.down)), status := Numerics.IEEEStatus.clear, ternary := Ordering.eq }

A finite sum whose exact accumulator is zero returns the specified signed zero and raises no status indicator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_value_toReal_eq_roundAt_of_finite (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (hfmt : destination.isIEEE = true) (hfinite : ∀ value ∈ values.toList, value.isFinite = true) (hresult : (sum destination values IEEERoundingMode.nearest true).value.isFinite = true) : (sum destination values IEEERoundingMode.nearest true).value.toReal = roundAt destination ↑(Semantics.finiteSum values.toList)

Every finite-input nearest-even sum with a finite result is one real rounding of the exact sum. Zero totals include empty input, signed zeros, and cancellation. Their stored signs are specified by sum_status_eq_zero_of_finite and disappear only in the real-valued conclusion.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_eq_zero_of_same_sign_zeros (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode) (negative : Bool) (hnonempty : values ≠ #[]) (hzero : ∀ value ∈ values.toList, value.isZero = true) (hsign : ∀ value ∈ values.toList, value.signBit = negative) : sum destination values mode true = { value := zero destination negative, status := Numerics.IEEEStatus.clear, ternary := Ordering.eq }

A nonempty sum of zeros with one common sign preserves that sign in every rounding mode.

The destination's zero constructor accounts for formats without a negative zero. The hypotheses refer only to the input values, independently of the accumulator's signed-zero flags.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_singleton_eq_cast_status_of_isInf (destination : FloatFormat) {source : FloatFormat} (value : Model source) (mode : IEEERoundingMode) (hinf : value.isInf = true) : sum destination #[value] mode true = cast source destination value mode true

A singleton infinity has the value and exception indicators of a destination cast.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dot_status_eq_round_of_finite_nonzero (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) (hnonzero : Semantics.finiteDot left.toList right.toList ≠ Except.ok 0) : dot destination left right mode true = Except.ok { value := Internal.Directed.roundDyadic destination mode (Internal.dotState left right hsize).exact, status := dyadicRoundingStatus destination mode (Internal.dotState left right hsize).exact (Internal.Directed.roundDyadic destination mode (Internal.dotState left right hsize).exact), ternary := dyadicTernary (Internal.dotState left right hsize).exact (Internal.Directed.roundDyadic destination mode (Internal.dotState left right hsize).exact) }

A nonzero dot product of finite inputs performs one final dyadic rounding and reports that rounding's status and ternary value.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dot_status_value_toReal_eq_roundAt_of_finite_nonzero (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (exact : ℚ) (outcome : IEEEOutcome destination) (hfmt : destination.isIEEE = true) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) (hspec : Semantics.finiteDot left.toList right.toList = Except.ok exact) (hnonzero : exact ≠ 0) (houtcome : dot destination left right IEEERoundingMode.nearest true = Except.ok outcome) (hresult : outcome.value.isFinite = true) : outcome.value.toReal = roundAt destination ↑exact

For finite equal-sized inputs with a nonzero exact dot product, the executable nearest-even reduction is the mathematical list dot product followed by one destination-format rounding.

outcome names the successful result of the Except-valued API. Its finiteness premise excludes overflow to infinity, whose encoding has no real denotation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dot_status_eq_zero_of_finite (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) (hzero : (Internal.dotState left right hsize).exact.significand = 0) : dot destination left right mode true = Except.ok { value := zero destination ((Internal.dotState left right hsize).sawFiniteTerm && ((Internal.dotState left right hsize).allTermsNegativeZero || !(Internal.dotState left right hsize).allTermsPositiveZero && mode == IEEERoundingMode.down)), status := Numerics.IEEEStatus.clear, ternary := Ordering.eq }

A finite dot product whose exact accumulator is zero returns the specified signed zero and raises no status indicator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dot_status_value_toReal_eq_roundAt_of_finite (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (exact : ℚ) (outcome : IEEEOutcome destination) (hfmt : destination.isIEEE = true) (hsize : left.size = right.size) (hleftFinite : ∀ (position : ℕ) (hposition : position < left.size), left[position].isFinite = true) (hrightFinite : ∀ (position : ℕ) (hposition : position < right.size), right[position].isFinite = true) (hspec : Semantics.finiteDot left.toList right.toList = Except.ok exact) (houtcome : dot destination left right IEEERoundingMode.nearest true = Except.ok outcome) (hresult : outcome.value.isFinite = true) : outcome.value.toReal = roundAt destination ↑exact

Every successful finite-input nearest-even dot product with a finite result is one real rounding of the exact product sum, including cancellation to zero. It requires equal input lengths and excludes exceptional outputs.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sum_status_empty (destination source : FloatFormat) (mode : IEEERoundingMode) : sum destination #[] mode true = { value := zero destination false, status := Numerics.IEEEStatus.clear, ternary := Ordering.eq }

The empty correctly rounded sum is an exact positive zero with no exception indicator.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dot_status_lengthMismatch (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) (hsize : left.size ≠ right.size) : dot destination left right mode true = Except.error (Numerics.ReductionError.lengthMismatch left.size right.size)

A mismatched dot product reports both observed lengths and performs no reduction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dot_status_empty (destination leftFormat rightFormat : FloatFormat) (mode : IEEERoundingMode) : dot destination #[] #[] mode true = Except.ok { value := zero destination false, status := Numerics.IEEEStatus.clear, ternary := Ordering.eq }

The empty correctly rounded dot product is an exact positive zero with no exception indicator.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.value_sum (destination : FloatFormat) {source : FloatFormat} (values : Array (Model source)) (mode : IEEERoundingMode) : (sum destination values mode true).value = sum destination values mode

The sum with status := true delivers the value of the sum in the same direction.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.map_value_dot (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) : Except.map IEEEOutcome.value (dot destination left right mode true) = dot destination left right mode

The dot product with status := true has the value and the length check of the dot product in the same direction.