ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passverified 2026-08-03 (gpt-5.6-sol-codex-subscription)

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.

No rational squares to $3$ or to $6$ , and none cubes to $2$ : three instances of the rational-root corollary

Example

Powers are the natural powers of Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ in the commutative monoid $(Q, \cdot, 1)$ of the field $Q$ (The rationals form a field, Field), and $j : Z \to Q$ , $j (u) = [(u, 1)]$ , is the embedding of The integers embed in the rationals. There is no $x \in Q$ with

$x^{2} = j (3), nor with x^{2} = j (6), nor with x^{3} = j (2) .$

Each is an instance of A rational root of $x^{k} = m$ is an integer: if $k \geq 1$ , $m \in Z$ , $x \in Q$ and $x^{k}$ is the image of $m$ , then $x$ is the image of an integer: such an $x$ would have to be $j (z)$ for an integer $z$ , and the remaining work is to rule out the finitely many integer candidates by size, which is done below.

Facts & Assumptions

Given: The integers $2$ , $3$ , $4$ , $6$ , $8$ , $9$ and the rationals they name under $j$ .

[L1]

If $k \geq 1$ , $m \in Z$ , $x \in Q$ and $x^{k} = j (m)$ , then $x = j (z)$ for some $z \in Z$ (A rational root of $x^{k} = m$ is an integer: if $k \geq 1$ , $m \in Z$ , $x \in Q$ and $x^{k}$ is the image of $m$ , then $x$ is the image of an integer).

[L2]

$j$ is injective and preserves addition and multiplication (The integers embed in the rationals); $Q$ is a field, so $(Q, \cdot, 1)$ is a commutative monoid (The rationals form a field, Field, Semigroup and monoid, The rationals as equivalence classes of pairs of integers, Arithmetic on the rationals).

[L3]

$g^{0} = e$ and $g^{σ (k)} = g^{k} g$ in a monoid (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ ); the exponent laws hold for natural exponents in a monoid (Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute).

[L4]

$∣ x ∣ \geq 0$ ; $∣ x ∣ = 0$ exactly when $x = 0$ ; $∣ x y ∣ = ∣ x ∣ ∣ y ∣$ ; $∣ x ∣ = x$ for $x \geq 0$ (The absolute value $∣ a ∣$ of an integer, Absolute value in $Z$ : $∣ a ∣ \geq 0$ ; $∣ a ∣ = 0$ exactly when $a = 0$ ; $∣ - a ∣ = ∣ a ∣$ ; $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ ; $- ∣ a ∣ \leq a \leq ∣ a ∣$ ; and $∣ a ∣ \leq c$ exactly when $- c \leq a \leq c$ ).

[L5]

$Z$ is a commutative ring; its order is total, antisymmetric and transitive, is compatible with addition, and positives are closed under multiplication (The integers form a commutative ring, Arithmetic on the integers, The integers as equivalence classes of pairs of naturals, The integers form a totally ordered ring, Order on the integers, The integers have no zero divisors; multiplicative cancellation).

[L6]

$ι : N \to Z$ is injective and order preserving with image the nonnegative integers, $ι (0) = 0$ , $ι (1) = 1$ (The naturals embed in the integers); $m < k$ exactly when $σ (m) \leq k$ , and $1 = σ (0)$ (Discreteness: $σ (n)$ is the immediate successor, The natural numbers $N$ (von Neumann), Order on the natural numbers).

Verification

technique · direct

1.1

$0 < 1$ , and every integer $y > 0$ satisfies $y \geq 1$ : $y = ι (t)$ with $t \neq 0$ , so $1 = σ (0) \leq t$ and $ι$ preserves the order. Consequently $y > c$ implies $y \geq c + 1$ for all integers $y, c$ , by applying this to $y - c$ .

L5L6

1.2

