Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 linear map T of Rn sends Lebesgue measurable sets to Lebesgue measurable sets, with λn(T[E])=detTλn(E) when T is invertible and T[E] Lebesgue null when it is not

Statement

Let n1, assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)) and let T:RnRn be linear with matrix A (Linear map between vector spaces over the same field, Every Euclidean linear map has a unique matrix and satisfies Lh2Kh2 for some K0).

  1. Invertible case. If detA0, then T[E] is Lebesgue measurable for every Lebesgue measurable E and λn(T[E])  =  detA  λn(E), both sides possibly +; the product is defined in R because detA>0.
  2. Singular case. If detA=0, then T[E] is Lebesgue measurable with λn(T[E])=0 for every ERn.

The singular clause is stated as nullity and not as a product. When detA=0 and λn(E)=+ the expression detAλn(E) is 0(+), which The extended real line R=R{,+}, its order, and the arithmetic that is left undefined leaves undefined; writing the conclusion as λn(T[E])=0 says the same thing wherever the product is defined and remains a statement where it is not.

Facts & Assumptions

Given: A natural number n1, the Axiom of Countable Choice, a linear map T of Rn with matrix A, and a set ERn.

[L1]

An invertible linear map carries Borel sets to Borel sets, and there is a strictly positive real c(T)=λn(T[(0,1]n]) with λn(T[E])=c(T)λn(E) for every Borel E, with c(ST)=c(S)c(T) and c(id)=1 (An invertible linear map of Rn scales the Lebesgue measure of every Borel set by a positive constant depending only on the map).

[L2]

λn(Dp(c)[(0,1]n])=c=detDp(c) and λn(Epq[(0,1]n])=1=detEpq (A coordinate scaling and a coordinate transposition send the unit cube to a set of measure equal to the absolute value of the determinant).

[L3]

For n2 a shear satisfies λn(Tij(t)[(0,1]n])=1=detTij(t) (A shear sends the unit cube to a set of Lebesgue measure one).

[L4]

Every proper linear subspace WRn is Lebesgue measurable with λn(W)=0 (Every affine hyperplane of Rn, and hence every proper linear subspace, is Lebesgue null).

[L5]

A Lipschitz self-map of Rn carries a set of Lebesgue outer measure zero to a Lebesgue measurable set of measure zero (A Lipschitz self-map of Rn carries Lebesgue null sets to Lebesgue null sets, Lipschitz map, α-Hölder map for rational 0<α1, and contraction).

[L6]

E is Lebesgue measurable if and only if E=HW for an Fσ set H and a set W with λn(W)=0 (Assuming countable choice, four equivalent descriptions of a Lebesgue measurable subset of Rn, condition 4; Gδ and Fσ subsets of a topological space, agreeing with the real-line notion).

[F1]
[F3]

For every n1 and every real matrix AMn(R), A is invertible if and only if det(A)0 (A finite square real matrix is invertible if and only if its determinant is nonzero).

[F5]

For a linear map T:VW, imT:={T(v):vV} (Kernel and image of a linear map), and it is a linear subspace (The kernel and image are linear subspaces, and a linear map is injective if and only if its kernel is trivial).

[F6]

Every product with one factor 0 and the other ± is left undefined in R (The extended real line R=R{,+}, its order, and the arithmetic that is left undefined).

[F7]

Let SN; if 0S and σ(n)S whenever nS, then S=N (The principle of mathematical induction).

Proof

technique · direct
1.1

Suppose detA=0. Then imT is a proper linear subspace of Rn: were T surjective, each standard vector ei would be T(vi) for some vi, finitely many instantiations, and the matrix B with bji:=(vi)j would satisfy (AB)ki=jakj(vi)j=(Tvi)k=(ei)k, so AB=In and detAdetB=detIn=1, contradicting detA=0.

F2F3F4F5
1.2

T is Lipschitz, since TxTy2=T(xy)2Kxy2 for a real K0.

F4
1.3

Every elementary matrix M of Mn(R) satisfies c(M)=detM: at n=1 the only elementary matrices are the scalings D0(c), and for n2 the three types are the scalings, the transpositions and the shears, whose unit-cube images have the measures c, 1 and 1, matching det in each case.

L1L2L3F1
2.1

Suppose detA0, so A is invertible and factors as a finite product M1Mr of elementary matrices, each invertible. Multiplicativity of c and of the determinant then give c(T)=sc(Ms)=sdetMs=detA by induction on r, the empty product giving c(id)=1=detIn.

step 1.1step 1.3L1F1F2F3F7
2.2

For detA=0, step 1.1 makes imT a proper linear subspace, hence Lebesgue null; every T[E] is a subset of it, so completeness makes T[E] Lebesgue measurable with λn(T[E])=0, which is claim 2; stating it as a product would require the undefined 0(+) when λn(E)=+.

step 1.1L4L7F6
3.1

For detA0 and E Lebesgue measurable, write E=HW with H an Fσ set, hence Borel, and λn(W)=0; then T[E]=T[H]T[W], where T[H] is Borel and T[W] is Lebesgue measurable of measure 0 by step 1.2 and the Lipschitz lemma, so T[E] is measurable. Since HE and EHW, and T[H]T[E] with T[E]T[H]T[W], both pairs differ by null sets, so λn(E)=λn(H) and λn(T[E])=λn(T[H])=c(T)λn(H)=detAλn(E), which is claim 1; claim 2 is step 2.2.

step 1.2step 2.1step 2.2L1L5L6L7

Depends on

Used by

Dependency tree · two levels

156 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