Alphabeta Math
DefinitionDefinition: 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.

Clifford normalizer

Definition

Work with actual unitary matrices, not equivalence classes modulo global phase. The n-qubit Clifford normalizer is

Cn:={U unitary on Hn:UPnU∗=Pn}.

It is a group under matrix multiplication. Every scalar unitary λI with ∣λ∣=1 belongs to Cn and has the same conjugation action as I; the chosen convention retains these distinct matrices.

Facts & Assumptions

Given: the finite-dimensional inner-product space Hn and the phase-aware Pauli group Pn.

[F1]

Pauli product and adjoint: Pn is a group under matrix multiplication.

[F2]

Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces: a unitary operator is an invertible linear isometry and its inverse is its adjoint.

Proof

1.1givenF1algebra

The identity conjugates Pn to itself. If U,V∈Cn, then (UV)Pn(UV)∗=U(VPnV∗)U∗=UPnU∗=Pn, so UV∈Cn.

2.1givenF1F2step 1.1algebra∎

If UPnU∗=Pn, multiplying this equality by U∗ on the left and U on the right gives U∗PnU=Pn, so U∗∈Cn by [F2]. Thus the set is a group. For ∣λ∣=1, (λI)P(λI)∗=P for every P, and conjugation by λU equals conjugation by U.

Depends on

Used by

Dependency tree · two levels

16 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