Alphabeta Math
PropositionStatement: 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 box with a degenerate side is Lebesgue null, and so is every coordinate hyperplane in Rn

Statement

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

  1. Degenerate boxes. If ai≤bi are reals with ai0=bi0 for some i0<n, then every set R between the open box {x:ai<xi<bi (i<n)} and the closed rectangle [a,b] is Lebesgue measurable with λn(R)=0.
  2. Coordinate hyperplanes. For i0<n and a real c, the set Hi0,c  :=  { x∈Rn:xi0=c } is Lebesgue measurable with λn(Hi0,c)=0.

At n=1 the hyperplane H0,c is the singleton {c}.

Facts & Assumptions

Given: A natural number n≥1, the Axiom of Countable Choice, an index i0<n and a real c.

[L1]

Every set R with R∘⊆R⊆R‾ is Lebesgue measurable with λn(R)=∏i<n(bi−ai), and it gives measure 0 to all of them whenever ai=bi for some i<n (A box in Rn with parameters ai≤bi is Lebesgue measurable of measure ∏i<n(bi−ai), whichever of its faces are included).

[L2]

Assuming countable choice, L(Rn) is a sigma-algebra and λn is a complete measure on it (Assuming countable choice, L(Rn) is a sigma-algebra containing every elementary set and λn is a complete measure extending elementary volume).

[L3]

Assuming countable choice, every Borel subset of Rn is Lebesgue measurable (Assuming countable choice, every Borel subset of Rn is Lebesgue measurable).

[F1]

For a measure μ and measurable (Ek)k∈N, μ(⋃k∈NEk)≤∑k=0∞μ(Ek) (Finite and countable subadditivity of measures).

[F2]

[a,b]:={x∈Rm:aj≤xj≤bj (j<m)} (Axis-parallel rectangles in Rm and their volume).

[F3]

A measurable set N∈A is μ-null if μ(N)=0 (Measure-null sets and almost-everywhere statements relative to a measure); a sigma-algebra is closed under countable unions (Sigma-algebras).

[F4]

Every complete ordered field F is Archimedean: for every x∈F there is a natural number n≥1 with x<n⋅1F (Every complete ordered field is Archimedean).

[F5]

B(a,b):={ x∈Rn:ai<xi≤bi  for every i<n } (Half-open boxes in Rn and their volume).

Proof

technique · direct
1.1L1F2F5

Claim 1 is the degenerate case of the box theorem, whose value ∏i<n(bi−ai) carries the factor bi0−ai0=0.

1.2F2

For a natural number k put Pk:={ x∈Rn:xi0=c and ∣xi∣≤k for every i≠i0 }. This is always the closed rectangle with sides [−k,k] for i≠i0 and the degenerate side [c,c] in coordinate i0.

2.1step 1.1step 1.2L2F3

Each Pk is Lebesgue measurable of measure 0 by claim 1.

2.2step 1.2F4

The union ⋃k∈NPk is Hi0,c, since a point of the hyperplane has finitely many coordinates and the Archimedean property supplies a natural k above each ∣xi∣ and above ∣c∣.

3.1step 2.1step 2.2L2L3F1F3∎

Therefore Hi0,c is a countable union of measurable sets, hence measurable, and countable subadditivity gives λn(Hi0,c)≤∑k=0∞λn(Pk)=0; at n=1 the set H0,c is {c}.

Depends on

Used by

Dependency tree · two levels

49 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