Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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 coordinate scaling and a coordinate transposition send the unit cube to a set of measure equal to the absolute value of the determinant

Statement

Let n≥1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Work with real matrices and identify a matrix with the linear map it defines by (Ax)i=∑j<naijxj (Every Euclidean linear map has a unique matrix and satisfies ∥Lh∥2≤K∥h∥2 for some K≥0).

  1. Coordinate scaling. Let p<n, let c≠0 be real and let Dp(c) be the elementary matrix obtained from the identity by multiplying row p by c (Elementary matrices obtained by applying one elementary row operation to an identity matrix). Then Dp(c) sends x to the point whose p-th coordinate is cxp and whose other coordinates are those of x, the image Dp(c)[(0,1]n] is Lebesgue measurable, and λn(Dp(c)[(0,1]n])  =  ∣c∣  =  ∣det⁡Dp(c)∣.
  2. Coordinate transposition. Let n≥2, let p≠q be below n and let Epq be the elementary matrix interchanging rows p and q. Then Epq exchanges the p-th and q-th coordinates, Epq[(0,1]n]=(0,1]n, and λn(Epq[(0,1]n])  =  1  =  ∣det⁡Epq∣.

Facts & Assumptions

Given: A natural number n≥1, the Axiom of Countable Choice, and the elementary matrices Dp(c) and Epq over R.

[L1]

If ai≤bi are real for i<n, then any box obtained from the coordinate interval product ∏i<n[ai,bi] by independently choosing for each endpoint whether it is included has Lebesgue measure ∏i<n(bi−ai) (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included). In particular (u,v]n=B(u,v) (Half-open boxes in Rn and their volume).

[F1]

An elementary matrix is a matrix obtained by applying one elementary row operation to the identity matrix In; there are three types: Epq interchanges rows p and q; Dp(c) multiplies row p by c≠0; and Tpq(c) adds c times row q to the distinct row p (Elementary matrices obtained by applying one elementary row operation to an identity matrix, Rectangular matrix multiplication and the identity matrix In, including zero-sized shapes).

[F2]

Let n≥1 and let A∈Mn(R) be a matrix over a commutative ring; interchanging two rows changes det⁡(A) to −det⁡(A), and multiplying one row by any c∈R changes it to cdet⁡(A) (For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged, claims 1 and 2; For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix).

[F3]

If A is upper or lower triangular over a commutative ring, with n≥1, then det⁡(A)=∏i<naii (The determinant of a triangular matrix is the product of its diagonal entries).

[F4]

For every linear L:Rm→Rn there is a unique matrix A such that (Lh)i=∑j<maijhj (Every Euclidean linear map has a unique matrix and satisfies ∥Lh∥2≤K∥h∥2 for some K≥0).

[F5]

The absolute value satisfies ∣c∣>0 for c≠0, ∣c∣=c for c≥0 and ∣c∣=−c for c≤0 (Absolute value in an ordered field, Basic properties of the absolute value).

Proof

technique · direct
1.1F1F2F3F5

The identity matrix is triangular with every diagonal entry 1, so det⁡In=1; the row-operation table applied to In then gives det⁡Dp(c)=c and det⁡Epq=−1, hence ∣det⁡Dp(c)∣=∣c∣ and ∣det⁡Epq∣=1.

1.2F1F4

Reading off the matrix entries, Dp(c) sends x to the point with p-th coordinate cxp and the other coordinates unchanged, and Epq sends x to the point with p-th coordinate xq, q-th coordinate xp and the others unchanged.

2.1step 1.2L1F5

For claim 1, Dp(c)[(0,1]n]={ x:0<xi≤1 for i≠p, xp∈c (0,1] }. When c>0 this is the half-open box with p-th side (0,c]; when c<0 it is the box with p-th side [c,0) and all other sides (0,1]. In either case [L1] gives Lebesgue measurability and measure ∏i<n(bi−ai)=∣c∣.

2.2step 1.2L1

For claim 2, Epq restricts to a bijection of (0,1]n onto itself, since exchanging two coordinates of a point all of whose coordinates lie in (0,1] again gives such a point and the map is its own inverse; hence the image is (0,1]n, of measure 1.

3.1step 1.1step 2.1step 2.2∎

Steps 1.1, 2.1 and 2.2 are the two claims.

Depends on

Used by

Dependency tree · two levels

60 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