The semantic check

Part G, lesson G7. You need lessons G1 to G6, and lesson F1.

Lesson F1 proved that the Bell certificate holds: where every ion is, cycle by cycle, and that every gate's ions are together in a trap that can gate. It ended on what that proof does not say: which gate the pulses make. That is the semantic half of the verdict called R10, and the semantic check, check_cert, computes it. This lesson proves it, for the Bell certificate: it reads the witnesses' pulses, composes them into the exact 4×4 unitary, and proves it equal to the circuit's up to a global phase. Then it takes the one mutation of Part F's suite that the proved checker accepts, finds the bug it stands for in the pulses, and refuses that.

*Lessons F1 and G1 to G6 are restated, unseen, above this line: the certificate bell, the numbers and matrices, the pulses R, VZ, MS (angles in eighths of a turn), kron, H, CX, entry, UpToPhase, and lesson G4's not_phase_of_zero.*

1. The certificate

Here is lesson F1's Bell certificate again, in the studio. The checker's rows are its conditions on the move and on the two witnesses: the Hadamard's at cycle 2 in C1, the CNOT's at cycle 8 in C0. Nothing in those rows says Hadamard or CNOT.

2. Reading the pulses

The certificate file bell.qcert.json carries, beside each witness, the pulses the compiler emitted for it ("the native sequence, from Gateset", says the certificate writer), in time order, as text. The checker's input (bell.qcheck.json, the Input above) does not carry them, and Lean's checker never reads them:

The trusted step. The compiler prints each angle to six significant figures (%.6g). 1.5708 is not π/2; it is the six-digit decimal nearest to it. To turn the text into pulses on the grid, this lesson rounds each angle to the nearest whole number of eighths of a turn, so 1.5708 becomes 2 (π/2) and 3.14159 becomes 4 (π). That rounding is trusted, not proved: Lean's core has no π to prove anything about, and nothing below could tell a pulse of 1.5708 radians from one of π/2. check_cert takes the same step its own way: it reads the angles from the programme, where they are the double-precision numbers (1.5707963267948966 in the Bell programme), and its tableau route accepts an angle as a multiple of π/2 when it is one to within 10⁻⁹ (is_right_angle). It also reads the instructions, not the certificate's copy of them; for this certificate the seven pulses are the same, in the same order (instructions 2, 3 and 5 to 9 of the programme), which is one more thing this lesson takes from the file rather than proves. The ions become qubits through the certificate's own map, bell.qmap.

A pulse on qubits, and the reading: written in Lean, run by #eval, which proves nothing.

From here on, the pulses are these values, and everything is proved about them:

3. The programme's unitary

check_cert's program_unitary starts from the identity and, for each pulse in time order, left-multiplies by that pulse on its qubits, through its helper apply_gate:

def apply_gate(U: np.ndarray, g: np.ndarray, qubits: list[int], n: int) -> np.ndarray:
    """Left-multiply `U` by `g` acting on `qubits`.

    Done by reshaping the row index into `n` qubit axes and contracting, which costs
    O(2^n · 2^n) per gate instead of the O(8^n) a dense matrix product would.
    Qubit 0 is the most significant bit.
    """

Ours does the same on two qubits. on q g U is kron g 1 * U for q = 0 and kron 1 g * U for q = 1, computed row pair by row pair without forming the 4×4. An MS acts on both qubits, and on (q1, q0) it is the same matrix as on (q0, q1), since X⊗X is symmetric.

Exercise 1 ★ on_is_kron open

Check on against lesson G2's kron on the Hadamard's pulses, on both qubits.

Exercise 2 ★ h_witness_unitary open

Prove the Hadamard witness's pulses make H on qubit 0, exactly (lesson G3).

Exercise 3 ★ cx_witness_unitary open

Prove the CNOT witness's pulses make e^(iπ/4)·CX (lesson G4).

4. The circuit's unitary, and the comparison

