CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Assuming choice, a Hamel-basis additive map transported through $\exp$ gives a discontinuous logarithmic function that is not $c \log$

Statement refuted

Continuity cannot be omitted from the multiplicative-to-additive characterisation. Assuming the Axiom of Choice, there is a function $f : (0, \infty) \to R$ satisfying $f (x y) = f (x) + f (y)$ that is discontinuous and is not $c \log$ for any scalar $c$ .

Facts & Assumptions

Given: The Axiom of Choice (The Axiom of Choice).

[L1]

Under choice, $R$ has a Hamel basis over $Q$ ; a chosen basis element has an additive coefficient map $g : R \to R$ , and there is a nonzero complementary vector on which that coefficient map vanishes (Assuming the Axiom of Choice, $R$ has a Hamel basis over $Q$ : there is $B \subseteq R$ such that every real is a finite $Q$ -linear combination of elements of $B$ in exactly one way, and each basis vector carries a well-defined $Q$ -linear coefficient map).

[L2]

An additive real function that is continuous at one point is scalar multiplication (Six regularity conditions each force an additive $f : R \to R$ to be $x \mapsto f (1) x$ : continuity at a single point, monotonicity on a nondegenerate interval, boundedness above on one, boundedness below on one, constancy of sign on one, and a graph that is not dense in $R^{2}$ ).

[L3]

$\exp (s + t) = \exp (s) \exp (t)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

[L4]

Exponential is continuous and strictly increasing (The exponential function is strictly increasing) and is a bijection from $R$ onto $(0, \infty)$ (The exponential is a continuous bijection from $R$ onto $(0, \infty)$ ).

[L5]

A composite of continuous functions is continuous (A composite of continuous functions is continuous, with no side hypothesis of the kind the composition of limits needs).

[F1]

$\log$ is the inverse of $\exp$ (The natural logarithm as the inverse of the exponential function).

Counterexample

technique · direct

1.1

Choose a Hamel basis element $b_{*}$ , its coefficient map $g$ , and a nonzero vector $w$ in the complementary span. Then $g (b_{*}) = 1$ and $g (w) = 0$ .

L1given

1.2

For $x > 0$ , let $t$ be the unique real with $x = \exp (t)$ , and define $f (x) : = g (t)$ . This is well defined by bijectivity in [L4].

L4construct

2.1

The map $g$ is not scalar multiplication. If $g (t) = c t$ , then $0 = g (w) = c w$ and $w \neq 0$ force $c = 0$ , contradicting $g (b_{*}) = 1$ .

step 1.1algebra

2.2

If $x = \exp (s)$ and $y = \exp (t)$ , then [L3] gives $x y = \exp (s + t)$ , so $f (x y) = g (s + t) = g (s) + g (t) = f (x) + f (y)$ .

step 1.2L3L1

3.1

If $f = c \log$ , then composing with exponential and using [F1] gives $g (t) = f (\exp t) = c t$ , contradicting step 2.1.

step 1.2step 2.1F1

3.2

If $f$ were continuous, then $g = f \circ \exp$ would be continuous by [L4] and [L5]. The regularity theorem [L2] would make $g$ scalar multiplication, again contradicting step 2.1.

step 1.2step 2.1L4L5L2

4.1

Thus the constructed $f$ satisfies the functional equation but is discontinuous and is not a scalar multiple of $\log$ .

step 2.2step 3.1step 3.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 209 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Henry Ricardo, The Equivalence of Definitions of the Natural Logarithm Function (standard reference, not scraped)

Assuming choice, a Hamel-basis additive map transported through exp⁡exp gives a discontinuous logarithmic function that is not clog⁡clog