Index plumbing for Fin (2 ^ n) registers (quantum-free)

The big-endian pairing of computational-basis labels used to compose qubit registers, factored out of the quantum framework so it carries no dependency on Gate/PureState.

Main definition

• LeanPool.LeanQuantumAlg.prodEquiv — Fin (2 ^ m) × Fin (2 ^ n) ≃ Fin (2 ^ (m + n)), (x, y) ↦ y + 2 ^ n * x, so the first (lower-qubit-index) factor carries the most significant bits.

Pinned Mathlib API: finProdFinEquiv ((x, y) ↦ y + n * x), finCongr.

def QuantumAlg.prodEquiv {m n : ℕ} : Fin (2 ^ m) × Fin (2 ^ n) ≃ Fin (2 ^ (m + n))

Big-endian pairing of basis labels: (x, y) ↦ y + 2 ^ n * x, so the first (lower-qubit-index) factor carries the most significant bits.

Equations

• QuantumAlg.prodEquiv = finProdFinEquiv.trans (finCongr ⋯)