Symplectic Pauli: Formalizing the Symplectic Basis Theorem in Agda

A complete Agda formalization of the mathematical structures underlying the CHP (CNOT-Hardmard-Phase) quantum circuit simulator, based on the insight that the CHP algorithm is a computational realization of the Symplectic Basis Theorem.

Status: All modules compile with zero warnings. Basic algebraic structures proven; Symplectic Basis Theorem inductive step fully proven (modulo standard geometric postulates).

Overview

This project translates the mathematical hierarchy from the Haskell symplectic-chp package into Agda, enabling formal proofs of the theorems that underpin stabilizer quantum computation.

Mathematical Foundation

The key insight is that the n-qubit Pauli group modulo phases is isomorphic to the symplectic vector space $(\mathbb{F}_2^{2n}, \omega)$, where:

$$\omega((x_1|z_1), (x_2|z_2)) = x_1 \cdot z_2 + z_1 \cdot x_2 \pmod{2}$$

This symplectic form encodes commutation relations:

• $\omega(v, w) = 0$ ⟺ Pauli operators commute
• $\omega(v, w) = 1$ ⟺ Pauli operators anticommute

Module Structure

src/
├── Field.agda            -- Field F_2 (the field with two elements)
├── Vector.agda           -- Vector space F_2^n
├── Symplectic.agda       -- Symplectic vector spaces, isotropic/Lagrangian subspaces
│                         -- and the Symplectic Basis Theorem (inductive framework)
├── Pauli.agda            -- The Pauli group and its symplectic structure
├── Tableau.agda          -- CHP Tableau as a Symplectic Basis
├── SymplecticCHP.agda    -- Main module with complete picture
├── Examples.agda         -- Verified concrete examples
└── CircuitExamples.agda  -- Verified proofs for all circuit-example/ circuits

Key Theorems

1. Symplectic Basis Theorem

symplecticBasisTheorem : ∀ {n} (S : SymplecticSpace n) → SymplecticBasis S

Theorem: Every symplectic vector space $(V, \omega)$ with $\dim(V) = 2n$ admits a basis ${e_1, \ldots, e_n, f_1, \ldots, f_n}$ such that:

