ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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 trigonometry-free oscillator $\psi(x) = \inf_{n \in \mathbb{Z}} |x - n|$ is well defined and attained at a nearest integer, takes values in $[0, 1/2]$ , vanishes exactly on $\mathbb{Z}$ , equals $1/2$ at half-integers, and is $1$ -periodic

Example

Identify $\mathbb{Z}$ with its canonical copy in $\mathbb{R}$ (The integers as equivalence classes of pairs of naturals, The integers embed in the rationals, The rationals embed densely in the reals) and for $x \in \mathbb{R}$ put

$D(x) \;:=\; \{\, |x - n| \ : \ n \in \mathbb{Z} \,\}, \qquad \psi(x) \;:=\; \inf D(x)$

(Greatest lower bound (infimum)). Write $m := \lfloor x \rfloor$ for the integer part of $x$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ ) and $t := x - m$ , so $0 \le t < 1$ . Then:

Existence and attainment. $\psi(x)$ exists and is attained: $\psi(x) \;=\; \min\{\, t,\ 1 - t \,\} \;=\; \min\bigl\{\, |x - m|,\ |x - (m+1)| \,\bigr\} ,$ so $\psi(x) = |x - n|$ for $n = m$ or $n = m + 1$ , and $\psi(x) = \min D(x)$ (Maximum and minimum of a set).
Range. $0 \le \psi(x) \le 1/2$ for every real $x$ , and every value in $[0, 1/2]$ occurs: the range of $\psi$ is exactly the interval $[0, 1/2]$ (Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).
Zero set. $\psi(x) = 0$ if and only if $x \in \mathbb{Z}$ .
Half-integers. $\psi(m + 1/2) = 1/2$ for every $m \in \mathbb{Z}$ .
Periodicity. $\psi(x + 1) = \psi(x)$ for every real $x$ .

What this function is for. It is the elementary, trigonometry-free substitute for $\sin$ : it is bounded, it oscillates, and on every punctured neighbourhood of $0$ the composite $\psi(1/x)$ attains both the value $0$ and the value $1/2$ . Claims 3 and 4 are exactly what the companion counterexample $\psi(1/x)$ has no limit at $0$ : two sequences tending to $0$ give values constantly $0$ and constantly $1/2$ evaluates, and claim 2 is what the squeeze argument of $x\,\psi(1/x) \to 0$ as $x \to 0$ , by the squeeze theorem uses.

Facts & Assumptions

Given: A real $x$ ; the set $D(x) = \{\, |x - n| : n \in \mathbb{Z} \,\}$ ; the integer $m := \lfloor x \rfloor$ and the real $t := x - m$ . Integers are identified with their canonical copies in $\mathbb{R}$ .

[L1]

Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ ). Hence $0 \le t < 1$ and $0 < 1 - t \le 1$ , where $1 - t = (m+1) - x$ .

[L2]

Integers in $\mathbb{R}$ : the embeddings $\mathbb{N} \to \mathbb{Z} \to \mathbb{Q} \to \mathbb{R}$ are injective and preserve $0$ , $1$ , addition and order; $\mathbb{Z}$ is a totally ordered commutative ring, closed under $n \mapsto n + 1$ and $n \mapsto n - 1$ ; every integer $\ge 0$ is the image of a unique natural; and a natural $j \ne 0$ satisfies $j \ge 1$ , so an integer $> 0$ is $\ge 1$ and consequently, for integers $n < n'$ , one has $n + 1 \le n'$ (The integers as equivalence classes of pairs of naturals, The naturals embed in the integers, The integers embed in the rationals, The rationals embed densely in the reals, The integers form a totally ordered ring, The integers form a commutative ring, Discreteness: $\sigma(n)$ is the immediate successor, The natural numbers $\mathbb{N}$ (von Neumann)).

[L3]

Infimum: $\ell = \inf S$ when $\ell \le s$ for every $s \in S$ and $\ell' \le \ell$ for every lower bound $\ell'$ of $S$ . So a lower bound of $S$ that belongs to $S$ is the infimum, and is then also the minimum of $S$ (Greatest lower bound (infimum), Maximum and minimum of a set, Lower bound, bounded below, bounded set).

[L4]

Absolute value: $|u| \ge 0$ ; $|u| = 0$ exactly when $u = 0$ ; $|u| = u$ for $u \ge 0$ and $|u| = -u$ for $u \le 0$ (Basic properties of the absolute value, Absolute value in an ordered field).

[L5]

Order and field arithmetic in $\mathbb{R}$ : the order is total and trichotomy holds; translation invariance and adding inequalities (Order is preserved by adding a constant and by adding inequalities); $0 < 1$ (The multiplicative identity is positive), so $2 > 0$ , $1/2 > 0$ (Inverses of positives are positive, and reciprocation reverses order), $1/2 < 1$ and $1 - 1/2 = 1/2$ (Sign rules for products and monotonicity of multiplication, Field); and the minimum of a two-element set of reals (Maximum and minimum of a set, Ordered field).

Verification

technique · direct

1.1

$D(x)$ is nonempty and $0$ is a lower bound of it: the integer $0$ gives $|x - 0| \in D(x)$ , and $|x - n| \ge 0$ for every $n \in \mathbb{Z}$ .

L2L4

1.2

By [L1] the integer $m = \lfloor x \rfloor$ satisfies $m \le x < m + 1$ , so $t = x - m$ satisfies $0 \le t < 1$ , and $(m+1) - x = 1 - t$ satisfies $0 < 1 - t \le 1$ .

L1L5

2.1

