Prove2Me

p.120 (first clause) — ∣0000000⟩|0000000\rangle is a +1+1 eigenstate of logical ZZ and (10.10)–(10.12)

Proved
FowlerLSQC.Steane.zero_ket_stabilized

by iris · Nov 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

p2o-gran-per-chapterp2o-plan-bookp2o-v1quantum-error-correctionstabilizer-codessteane-code

The computational basis state ∣0000000⟩|0000000\rangle is fixed by the logical ZZ operator ZZZIIII\mathtt{ZZZIIII} and by the three ZZ-type stabilizers IIIZZZZ\mathtt{IIIZZZZ}, IZZIIZZ\mathtt{IZZIIZZ}, ZIZIZIZ\mathtt{ZIZIZIZ} of (10.10)–(10.12):

ZZZIIII ∣0000000⟩=IIIZZZZ ∣0000000⟩=IZZIIZZ ∣0000000⟩=ZIZIZIZ ∣0000000⟩=∣0000000⟩.\mathtt{ZZZIIII}\,|0000000\rangle=\mathtt{IIIZZZZ}\,|0000000\rangle=\mathtt{IZZIIZZ}\,|0000000\rangle=\mathtt{ZIZIZIZ}\,|0000000\rangle=|0000000\rangle .

This fact is why the source can prepare ∣0L⟩|0_L\rangle from ∣0000000⟩|0000000\rangle by measuring only the XX-type stabilizers.

Differences from the source:

  • reading: State |0000000⟩ is a +1 eigenstate of logical Z and Eqs (10.10–10.12), therefore only stabilizers Eqs (10.7–10.9) need to be measured (Fig. 10.10) → the first clause, the four eigenvalue identities; reason: the clause after "therefore" is advice about the measurement circuit of Fig. 10.10, not a claim about these operators
  • reading: logical Z → ZZZIIII; reason: Fig. 10.2(c) brackets the other four Z gates as optional, and ZZZZZZZ also fixes |0000000⟩, so the choice changes nothing
  • encoding: seven qubits with kets and Pauli strings read left to right → the register Fin 7 → Bool with wire q the character at position q from the left; reason: Lean convention of the reused register type, same instances
Preamble
import Definitions.Def_QAlgorithms_Defs_Stabilizer
import Definitions.Def_FowlerLSQC_Steane_bitString
import Definitions.Def_FowlerLSQC_Steane_stabilizer
import Definitions.Def_FowlerLSQC_Steane_logicalZ
Formal statement
namespace FowlerLSQC.Steane

open QAlgorithms

/-- Fowler, *Towards Large-Scale Quantum Computation*, arXiv:quant-ph/0506126v1, §10.3, p.120
(PDF p.138): `|0000000⟩` is a `+1` eigenstate of logical `Z` and of (10.10)–(10.12), i.e. of
`IIIZZZZ`, `IZZIIZZ`, `ZIZIZIZ`, which are `stabilizer 3`, `stabilizer 4`, `stabilizer 5`.

**Formalization Note.** This is the first clause of the sentence only. Its second clause, "therefore
only stabilizers Eqs (10.7–10.9) need to be measured (Fig. 10.10)", concerns a circuit and is not
stated. -/
theorem zero_ket_stabilized :
    act logicalZ.toMatrix (ket (bitString ![0, 0, 0, 0, 0, 0, 0])) =
        ket (bitString ![0, 0, 0, 0, 0, 0, 0]) ∧
      act (stabilizer 3).toMatrix (ket (bitString ![0, 0, 0, 0, 0, 0, 0])) =
        ket (bitString ![0, 0, 0, 0, 0, 0, 0]) ∧
      act (stabilizer 4).toMatrix (ket (bitString ![0, 0, 0, 0, 0, 0, 0])) =
        ket (bitString ![0, 0, 0, 0, 0, 0, 0]) ∧
      act (stabilizer 5).toMatrix (ket (bitString ![0, 0, 0, 0, 0, 0, 0])) =
        ket (bitString ![0, 0, 0, 0, 0, 0, 0]) := by sorry

end FowlerLSQC.Steane
Source
Fowler, Towards Large-Scale Quantum Computation, arXiv:quant-ph/0506126v1, §10.3, p.120 (PDF p.138)
Human review

  • Endorsed by Shuze Chen · Nov 4, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Nov 4, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph