LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

Square root of two divisibility criterion in the eighth cyclotomic ring

Statement

For $x = a + b ω + c ω^{2} + d ω^{3} \in O$ , multiplication by $\sqrt{2} = ω - ω^{3}$ has coefficient vector $(b - d, a + c, b + d, c - a)$ . Consequently $\sqrt{2}$ divides $x$ in $O$ exactly when $a \equiv c$ and $b \equiv d (m o d 2)$ . Also,

$x \overset{ˉ}{x} = P + \sqrt{2} Q, P = a^{2} + b^{2} + c^{2} + d^{2}, Q = a (b - d) + c (b + d),$

and $2$ divides $x \overset{ˉ}{x}$ in $O$ exactly when $\sqrt{2}$ divides $x$ .

Facts & Assumptions

Given: $O = Z [ω]$ , $ω^{4} = - 1$ , and $\overset{ˉ}{ω} = ω^{- 1} = - ω^{3}$ .

[F1]

Dyadic cyclotomic ring for Clifford+T synthesis: $O = Z [ω]$ and $ω^{4} = - 1$ ; the power-basis coefficients are unique.

Proof

1.1F1givenalgebra

Multiplying $(ω - ω^{3}) (a + b ω + c ω^{2} + d ω^{3})$ and reducing every power $ω^{j}$ with $ω^{4} = - 1$ gives $(b - d) + (a + c) ω + (b + d) ω^{2} + (c - a) ω^{3}$ . By [F1], this product is in $2 O$ exactly when all four displayed coefficients are even, which is equivalent to $a + c$ and $b + d$ even, or $a \equiv c$ and $b \equiv d (m o d 2)$ . This proves the first criterion.

2.1F1step 1.1algebra∎

Expanding $x \overset{ˉ}{x}$ with $\overset{ˉ}{ω} = - ω^{3}$ and reducing powers gives the stated $P + \sqrt{2} Q$ . Write $A = a + c$ and $B = b + d$ modulo $2$ . Then $P \equiv A + B$ and $Q \equiv A B (m o d 2)$ . The pair $(A + B, A B)$ is $(0, 0)$ exactly for $(A, B) = (0, 0)$ : the other three pairs give $(0, 1)$ , $(1, 0)$ , or $(1, 0)$ . Since $P + \sqrt{2} Q$ is in $2 O$ exactly when its unique power-basis coefficients are all even, equivalently when $P, Q$ are both even, the norm is in $2 O$ exactly when $A = B = 0$ , which by step 1.1 is exactly when $\sqrt{2}$ divides $x$ .

Remarks

Here divisibility means divisibility by an element of $O$ : $u ∣ v$ iff $v = u w$ for some $w \in O$ . The parity criterion is coefficient arithmetic, not an ideal-factorization assertion.

Depends on

Dyadic cyclotomic ring for Clifford+T synthesis

Used by

Dependency tree · two levels

3 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

Kliuchnikov, Maslov, and Mosca, Practical approximation of single-qubit unitaries by single-qubit quantum circuits (standard reference, not scraped)