Exact numbers

Part G, lesson G1. Part G assumes Parts E and F; you need at least lesson F1, whose last section this Part takes up.

Lesson F1 ended on a gap. The proved checker names no gate: a witness says an operation happened here, now, on these ions, never which gate the laser pulses make. That second question is answered by the semantic check, check_cert. It reads the native pulses out of the emitted programme, composes them, and compares the result with the source circuit: with the stabilizer library stim for a Clifford circuit, and otherwise, up to ten qubits by default, with the full matrix in floating point, equal when every entry agrees to within 10⁻⁸ up to one global phase (same_up_to_phase). It is computed, not proved.

Part G does that comparison in Lean, as a proof. The objects are matrices: a pulse on one ion is a 2×2 matrix of complex numbers, the entangling pulse on two ions a 4×4 one, and their entries are numbers like cos(π/4) and e^(iπ/4). The compiler's own pulse identities are proved in Lean with Mathlib, whose real and complex numbers make that easy (the modules QCCDC.Pulse.Native and QCCDC.Pulse.Decompose). This page has Lean's core only, which has whole numbers and no real numbers at all. So this lesson builds, out of Int, exactly the numbers the pulses need, and makes equality between them something Lean's kernel can decide.

1. Which numbers

For a circuit of Clifford+T gates (h, s, t, x, cx, cz, swap, ccx and their relatives) every angle the compiler writes into a pulse is a whole multiple of π/4; lessons G3 and G4 show where each one comes from. On that grid every phase is a power of

ω = e^(iπ/4) = (1 + i)/√2,

and every sine and cosine is one of 0, ±1, ±√2/2. Add and multiply such numbers and you never leave the set of numbers

(a + b·i + (c + d·i)·√2) / 2^k, a, b, c, d whole numbers, k ≥ 0,

because i·i = -1 and √2·√2 = 2 turn every product back into that shape. This set is a ring; its usual name is ℤ[ω, ½]. Here is one of its numbers as a Lean record. A structure with deriving DecidableEq also gets, written by Lean, the program that decides whether two records are equal field by field.

2. One spelling per number

The same number has many spellings: one half is ⟨1, 0, 0, 0, 1⟩ and also ⟨2, 0, 0, 0, 2⟩. Two records are equal only when every field is, so as records those two differ. To make equality of records the same thing as equality of numbers, we keep exactly one spelling per number, the one with the smallest power of two: while k > 0 and all four of a, b, c, d are even, halve them and lower k.

When that stops, either k = 0 or one coefficient is odd, and no spelling of the number has a smaller k. The reason is one fact about the four numbers 1, i, √2 and i√2: no whole-number combination of them is 0 unless every coefficient is 0 (√2 is irrational and i is not real). So for each k a number has at most one spelling, and halving all four is the only way to lower k.

norm k a b c d is that normal form. It is defined by pattern matching on k, one equation for 0 and one for k + 1; each call lowers k, so Lean accepts that it stops. A namespace groups names: inside namespace Zω, norm is Zω.norm.

3. Arithmetic

To add, bring both numbers to the larger power of two and add the coefficients. To multiply, write each number as g + h·√2 with g = a + b·i and h = c + d·i; then

(g + h√2)(g' + h'√2) = (g·g' + 2·h·h') + (g·h' + h·g')·√2,

and multiplying out the Gaussian products gives the four lines of mul; the powers of two add. Negation flips every sign. The complex conjugate flips the sign of i, which leaves √2 alone. Every operation that can produce an even spelling ends in norm, so every number they build is in normal form.

An instance tells Lean what +, *, -, ^ and the numerals 0, 1, 2, ... mean on Zω. A numeral n is the whole number n: ⟨n, 0, 0, 0, 0⟩, already in normal form.

So that #eval shows a number the way you would write it, here is a printer. It is for your eyes only: no proof below uses it.

4. Computing, and deciding

#eval computes and shows the answer. It proves nothing.

