ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)

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.

The function equal to $q$ at a rational $p / q$ in lowest terms and to $0$ at every irrational is finite at every point and unbounded on every nondegenerate interval

Example

Throughout, $N \subseteq Z \subseteq Q \subseteq R$ denotes the canonical copies. Natural numbers, integers and rationals are written directly when used in real arithmetic.

Let $q (x)$ be the least denominator of a rational $x$ (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ ) and define $h : R \to R$ by

$h (x) : = q (x) for x \in Q, h (x) : = 0 for x \notin Q,$

where a natural $q$ is identified with its canonical real value (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field) and $Q$ is the canonical copy of the rationals inside $R$ (The rationals embed densely in the reals). Equivalently $h (x) = 1 / t (x)$ at a rational $x$ , where $t$ is Thomae's function. Then:

$h (x)$ is a real number for every real $x$ : $h$ is finite at every point;
$h$ is unbounded on every nondegenerate interval (Lower bound, bounded below, bounded set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length): for all reals $a < b$ and every real $M$ there is $x \in (a, b)$ with $h (x) > M$ .

So a function may be finite at every single point and yet fail to be bounded on every interval, however short. In particular $h$ is bounded on no neighbourhood of any point.

Facts & Assumptions

Given: The function $h$ above, with $q (x) = \min {q \in N : q \geq 1 and q x \in Z}$ for $x \in Q$ .

[A1]

$q (x) \geq 1$ is a natural with $q (x) x \in Z$ , and $q (x) \leq q$ for every natural $q \geq 1$ with $q x \in Z$ (The Dirichlet function $1_{Q}$ , and Thomae's function $t$ with $t (x) = 1 / q$ at a rational $x = p / q$ in lowest terms with $q \geq 1$ and $t (x) = 0$ at every irrational $x$ ).

[L1]

Strictly between any two distinct reals there lies a rational (The rationals embed densely in the reals, Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

[L2]

A nonzero integer has absolute value at least $1$ , since no integer lies strictly between $0$ and $1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ , Basic properties of the absolute value).

[L3]

For every real $η > 0$ there is a natural $n \geq 1$ with $1 / n < η$ , and for every real $x$ a natural $n \geq 1$ with $x < n$ ; the natural numbers $\geq 1$ are positive in $R$ and their order is preserved there (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[L4]

$R$ is an ordered field (Complete ordered field (least-upper-bound property)).

Verification

technique · direct

1.1A1

Claim 1: for a rational $x$ the value $h (x) = q (x)$ is a canonical natural, hence a real number, and for an irrational $x$ the value is $0$ . Every real falls under exactly one clause, so $h$ is a function $R \to R$ .

1.2A1L2L4

Separation of rationals by their denominators. Let $x \neq y$ be rationals. Then $∣ x - y ∣ \geq 1 / (q (x) q (y))$ . Indeed, put $q_{1} : = q (x)$ , $q_{2} : = q (y)$ , $p_{1} : = q_{1} x$ and $p_{2} : = q_{2} y$ , all integers; then $x - y = (p_{1} q_{2} - p_{2} q_{1}) / (q_{1} q_{2})$ , the numerator is an integer, and it is nonzero because $x \neq y$ ; so its absolute value is at least $1$ .

2.1step 1.2L1L3L4

Claim 2: let $a < b$ be reals and let $M$ be real. Take a rational $x_{1}$ with $a < x_{1} < b$ and put $q_{1} : = q (x_{1})$ . Take a natural $N \geq 1$ with $M < N$ , and put $η : = \min {\frac{1}{q_{1} N}, b - x_{1}} > 0.$

3.1step 2.1L1

With $x_{1}$ , $q_{1}$ , $N$ and $η$ as in step 2.1, take a rational $y$ with $x_{1} < y < x_{1} + η$ . Then $a < x_{1} < y < b$ , so $y \in (a, b)$ ; and $y \neq x_{1}$ with $∣ y - x_{1} ∣ < η \leq 1 / (q_{1} N)$ .

4.1step 1.2step 3.1L3

Hence $q (y) > N$ . If instead $q (y) \leq N$ then $q (y) \leq N$ , and step 1.2 would give $∣ y - x_{1} ∣ \geq 1 / (q_{1} q (y)) \geq 1 / (q_{1} N)$ , contradicting step 3.1.

5.1step 2.1step 3.1step 4.1L3∎

Therefore $h (y) = q (y) > N > M$ , and $y \in (a, b)$ : the values of $h$ on $(a, b)$ exceed every real, so $h$ is unbounded on $(a, b)$ , and hence on every set containing it.

Remarks

Finiteness at a point says nothing about local boundedness. The two notions are often conflated; this example separates them as sharply as possible, since $h$ is unbounded on every nondegenerate interval and yet takes only real values.
$h$ is nowhere continuous, and the oscillation is infinite everywhere. Continuity at $c$ would give a neighbourhood on which $∣ h - h (c) ∣ < 1$ , hence a neighbourhood on which $h$ is bounded, which claim 2 forbids; equivalently $ω_{h} (c) = + \infty$ at every real $c$ (The oscillation $ω_{f} (S) = \sup {∣ f (x) - f (y) ∣ : x, y \in S}$ of $f$ on a set and the oscillation $ω_{f} (c) = \inf_{δ > 0} ω_{f} (A \cap N_{δ} (c))$ at a point, both taken in the extended reals, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point). This is a different pathology from Thomae's function, whose values are bounded by $1$ and which is continuous at every irrational (The Dirichlet function is continuous at no point of $R$ , and Thomae's function is continuous at every irrational and at no rational, so its set of continuity points is exactly the set of irrationals and its oscillation at $c$ equals $t (c)$ ).
The separation estimate is the only arithmetic used. Step 1.2 is the standard fact that two distinct rationals with denominators $q_{1}$ and $q_{2}$ are at least $1 / (q_{1} q_{2})$ apart, and it is proved from nothing more than "a nonzero integer has absolute value at least $1$ ".

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

62 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

Thomae's function (Wikipedia) (standard reference, not scraped)
Elements of Real Analysis (Rutgers University-Camden) (standard reference, not scraped)

The function equal to qq at a rational p/qp/q in lowest terms and to 00 at every irrational is finite at every point and unbounded on every nondegenerate interval