The circuit is h q[0]; cx q[0],q[1]; and two measurements. Both measurements are the last thing done to their qubit, in the circuit and in the programme, so readout_plan defers neither (lesson G6), and the comparison is over the two qubits alone: the circuit's unitary is the Hadamard on qubit 0, then the CNOT. check_cert reads the circuit's gates from the QASM through qiskit's own definitions (source_unitary); ours are the matrices of lessons G3 and G4.

Exercise 4 ★★ bell_semantic open

The theorem check_cert only computes, for this certificate: the programme's pulses implement the circuit, up to a global phase. Name the phase.

check_cert itself decides this certificate by the tableau route (its verdict on the Compilation page: "stabilizer tableau, composed from the emitted pulses, against the source QASM"), which lesson G5 proved. The full matrix is its route outside the Clifford fragment, for up to --max-unitary-qubits (default 10) qubits; it is the stronger comparison, since it sees every amplitude.

5. The mutant the proved checker accepts, and the bug behind it

Part F's mutation suite (mutate_cert, lesson F5) seeds defects into accepted certificates and requires each refused. One of them it expects the proved checker to accept:

`swap_operands` exchanges the two ions of a gate.  The Lean checker verifies that a
witness names its op's own ions, in any order (`OwnIons`), and that they are
**co-located** in one gate-capable trap; swapping them changes neither, so it passes,
correctly, because O1 does not claim to see operand *order*.  A CX is not symmetric, so
the swap is a real bug

Exercise 5 ★ swapped_accepted open

Prove that Part F's checker accepts the Bell certificate with the CNOT's witness written q1, q0.

Lesson F5 explains why that is right: a witness names the ions an operation ran on, never which one is the control, and OwnIons compares them as a rearrangement, so the order of a witness's ions carries no meaning. The bug the mutation stands for is real all the same, and it lives in the pulses: a CNOT with its control and target exchanged. A compiler with that bug emits decompose_cx with q1 as the control, so the single-ion pulses move to the other ion; the witnesses need not change at all, and the proved checker, which never reads a pulse, cannot tell. The Compilation page's swap certificate has exactly this sequence, as the second of its three CNOTs: "R(1.5708,1.5708)@q1","MS(1.5708)@q1,q0","R(-1.5708,0)@q1","R(-1.5708,0)@q0","R(-1.5708,1.5708)@q1".

Exercise 6 ★★ swapped_refused open

Prove the semantic check refuses a programme with those pulses for its CNOT: no phase takes it to the circuit. From |00⟩ the circuit reaches |11⟩ (entry (3, 0)) and the swapped programme does not: apply not_phase_of_zero there.

That is the reason R10 has two halves. Neither sees what the other does: the proved checker never reads a pulse, and the semantic check never asks where an ion is. Lesson F5 ran this bug through check_cert on the published Bell programme: accepted by the proved checker, refused by the tableau. Exercise 6 is that refusal, proved.

6. The check as a program

check_cert's comparison is a procedure that answers yes or no (same_up_to_phase). Here is one for our numbers: try the eight phases ω⁰ .. ω⁷. Like Part F's check, it is worth having only with a theorem that its yes means the specification holds.

Exercise 7 ★★★ samePhase_sound open

Prove it: if samePhase A B is true, then UpToPhase A B, for every pair of matrices. Hints: List.any_eq_true turns the any into an ∃ k ∈ List.range 8; List.mem_range gives k < 8; beq_iff_eq turns == into =; and the eight phases have size one by a finite check, key.

Exercise 8 ★★ bell_semantic_by_check open

Prove bell_semantic again, without naming the phase: run the check, and apply its soundness.

7. What is proved, and what is trusted

For the Bell certificate, this Part has proved what check_cert computes: the pulses the witnesses carry make the circuit, exactly, up to the phase e^(−iπ/4) (Exercise 4); with lesson F1, both halves of R10 are proved for this certificate, up to the steps the table marks. What remains trusted or computed, and where:

The last row is why this lesson is about one certificate: the kernel composes a 4×4 matrix in seconds, but the Compilation page's larger examples and the boards' rounds are far beyond a matrix, and there the comparison stays stim's.