Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge 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.

Hadamard conjugation of the Pauli matrices

Statement

For H as defined in Exact one-qubit gates and rotations, HXH=Z,HZH=X,HYH=−Y. Moreover, if ∣+⟩=(∣0⟩+∣1⟩)/2 and ∣−⟩=(∣0⟩−∣1⟩)/2, then H∣0⟩=∣+⟩, H∣1⟩=∣−⟩, and ∣+⟩,∣−⟩ are the +1 and −1 eigenvectors of X, respectively. Thus H sends the computational basis to the X-eigenbasis.

Facts & Assumptions

Given: The ordered computational basis (∣0⟩,∣1⟩) and the matrices H,X,Y,Z.

[F1]

Exact one-qubit gates and rotations: H=2−1/2(111−1).

[F2]

The Pauli matrices: X=(0110), Y=(0−ii0), and Z=(100−1).

[F3]

Pauli matrix algebra and trace identities: X,Y,Z have the products displayed in the Pauli multiplication table.

[F4]

The computational basis is orthonormal: the computational basis (∣0⟩,∣1⟩) is orthonormal.

Proof

1.1F1F2F3algebra

Using [F1] and [F2], direct multiplication gives HXH=12(111−1)(0110)(111−1)=Z, HZH=12(111−1)(100−1)(111−1)=X, and HYH=12(111−1)(0−ii0)(111−1)=−Y. The products agree with the Pauli multiplication table in [F3], including the negative sign.

2.1givenF1F2F4algebra∎

The first column of H in [F1] gives H∣0⟩=(∣0⟩+∣1⟩)/2=∣+⟩, and its second gives H∣1⟩=(∣0⟩−∣1⟩)/2=∣−⟩. By [F2], X∣+⟩=∣+⟩ and X∣−⟩=−∣−⟩. Expanding with [F4] gives ⟨+,+⟩root=12(1+0+0+1)=1, ⟨−,−⟩root=12(1−0−0+1)=1, and ⟨+,−⟩root=12(1−0+0−1)=0. Thus these vectors form the X-eigenbasis.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

19 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