Alphabeta MathHow 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.
Pauli and Clifford Groups, Binary Symplectic Tableaux — Examples
1 · Prerequisites
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Finite Counting, Factorials and Binomial Coefficients
- Finite-Dimensional Complex Inner-Product Spaces and Matrix Interfaces
- Foundations of the Real Numbers for Analysis
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Hilbert Space Geometry and Riesz Representation
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Pauli and Clifford Groups, Binary Symplectic Tableaux
- Polynomial Rings, the Division Algorithm and Roots
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Pure and Mixed States, Ensembles, and Schmidt Decomposition
- Qubits, Bloch Sphere, Pauli Algebra, and One-Qubit Gates
- Registers, Tensor Products, and Partial Trace
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Roots, Rational Powers, and Classical Inequalities
- Simple Field Extensions and the Construction of the Complex Numbers
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tensor Products of Modules
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Spectral Theorem, Positive Operators and Singular Value Decomposition
- The ZFC Axioms and the Basic Set Constructions
- Vector Spaces, Linear Subspaces, Span and Direct Sums
2 · Summary
The one-qubit example checks the sign convention directly: X and Z have pairing one and anticommute, while Z and −Z share a binary label and retain distinct scalar phases.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
Pauli commutator and binary symplectic sign
Example
For one qubit, the labels of and have symplectic pairing , so the binary form records their anticommutation. The two operators and have the same binary label but different mod- phases.
Facts & Assumptions
Given: one qubit and .
Pauli commutator is symplectic pairing: Pauli commutation is determined by .
The Pauli matrices and Pauli matrix algebra and trace identities: and are the displayed one-qubit matrices and .
Verification
The labels are and . Their pairing is in , so [F1] gives , which also follows by multiplying the matrices in [F2].
The operators and have equal binary label and distinct scalar phases and . Thus the label quotient records commutation but alone does not recover the exact signed Pauli.