Monotonicity of squaring and cubing on the nonnegative integers: if $0 \leq u \leq w$ then $u^{2} \leq w^{2}$ and $u^{3} \leq w^{3}$ , since $w^{2} - u^{2} = (w - u) (w + u)$ and $w^{3} - u^{3} = (w - u) (w^{2} + w u + u^{2})$ have both factors nonnegative.

L3L5

1.3

Suppose $x \in Q$ has $x^{2} = j (3)$ . By [L1] with $k = 2 \geq 1$ we get $x = j (z)$ for some $z \in Z$ ; then $j (z^{2}) = j (z)^{2} = j (3)$ , so $z^{2} = 3$ by injectivity of $j$ .

L1L2L3

2.1

Now $∣ z ∣^{2} = ∣ z^{2} ∣ = ∣ 3 ∣ = 3$ , and $∣ z ∣ \geq 0$ . If $∣ z ∣ = 0$ then $∣ z ∣^{2} = 0 \neq 3$ ; if $∣ z ∣ = 1$ then $∣ z ∣^{2} = 1 \neq 3$ ; and if $∣ z ∣ \geq 2$ then $∣ z ∣^{2} \geq 2^{2} = 4 > 3$ by step 1.2. Since $∣ z ∣ \geq 0$ and $∣ z ∣ \neq 0$ force $∣ z ∣ \geq 1$ , and $∣ z ∣ \neq 1$ forces $∣ z ∣ \geq 2$ , no value remains, so no such $x$ exists.

step 1.1step 1.2step 1.3L4L5

2.2

Suppose $x^{2} = j (6)$ . As in step 1.3, $x = j (z)$ with $z^{2} = 6$ , so $∣ z ∣^{2} = 6$ . Now $0^{2} = 0$ , $1^{2} = 1$ , $2^{2} = 4$ , and $∣ z ∣ \geq 3$ gives $∣ z ∣^{2} \geq 9 > 6$ ; none of $0$ , $1$ , $4$ is $6$ , and the four ranges are exhaustive by step 1.1. So no such $x$ exists.

step 1.1step 1.2step 1.3L1L2L3L4L5

2.3

Suppose $x^{3} = j (2)$ . As before $x = j (z)$ with $z^{3} = 2$ . If $z \leq 0$ then $z^{3} \leq 0 < 2$ , since $z^{3} = z \cdot z \cdot z$ is a product of three nonpositive factors and is therefore nonpositive. So $z \geq 1$ ; and $1^{3} = 1 \neq 2$ , while $z \geq 2$ gives $z^{3} \geq 2^{3} = 8 > 2$ by step 1.2. No value remains, so no such $x$ exists.

step 1.1step 1.2step 1.3L1L2L3L5

3.1

The three claims are established.

step 2.1step 2.2step 2.3∎

Remarks

A fourth instance was already in the library, proved differently. The published FALSE: some rational number squares to 2 refutes "some rational number squares to $2$ " on the construction pages, by parity alone and long before primes were available here. The case $k = 2$ , $m = 2$ of A rational root of $x^{k} = m$ is an integer: if $k \geq 1$ , $m \in Z$ , $x \in Q$ and $x^{k}$ is the image of $m$ , then $x$ is the image of an integer gives the same conclusion from Euclid's lemma instead, and the two agree.
Nothing here asserts that a real square root of $3$ exists. The statement is entirely about $Q$ : no rational squares to $3$ . That $R$ contains such a number is a separate fact, proved elsewhere in the library from completeness, and it is not used or needed above.
The size argument is the whole of the remaining work. Once the corollary has reduced the question to integers, each case is a finite check, because squaring and cubing are monotone on the nonnegative integers and the candidate values overshoot immediately.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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

Rational root theorem (Wikipedia) (standard reference, not scraped)
Square root of 2 (Wikipedia) (standard reference, not scraped)
Wichita State University notes: Logic and proofs (standard reference, not scraped)
Michigan State University Math 310 course notes (standard reference, not scraped)
University of Minnesota Duluth number theory solutions (standard reference, not scraped)

No rational squares to 33 or to 66, and none cubes to 22: three instances of the rational-root corollary