Every element of $D(x)$ is at least $\min\{t, 1-t\}$ . Let $n \in \mathbb{Z}$ . By [L2] and totality either $n \le m$ or $m < n$ , and in the second case $m + 1 \le n$ . If $n \le m$ then $x - n \ge x - m = t \ge 0$ , so $|x - n| = x - n \ge t$ . If $m + 1 \le n$ then $n - x \ge (m+1) - x = 1 - t > 0$ , so $|x - n| = n - x \ge 1 - t$ . In both cases $|x - n| \ge \min\{t, 1-t\}$ .

step 1.2L2L4L5

2.2

Both $t$ and $1 - t$ belong to $D(x)$ : since $t \ge 0$ we have $t = |x - m|$ , and since $1 - t > 0$ we have $1 - t = |x - (m+1)|$ , with $m$ and $m+1$ in $\mathbb{Z}$ .

step 1.2L2L4

3.1

Hence $\min\{t, 1-t\}$ is a lower bound of $D(x)$ belonging to $D(x)$ , so by [L3] it is the greatest lower bound and also the minimum: $\psi(x) = \min\{t, 1-t\} = \min\{|x - m|, |x - (m+1)|\}$ , attained at $n = m$ or at $n = m+1$ . This is claim 1.

step 2.1step 2.2L3L5

4.1

Claim 2, the inclusion. $\psi(x) \ge 0$ , since $t \ge 0$ and $1 - t > 0$ ; and $\psi(x) \le 1/2$ : if $t \le 1/2$ then $\psi(x) \le t \le 1/2$ , while if $1/2 < t$ then $1 - t < 1 - 1/2 = 1/2$ and $\psi(x) \le 1 - t < 1/2$ . So $0 \le \psi(x) \le 1/2$ for every real $x$ .

step 1.2step 3.1L5

4.2

Claim 3. If $\psi(x) = 0$ then $\min\{t, 1-t\} = 0$ ; since $1 - t > 0$ this forces $t = 0$ , that is $x = m \in \mathbb{Z}$ . Conversely if $x \in \mathbb{Z}$ then $|x - x| = 0$ lies in $D(x)$ and $0$ is a lower bound of $D(x)$ by step 1.1, so $\psi(x) = 0$ by [L3].

step 1.1step 1.2step 3.1L3L4L5

4.3

Claim 4. Let $m \in \mathbb{Z}$ and $x := m + 1/2$ . Since $0 < 1/2 < 1$ we have $m \le x < m + 1$ , so the uniqueness in [L1] gives $\lfloor x \rfloor = m$ and $t = 1/2$ ; then step 3.1 gives $\psi(x) = \min\{1/2,\ 1 - 1/2\} = \min\{1/2, 1/2\} = 1/2$ .

step 3.1L1L5

4.4

Claim 5. The map $n \mapsto n + 1$ is a bijection of $\mathbb{Z}$ onto itself, with inverse $n \mapsto n - 1$ [L2]; so, substituting $n = n' + 1$ , $D(x+1) = \{\, |(x+1) - n| : n \in \mathbb{Z} \,\} = \{\, |x - n'| : n' \in \mathbb{Z} \,\} = D(x) .$ Being infima of the same set, $\psi(x+1)$ and $\psi(x)$ are equal by step 3.1 applied at $x + 1$ and at $x$ .

step 3.1L2L3

5.1

Claim 2, the exact range. Every value of $\psi$ lies in $[0,1/2]$ by step 4.1. Conversely let $s$ satisfy $0 \le s \le 1/2$ ; then $0 \le s < 1$ , so $0 \le s < 0 + 1$ and the uniqueness in [L1] gives $\lfloor s \rfloor = 0$ and $t = s$ ; and $s \le 1/2 \le 1 - s$ because $2s \le 1$ , so step 3.1 gives $\psi(s) = \min\{s, 1-s\} = s$ . Hence the range of $\psi$ is exactly $[0,1/2]$ .

step 3.1step 4.1L1L5

6.1

So $\psi$ is defined at every real, is attained at a nearest integer, has range exactly $[0,1/2]$ , vanishes exactly on $\mathbb{Z}$ , takes the value $1/2$ at every half-integer, and is $1$ -periodic.

step 3.1step 4.1step 4.2step 4.3step 4.4step 5.1∎

Remarks

No completeness of $\mathbb{R}$ is needed for the infimum here. The general existence theorem Every nonempty set bounded below has an infimum would supply $\inf D(x)$ from the least-upper-bound property, but step 3.1 does not use it: the infimum is produced by exhibiting an element of $D(x)$ that is also a lower bound, which is Greatest lower bound (infimum) read directly. Completeness does enter, once, through Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$ , whose existence half is the Archimedean property.
Why $\min\{t, 1-t\}$ and not "the distance to the nearest integer". The phrase presupposes that a nearest integer exists, which is exactly what step 2.2 establishes and what the picture cannot. When $t = 1/2$ there are two nearest integers, $m$ and $m+1$ , and the formula is indifferent to which is chosen, so nothing has to be selected.
$\psi$ is the triangle wave of amplitude $1/2$ and period $1$ — not the sawtooth $x - \lfloor x \rfloor$ , which drops discontinuously at every integer: on $[0, 1/2]$ it is $\psi(s) = s$ by step 5.1, and periodicity and the reflection $\psi(-x) = \psi(x)$ — immediate from $D(-x) = \{\, |-x - n| : n \in \mathbb{Z} \,\} = \{\, |x + n| : n \in \mathbb{Z} \,\} = D(x)$ , using $|-u| = |u|$ and the bijection $n \mapsto -n$ of $\mathbb{Z}$ — determine it everywhere.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 32 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

Floor and ceiling functions (Wikipedia) (standard reference, not scraped)
Infimum and supremum (Wikipedia) (standard reference, not scraped)
Triangle wave (Wikipedia) (standard reference, not scraped)