Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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 Hamel coefficient has dense graph and a nonmeasurable kernel

Statement

Assume AC. Fix a Hamel basis B of R over Q and b∈B. Its coefficient map f=Λb:R→Q⊆R is additive, has dense graph, is unbounded above and below on every nondegenerate interval, and is continuous nowhere. Its kernel W is not Lebesgue measurable, so f is not Lebesgue measurable. No claim that every Hamel basis itself is nonmeasurable is made.

Facts & Assumptions

[F2]

The rationals embed densely in the reals gives rational density; Q is countably infinite gives an enumeration of Q.

[F3]

Every complete ordered field is Archimedean gives natural numbers exceeding any prescribed real bound.

[F7]

Borel measurable and Lebesgue measurable functions on Rn requires Borel preimages to be Lebesgue measurable; The Borel sigma-algebra of a topological space contains closed singletons.

[A1]

Assume The Axiom of Choice, including countable choice for F5–F7.

Proof

Given: The basis vector and coefficient map as in the statement, with the real codomain convention.

1.1F1F2A1

F1 applies under A1. It gives additivity and rational linearity, f(b)=1, and 0≠w∈W. In particular b≠0, Qw⊆W, and f−1{q}=qb+W: subtract qb and apply additivity in either direction. For any u<v choose by F2 a rational r strictly between min⁡(u/w,v/w) and max⁡(u/w,v/w). Then rw∈(u,v), with the order reversed when w<0. Thus W is dense, and translation shows every fiber qb+W is dense.

2.1F2F8step 1.1

For any open rectangle (u,v)×(c,d), F2 gives rational q in (c,d); step 1.1 gives x in (u,v)∩(qb+W), so (x,f(x))=(x,q) lies in the rectangle. Such rectangles form a basis, proving graph density. Taking (c,d) wholly above any prescribed M or wholly below -M shows both unboundedness assertions on each nondegenerate interval, whose interior contains an open interval. For any x_0 and δ>0, density gives x with ∣x−x0∣<δ and f(x)∈(f(x0)+2,f(x0)+3). This violates F8 with ϵ=1, so f is continuous at no x_0.

2.2F2F3F4F5F6A1step 1.1

Suppose W measurable and put Wm=W∩[−m,m], m a positive integer. F5 and F6, licensed by A1, make these measurable with finite measure am≤2m. Distinct rational translates qb+W are disjoint: an equality qb+w=rb+w′ gives q=r after applying f and step 1.1. F2 enumerates the infinitely many rationals q with ∣qb∣<1; infinitude follows from density in (−1/∣b∣,1/∣b∣), since any finite list can be avoided in a smaller subinterval. The sets Wm+qb along this enumeration are pairwise disjoint and all lie in [−m−1,m+1]. By F4 each has measure a_m. If am>0, choose by F3 a natural N with Nam>2m+2. Finite additivity F5 and the enclosing interval value F6 then give Nam≤2m+2, contradiction. Hence every a_m is zero.

3.1F1F2F3F4F5F6F7step 2.2

By F3, W=⋃m≥1Wm. Disjointizing this sequence and using F5's countable additivity shows W null. All cosets qb+W are null by F4, and their countable union is R by F1's rational coefficient decomposition and F2's enumeration. Disjointization and F5 again make R null, contradicting F6's value one on [0,1] and monotonicity. Thus W is not measurable. Finally {0} is closed and Borel, so if f were Lebesgue measurable, F7 would make f−1{0}=W measurable, a contradiction. QED.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

101 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