The last line is one half spelled badly; adding 0 ran it through norm.

A proof that two numbers are equal is a computation too. decide +kernel (lesson F1) has Lean's kernel run the equality test that deriving DecidableEq wrote, on the normal forms the operations produce, and accept the statement only if the answer is true. No floating point, no tolerance: equal means equal.

Exercise 1 ★ sqrt2_mul_sqrt2 open

Prove √2 · √2 = 2.

Exercise 2 ★ omega_sq open

Prove ω² = i: two eighths of a turn are a quarter turn.

Exercise 3 ★ omega_pow_eight open

Prove ω⁸ = 1: eight eighths of a turn are a whole turn.

Exercise 4 ★ gauss_div_sqrt2 open

Prove (1 + i)/√2 = ω, dividing by √2 as multiplying by invSqrt2.

Exercise 5 ★ two_spellings open

Prove both halves: the normal form of 2/2 is 1, and the badly spelled record ⟨2, 0, 0, 0, 1⟩ is not equal to 1 as a record. That second half is why every operation ends in norm: a record you write by hand is trusted to be in normal form, and these lessons only write ones that are.

5. Angles on the grid

An angle n·π/4 is stored as the whole number n. Its phase e^(inπ/4) is ω^n, and since ω⁸ = 1 only n mod 8 matters. cis n (for cos + i sin) looks the phase up in a table of the eight powers, written in normal form. Lean's % on Int is the remainder in 0 .. 7 here, also for negative n, and toNat turns it into a Nat for the table.

A table is a claim; check it.

Exercise 6 ★ cis_is_power open

Prove that the table is the powers of ω: for each of the eight n, cis n = ω ^ n. Over Fin 8 (the numbers below 8) a ∀ is eight cases, and decide +kernel runs them all.

The remaining exercises of this section are about every angle, not eight of them. omega is a tactic that proves statements of linear arithmetic over Int and Nat, including % and / by a fixed number: here, facts like (n + 8) % 8 = n % 8.

Exercise 7 ★★ cis_periodic open

Prove that a whole turn changes nothing. Unfold cis, then rewrite the remainder with a fact omega proves: rw [show (n + 8) % 8 = n % 8 by omega].

Exercise 8 ★★ cis_neg open

Prove e^(-inπ/4) is the conjugate of e^(inπ/4), for every n. Hint: first prove the table fact for the eight remainders (key, by decide +kernel); then unfold cis, apply key to the remainder of n, and let omega show the two indices agree. congr 1 reduces f x = f y to x = y.

Exercise 9 ★★★ cis_add open

Prove that phases add, e^(iaπ/4)·e^(ibπ/4) = e^(i(a+b)π/4), for every pair of whole numbers. Same method: a table fact for the 64 pairs of remainders, then omega to show that the remainder of a + b is the remainder of the sum of the remainders.

6. A fact about every number

Lessons G4 and G7 refute claims of the form these two matrices differ only by a phase c, for a c nobody names. They need one fact that holds for every record c, normal or not: c · 0 = 0. It is not a computation, because c is unknown; it is a proof by induction.

Exercise 10 ★★★ mul_zero_right open

First prove norm_zero: the normal form of 0/2^k is the zero record, by induction on k (simp [Zω.norm, ih] does the step: the four remainders are 0, and 0/2 = 0). show restates the goal with 0 spelled as its record, so that simp can see its fields; simp [mul] then turns the product into norm x.k 0 0 0 0, since every term is a coefficient of x times 0.

7. What this lesson built

A number of ℤ[ω, ½] is a record of four whole numbers and a power of two, kept in its one normal form, so that = is decided by comparing fields; decide +kernel has the kernel do that, and is a proof. Phases on the π/4 grid are a table of eight numbers, checked against the powers of ω. Lesson G2 builds the native pulses out of them, as matrices, and compares them entry by entry with the definitions the compiler's proofs use.