LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

A left-to-right Leibniz determinant has an explicit forward error bound

Statement

Let $M$ be an $s \times s$ matrix, $s \geq 2$ , whose entries are exactly represented in a selected floating-point system. Compute its Leibniz determinant by forming each product left-to-right, applying each permutation sign by an exact sign-bit change, and summing the $s!$ signed terms left-to-right. If every rounded operation is zero or has a normal-range exact result, every operation satisfies the standard relative model with unit roundoff $u$ , and $q u < 1$ for $q = s + s! - 2$ , then $∣ \hat{D} - \det M ∣ \leq γ_{q} S, γ_{q} = \frac{q u}{1 - q u}, S = \sum_{π \in S_{s}} \prod_{i = 0}^{s - 1} ∣ M_{i, π (i)} ∣ .$

Facts & Assumptions

Given: For the real entries of $M$ , write $\det M = \sum_{π \in S_{s}} sgn (π) \prod_{i = 0}^{s - 1} M_{i, π (i)}$ , using the permutation and sign conventions of Dyadic orientation and lifted sphere determinants. This finite polynomial defines the determinant for arbitrary real entries and agrees with that item's definition on dyadic matrices; representability here does not require dyadic entries. Use the operationwise model in The standard relative floating-point model and unit roundoff, lexicographic permutation order, left-to-right products and summation, and an exact sign change after each product when its permutation is odd. Set $γ_{0} = 0$ .

[F1]

The standard relative floating-point model and unit roundoff: for each addition or multiplication whose exact result is zero or normal-range, $fl (x \circ y) = (x \circ y) (1 + δ)$ with $∣ δ ∣ \leq u$ .

[F2]

Basic properties of the absolute value and The triangle inequality: $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ , $- ∣ x ∣ \leq x \leq ∣ x ∣$ , and $∣ x + y ∣ \leq ∣ x ∣ + ∣ y ∣$ .

[A1]

Every rounded operation in this computation has exact result zero or in the normal range; no overflow, underflow, or invalid operation occurs; $q u < 1$ ; and each permutation sign is applied by an exact sign-bit change after its product, with no rounded arithmetic operation.

Proof

1.1givenF1algebra

For an integer $n \geq 0$ with $n u < 1$ , the binomial theorem and $(\binom{n}{k}) \leq n^{k}$ give $(1 + u)^{n} \leq \sum_{k \geq 0} (n u)^{k} = 1 / (1 - n u)$ . Therefore $(1 + u)^{n} - 1 \leq γ_{n}$ .

2.1givenF1F2A1step 1.1algebra

Put $a = s - 1$ and let $t_{π}$ be one exact signed Leibniz product. Its $a$ rounded multiplications introduce factors $(1 + δ_{k})$ by [F1] and [A1]. The identity $\prod_{k} (1 + δ_{k}) - 1 = \sum_{k} δ_{k} \prod_{j < k} (1 + δ_{j})$ , the triangle inequality [F2], and $∣ 1 + δ_{j} ∣ \leq 1 + u$ show $∣ {\hat{t}}_{π} - t_{π} ∣ \leq ((1 + u)^{a} - 1) ∣ t_{π} ∣ \leq γ_{a} ∣ t_{π} ∣$ by [step 1.1]. The same product bound gives $∣ {\hat{t}}_{π} ∣ \leq (1 + γ_{a}) ∣ t_{π} ∣$ ; an exact zero term remains zero.

3.1givenF1F2A1step 1.1step 2.1inductionalgebra

There are $s!$ terms and hence $b = s! - 1$ rounded additions after the first term is placed in the accumulator. If the successive addition errors are $η_{1}, \dots, η_{b}$ , induction in the accumulator recurrence writes $\hat{D} = \sum_{j = 1}^{s!} {\hat{t}}_{j} P_{j}$ , where each $P_{j}$ is a product of at most $b$ factors $(1 + η_{k})$ . The telescoping identity in [step 2.1] gives $∣ P_{j} - 1 ∣ \leq γ_{b}$ . Thus $∣ \hat{D} - \sum_{j} {\hat{t}}_{j} ∣ = ∣ \sum_{j} {\hat{t}}_{j} (P_{j} - 1) ∣$ is at most $γ_{b} \sum_{j} ∣ {\hat{t}}_{j} ∣$ by [F2].

4.1givenF2step 2.1step 3.1algebra

Apply [F2], [step 2.1], and [step 3.1] to the exact signed sum. With $S = \sum_{π} ∣ t_{π} ∣$ this gives $∣ \hat{D} - \det M ∣ \leq (γ_{a} + γ_{b} + γ_{a} γ_{b}) S$ .

5.1givenA1step 4.1algebra∎

Since $q = a + b$ and $q u < 1$ , $(1 - a u) (1 - b u) = 1 - q u + a b u^{2} \geq 1 - q u > 0$ . Therefore $(1 + γ_{a}) (1 + γ_{b}) - 1 \leq γ_{q}$ , so the coefficient in [step 4.1] is at most $γ_{q}$ . This proves the stated bound.

Depends on

Used by

Dependency tree · two levels

12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jonathan R. Shewchuk, Adaptive Precision Floating-Point Arithmetic and Fast Robust Geometric Predicates, §§4.2–4.4 (standard reference, not scraped)
Mark de Berg et al., Computational Geometry: Algorithms and Applications, 2nd ed., §1.2 (standard reference, not scraped)