Alphabeta Math
TheoremStatement: 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.

Every affine hyperplane of Rn, and hence every proper linear subspace, is Lebesgue null

Statement

Let n≥1 and assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Then:

  1. For every u∈Rn with u≠0 and every real c, the affine hyperplane Hu,c  :=  { x∈Rn:⟨u,x⟩=c } (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn) is Lebesgue measurable with λn(Hu,c)=0, and so is every subset of it.
  2. Every proper linear subspace W⊊Rn (Linear subspace of a vector space) is Lebesgue measurable with λn(W)=0.

At n=1 a hyperplane is the singleton {c/u0} and the only proper linear subspace is {0}.

Facts & Assumptions

Given: A natural number n≥1, the Axiom of Countable Choice, a nonzero u∈Rn, a real c, and a proper linear subspace W of Rn.

[L1]

Assuming countable choice, 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).

[L2]

For i0<n and a real c, the coordinate hyperplane { x∈Rn:xi0=c } is Lebesgue measurable with measure 0 (A box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in Rn).

[L3]

Assuming countable choice, λn is a complete measure on L(Rn), so every subset of a measurable null set is measurable of measure 0 (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume).

[F1]

The Euclidean inner product of x,y∈Rn is ⟨x,y⟩:=∑k<nxkyk, and it is symmetric, bilinear and positive definite, making Rn an inner product space (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[F2]

For a linear subspace W of an inner product space V, W⊥:={v∈V:⟨v,w⟩=0 for every w∈W}, and {0}⊥=V (The orthogonal complement W⊥={v:⟨v,w⟩=0 for all w∈W}, Linear subspace of a vector space).

[F3]

For every subspace W of a finite-dimensional inner product space V, W⊥⊥=W (In finite dimension, W⊥⊥=W and dim⁡W+dim⁡W⊥=dim⁡V).

[F4]

For every linear L:Rm→Rn there is K≥0 with ∥Lh∥2≤K∥h∥2 for every h (Every Euclidean linear map has a unique matrix and satisfies ∥Lh∥2≤K∥h∥2 for some K≥0, Linear map between vector spaces over the same field).

Proof

technique · direct
1.1F1

Fix j<n with uj≠0 and define Ψ:Rn→Rn by Ψ(x)l:=xl for l≠j and Ψ(x)j:=(c−∑l≠julxl)/uj. Then Ψ carries the coordinate hyperplane P:={ x:xj=0 } onto Hu,c: a point of P has ⟨u,Ψ(x)⟩=∑l≠julxl+ujΨ(x)j=c, and conversely a point y∈Hu,c is Ψ(x) for the point x agreeing with y off the coordinate j and having xj=0.

1.2F4F5

Ψ is Lipschitz: the difference Ψ(x)−Ψ(x′) equals L(x−x′) for the linear map L obtained from Ψ by deleting the constant c/uj, so d2(Ψ(x),Ψ(x′))=∥L(x−x′)∥2≤K d2(x,x′) for a real K≥0.

2.1step 1.1step 1.2L1L2L3

The coordinate hyperplane P is Lebesgue measurable of measure 0, hence of outer measure 0, so steps 1.1 and 1.2 with the Lipschitz lemma give that Hu,c=Ψ[P] is Lebesgue measurable with λn(Hu,c)=0; completeness then gives the same for every subset of it, which is claim 1.

3.1step 2.1L3F1F2F3∎

If W is a proper linear subspace then W⊥≠{0}: otherwise W=W⊥⊥={0}⊥=Rn. Choosing a nonzero u∈W⊥ puts W inside Hu,0, so claim 1 and completeness make W Lebesgue measurable of measure 0; at n=1 the hyperplane Hu,c is the singleton {c/u0} and the only proper subspace is {0}.

Depends on

Used by

Dependency tree · two levels

96 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