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; Internal proves that the accumulator preserves them. The final theorems connect these invariants to sumWithStatus and dotWithStatus.

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; 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 explicit 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 exactly.

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 exactly 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 exactly 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 exactly 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 precisely 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 deliberately remains traversal-order dependent.

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.

This keeps callers in the rational specification and hides 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; equal array lengths rule out the error branch.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sumWithStatus_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) : sumWithStatus destination values mode = { value := roundDyadicWithRounding destination mode (Array.foldl Internal.State.pushValue { } values).exact, status := dyadicRoundingStatus destination mode (Array.foldl Internal.State.pushValue { } values).exact (roundDyadicWithRounding destination mode (Array.foldl Internal.State.pushValue { } values).exact) }

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sumWithStatus_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 : (sumWithStatus destination values IEEERoundingMode.nearestEven).value.isFinite = true) : (sumWithStatus destination values IEEERoundingMode.nearestEven).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.sumWithStatus_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) : sumWithStatus destination values mode = { 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.towardNegativeInfinity)), status := IEEEStatus.clear }

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.sumWithStatus_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) : sumWithStatus destination values mode = { value := zero destination negative, status := IEEEStatus.clear }

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.sumWithStatus_singleton_eq_castWithStatus_of_isInf (destination : FloatFormat) {source : FloatFormat} (value : Model source) (mode : IEEERoundingMode) (hinf : value.isInf = true) : sumWithStatus destination #[value] mode = castWithStatus source destination value mode

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dotWithStatus_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) : dotWithStatus destination left right mode = Except.ok { value := roundDyadicWithRounding destination mode (Internal.dotState left right hsize).exact, status := dyadicRoundingStatus destination mode (Internal.dotState left right hsize).exact (roundDyadicWithRounding destination mode (Internal.dotState left right hsize).exact) }

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dotWithStatus_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 : dotWithStatus destination left right IEEERoundingMode.nearestEven = 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.dotWithStatus_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) : dotWithStatus destination left right mode = 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.towardNegativeInfinity)), status := IEEEStatus.clear }

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

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.sumWithStatus_empty (destination source : FloatFormat) (mode : IEEERoundingMode) : sumWithStatus destination #[] mode = { value := zero destination false, status := IEEEStatus.clear }

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

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.Reduction.dotWithStatus_lengthMismatch (destination : FloatFormat) {leftFormat rightFormat : FloatFormat} (left : Array (Model leftFormat)) (right : Array (Model rightFormat)) (mode : IEEERoundingMode) (hsize : left.size ≠ right.size) : dotWithStatus destination left right mode = 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.dotWithStatus_empty (destination leftFormat rightFormat : FloatFormat) (mode : IEEERoundingMode) : dotWithStatus destination #[] #[] mode = Except.ok { value := zero destination false, status := IEEEStatus.clear }

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