• $\omega(e_i, e_j) = 0$ (e's span a Lagrangian)
• $\omega(f_i, f_j) = 0$ (f's span a Lagrangian)
• $\omega(e_i, f_j) = \delta_{ij}$ (duality)

Status:

• ✅ Base case (n=0): Proven with empty bases
• ✅ Inductive step: Fully proven
  • ✅ Standard basis vector properties (ω(eᵢ,fⱼ)=δᵢⱼ, isotropy)
  • ✅ v ≠ 0 proof for inductive step
  • ✅ Complete isotropy proofs for e-basis and f-basis
  • ✅ Complete duality proof
  • ⚠️ Geometric constructions postulated (symplectic partner, complement)

The proof proceeds by induction on n:

• Base case (n=0): Trivially satisfied with empty bases
• Inductive step:
  1. Choose v = e₀ (first standard basis vector), prove v ≠ 0
  2. Find symplectic partner w with ω(v,w) = 1
  3. Construct symplectic complement W^ω
  4. Apply induction to W^ω, lift basis via embedding
  5. Prove isotropy and duality using orthogonality conditions

2. Fundamental Correspondence

fundamental-theorem : ∀ {n} (p₁ p₂ : Pauli n) → 
  commute p₁ p₂ ≡ true ↔ ω-Pauli p₁ p₂ ≡ 0#

Theorem: For Pauli operators $P, Q$: $[P, Q] = I$ ⟺ $\omega(P, Q) = 0$

This connects group-theoretic commutation with the geometric symplectic form.

3. Tableau as Symplectic Basis

record Tableau (n : ℕ) : Set where
  field
    S : Vec (Pauli n) n  -- Stabilizers (first Lagrangian)
    D : Vec (Pauli n) n  -- Destabilizers (second Lagrangian)
    
    -- Conditions from Symplectic Basis Theorem:
    S-commute : ∀ i j → commute (S i) (S j) ≡ true
    D-commute : ∀ i j → commute (D i) (D j) ≡ true
    duality   : ∀ i j → ω(Dᵢ, Sⱼ) = δᵢⱼ

Theorem: The CHP Tableau IS a Symplectic Basis.

4. Verified Circuit Examples

All 10 circuits in circuit-example/ have been mechanically verified in src/CircuitExamples.agda. Each proof chains evolveTableau and measure (or measureWithRandom) and confirms the expected quantum behavior with refl.

Circuit	Type	Verified Property
single-hadamard	Deterministic	`H
multi-target	Deterministic	`H^{⊗3}
stabilizer-cycle	Deterministic	HSSH = X, so MZ = -1
swap-gate	Deterministic	X₁; SWAP(0,1) maps `
bell-state	Random	50/50 correlated Z measurements
ghz-state	Random	50/50 all-equal Z measurements
cz-gate	Random	25/25/25/25 MX measurements
phase-gate	Random	HSS = HZ, random Z measurement
y-measurement	Random	HSHS prepares `
unsupported-rx	Unsupported	RX has no constructor in Gate

Example proof (single-hadamard):

tab = evolveTableau (Local (H zero)) (emptyTableau 1)
result = measure tab (X zero)
outcomeCorrect : proj₂ result ≡ Determinate false  -- corresponds to +1
outcomeCorrect = refl

This demonstrates applying our verified theorems to CHP circuit validation: every stabilizer, destabilizer, and measurement outcome is proven correct at compile time.

Mathematical-Computational Dictionary

Mathematics	Agda Type	Computational Role
Field $\mathbb{F}_2$	Field.𝔽₂	Boolean values
Vector space $\mathbb{F}_2^n$	Vector.Vector n	Bit vectors
Symplectic form $\omega$	Symplectic.ω	Commutation check
Isotropic subspace	Symplectic.Isotropic	Commuting Pauli set
Lagrangian subspace	Symplectic.Lagrangian	Maximal commuting set
Symplectic Basis	Symplectic.SymplecticBasis	Theorem structure
Pauli group $\mathcal{P}_n$	Pauli.Pauli n	Quantum operators
CHP Tableau	Tableau.Tableau n	Stabilizer state

Comparison with Haskell Implementation

The Haskell symplectic-chp package uses type classes to encode mathematical structures:

class SymplecticVectorSpace v where
  omega :: v -> v -> Field v

class SymplecticBasisTheorem s n v where
  firstLagrangian  :: s n v -> Lagrangian n v
  secondLagrangian :: s n v -> Lagrangian n v
  verifyDuality    :: s n v -> Bool

In Agda, we use dependent records with proofs:

record SymplecticBasis {n} (S : SymplecticSpace n) : Set where
  field
    e-basis : Vec (VecS S) n
    e-isotropic : ∀ i j → ω S (e-basis i) (e-basis j) ≡ 0#
    f-basis : Vec (VecS S) n
    f-isotropic : ∀ i j → ω S (f-basis i) (f-basis j) ≡ 0#
    duality : ∀ i j → ω S (f-basis i) (e-basis j) ≡ delta i j

Key difference: In Agda, the isotropy and duality conditions are part of the type and must be proven at construction time, whereas Haskell only verifies them at runtime via verifyDuality.

Type Safety Guarantees

Agda's dependent types provide compile-time guarantees that Haskell cannot:

1. Dimensional correctness: Vector n ensures exactly $n$ components
2. Field consistency: Field v ~ 𝔽₂ ensures symplectic form outputs are in $\mathbb{F}_2$
3. Geometric invariants: Isotropy and duality are type-level constraints
4. Termination: All functions must be total (provably terminating)

Running the Code

Prerequisites

• Agda 2.8.0
• agda-stdlib 2.3

These specific versions are required due to syntax changes in the standard library (e.g., replicate now takes explicit arguments, boolean equality uses ≡ᵇ).

Type Checking

make check

or manually:

agda src/SymplecticCHP.agda

This will:

1. Parse all modules
2. Type check all definitions
3. Verify all proofs (goals marked with {!!} are incomplete but accepted)

Emacs Mode

For interactive development:

agda-mode setup

Then open any .agda file in Emacs and use:

• C-c C-l : Load file
• C-c C-, : Goal type
• C-c C-. : Goal type and context
• C-c C-r : Refine (fill goal)
• C-c C-a : Auto-fill goal

Proof Status

Theorem	Status
Field axioms for $\mathbb{F}_2$	✅ Proven
Vector space axioms	✅ Proven
Standard basis vector properties (ω-e-f, ω-e-e, ω-f-f)	✅ Proven
Symplectic Basis Theorem (n=0)	✅ Proven
Symplectic Basis Theorem (inductive step)	✅ Proven (modulo geometric postulates)
Symplectic form bilinearity	⚠️ Postulated (requires vector lemmas)
Symplectic form alternating	⚠️ Postulated
Fundamental Correspondence	⚠️ Postulated
Pauli X/Z properties	⚠️ Postulated
Tableau validity	✅ By construction
CHP Operations (gates, measurement)	✅ Implemented

Current Progress & Future Work

Recently Completed

1. ✅ Helper lemmas for vector manipulation (lookup-basisVec, lookup-replicate-zero)
2. ✅ Standard symplectic basis vector characterizations (x-part-symplecticE, etc.)
3. ✅ Proof that ω(eᵢ, fⱼ) = δᵢⱼ
4. ✅ Proof that e-basis and f-basis are isotropic
5. ✅ Inductive step framework with InductiveStep module
6. ✅ Proof that v = e₀ is non-zero (using component extraction)
7. ✅ Complete proofs for new-e-isotropic, new-f-isotropic, new-duality
8. ✅ Added form-preservation property to symplectic complement
9. ✅ Implemented CHP operations: gate conjugation (H, S, CNOT, CZ, SWAP, X), tableau evolution, measurement algorithm, and runtime validity checker
10. ✅ Circuit example proofs: All 10 circuit-example/ circuits have corresponding verified Agda proofs

Remaining Goals

1. stabilizer and destabilizer duality
2. generalize CHP state into stabilizer code
3. Error correction codes: Formalize surface code, Steane code, etc.

References

1. Aaronson & Gottesman, "Improved Simulation of Stabilizer Circuits," Phys. Rev. A 70, 052328 (2004)
2. Artin, Geometric Algebra (symplectic groups)
3. Gosson, Symplectic Geometry and Quantum Mechanics
4. Nielsen & Chuang, Quantum Computation and Quantum Information
5. Gottesman, Stabilizer Codes and Quantum Error Correction (PhD thesis, 1997)

License

MIT License (same as the original Haskell symplectic-chp package)

Acknowledgments

This formalization is based on the Haskell symplectic-chp package, which demonstrated the elegant connection between symplectic geometry and quantum computation.