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

Statement

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

  1. Degenerate boxes. If aibi 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  :=  {xRn: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 n1, the Axiom of Countable Choice, an index i0<n and a real c.

[L1]

Every set R with RRR is Lebesgue measurable with λn(R)=i<n(biai), and it gives measure 0 to all of them whenever ai=bi for some i<n (A box in Rn with parameters aibi is Lebesgue measurable of measure i<n(biai), 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)kN, μ(kNEk)k=0μ(Ek) (Finite and countable subadditivity of measures).

[F2]

[a,b]:={xRm:ajxjbj (j<m)} (Axis-parallel rectangles in Rm and their volume).

[F3]

A measurable set NA 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 xF there is a natural number n1 with x<n1F (Every complete ordered field is Archimedean).

[F5]

B(a,b):={xRn:ai<xibi  for every i<n} (Half-open boxes in Rn and their volume).

Proof

technique · direct
1.1

Claim 1 is the degenerate case of the box theorem, whose value i<n(biai) carries the factor bi0ai0=0.

L1F2F5
1.2

For a natural number k put Pk:={xRn:xi0=c and xik for every ii0}. This is always the closed rectangle with sides [k,k] for ii0 and the degenerate side [c,c] in coordinate i0.

F2
2.1

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

step 1.1step 1.2L2F3
2.2

The union kNPk 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.

step 1.2F4
3.1

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}.

step 2.1step 2.2L2L3F1F3

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