LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

The integer-clearance determinant-sign algorithm is correct and terminates

Statement

For every finite encoded $s \times s$ matrix $M$ of exact dyadic rationals, $s \geq 1$ , Exact dyadic determinant sign by integer clearance terminates and returns $sgn (\det M)$ , including zero. No axiom of choice is required.

Facts & Assumptions

Given: A positive integer $s$ and a finite encoding of the dyadic entries of $M$ ; arbitrary-precision integer arithmetic means exact arithmetic on finite integer encodings, without a fixed storage cap.

[F1]

Exact dyadic determinant sign by integer clearance: write $M_{i j} = a_{i j} / 2^{b_{i j}}$ with $b_{i j} \geq 0$ , take $k_{i} = \max_{j} b_{i j}$ , form the integer matrix $N_{i j} = 2^{k_{i}} M_{i j}$ , and return the sign of its integer Leibniz sum.

[F2]

Dyadic orientation and lifted sphere determinants: the dyadic determinant is the signed permutation sum, with exactly one entry from each row in each product.

[F3]

Clearing dyadic row denominators preserves determinant sign: positive power-of-two row clearance preserves determinant sign and zero.

Proof

1.1givenF1constructalgebra

Each finitely encoded dyadic entry can be put in the form in [F1] by integer shifts and cancellation of powers of two; zero uses exponent zero. Since $s \geq 1$ , every row has a nonempty finite list of exponents and its maximum $k_{i}$ exists and is computed by finitely many comparisons. Then $N_{i j} = a_{i j} 2^{k_{i} - b_{i j}}$ is an exactly computable integer.

2.1F1F2F3step 1.1algebra

In each permutation product of $N$ , the row factors multiply to the same positive integer $C = \prod_{i} 2^{k_{i}}$ . Thus [F2] gives $\det N = C \det M$ , the sign-preserving identity underlying [F3]. The integer sum in [F1] is exactly $\det N$ , so the returned sign equals $sgn (\det M)$ , also when this value is zero.

3.1givenF1step 1.1step 2.1construct∎

There are exactly $s!$ permutations, which can be enumerated in lexicographic order from the finite set of tuples of length $s$ with entries in ${0, \dots, s - 1}$ by retaining those with distinct entries. Each product, sum, integer shift and sign comparison operates on finite integer encodings and terminates. Hence all loops and the algorithm terminate, even for singular matrices and $s = 1$ ; there is no pivot division. All constructions are explicit and finite, so no axiom of choice is used.

Depends on

Used by

Certified predicate for exact dyadic geometric inputs Algorithm

Cited to discharge well-definedness by Exact dyadic determinant sign by integer clearance.

Dependency tree · two levels

6 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

CGAL Manual, Robustness Issues: exact arithmetic and predicates (standard reference, not scraped)