ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

$Z [1 / 6]$ consists exactly of rationals $a / 6^{n}$ and inverts precisely the primes $2$ and $3$

Example

Inside $Q$ , $Z [1 / 6] = Z_{6} = {\frac{a}{6^{n}} : a \in Z, n \in N} .$ Among positive prime integers, exactly $2$ and $3$ become units in this ring.

Facts & Assumptions

Given: The principal localisation of $Z$ at $6$ and its canonical map into $Q$ .

[F1]

The principal localisation at $6$ consists of fractions $a / 6^{n}$ (Principal localisation $R_{f} = {1, f, f^{2}, \dots}^{- 1} R$ ).

[F2]

The field $Frac (Z)$ is canonically $Q$ ( $Frac (Z)$ is canonically isomorphic to $Q$ ).

[F3]

For an integer prime $q > 1$ , $q ∣ a b$ implies $q ∣ a$ or $q ∣ b$ (For an integer $p > 1$ : $p$ is prime if and only if, for all integers $a$ and $b$ , $p ∣ a b$ implies $p ∣ a$ or $p ∣ b$ ).

[F4]

A map that sends the chosen denominators to units extends uniquely through the localisation (Universal property of localisation: maps that invert $S$ factor uniquely through $S^{- 1} R$ ).

[F5]

A fraction $a / s$ is zero exactly when some denominator annihilates $a$ (Equality, vanishing, and the kernel of the localisation map).

Verification

technique · direct

1.1

The inclusion $Z ↪ Q$ sends $6$ to a unit, so [F4] gives a map $Z_{6} \to Q$ with $a / 6^{n} \mapsto a / 6^{n}$ . If its image is zero, multiplication by the nonzero element $6^{n}$ in the field $Q$ gives $a = 0$ , and then [F5] makes $a / 6^{n} = 0$ ; hence the map is injective. Its image is exactly the set displayed in [F1].

F1F2F4F5algebra

2.1

The elements $2$ and $3$ are units because $2 (3 / 6) = 1$ and $3 (2 / 6) = 1$ .

step 1.1algebra

3.1

If a positive prime $q$ is a unit, then $q (a / 6^{n}) = 1$ for some $a, n$ , so $q a = 6^{n}$ . The case $n = 0$ is impossible because $q > 1$ . For $n > 0$ , [F3] applied repeatedly to $6^{n} = 2^{n} 3^{n}$ gives $q ∣ 2$ or $q ∣ 3$ , and primality with positivity forces $q = 2$ or $q = 3$ .

F3step 1.1algebra∎

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: 75 results over 20 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

The Stacks Project, Section 10.9: Localization (standard reference, not scraped)

Z[1/6]Z[1/6] consists exactly of rationals a/6na/6n and inverts precisely the primes 22 and 33