feat(Computability): add quantum computing foundations

[exAClior]

Closes #688

Adds foundational types for pure-state unitary quantum computing under Cslib/Computability/Quantum/:

File	Key definitions
Register.lean	Register (finite basis with Fintype + DecidableEq), Qubits n, Register.prod
State.lean	StateVector R, PureState R (unit-norm), PureState.ket (|x⟩); extensionality & norm lemmas
Gate.lean	HilbertOperator R, Gate R (matrix + unitarity proof), apply/evolve, ofPerm, Monoid instance; inner-product/norm preservation, simp lemmas

Pure states + unitary gates = the standard quantum circuit model for closed systems. This is the minimal core for follow-up PRs (tensor products, standard gates, measurement, algorithms).

Discussion: #CSLib > Developing quantum algorithms in CSLib

Design decisions

• Pure states over density matrices — standard for algorithms; complements Physlib without depending on it.
• Abstract Register index — parametric over any finite basis (qubits, qutrits, etc.).
• Gate bundles matrix + unitarity proof — enforced by construction, open gate set.
• Mathlib only — no external quantum libraries.

AI Disclosure

Claude assisted with documentation drafting and style review. All Lean definitions, theorems, and proofs are human-authored.

Checklist

• lake build --wfail --iofail
• lake exe mk_all --lib Cslib --module --check
• lake test / lake lint / lake exe lint-style
• All files import Cslib.Init, have copyright headers and docstrings

[chatgpt-codex-connector]

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: af1eb55e5a

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

[chatgpt-codex-connector]

Preserve the requested permutation direction

For non-involutive permutations this matrix implements the inverse action on basis states: the theorem below proves (ofPerm sigma).apply (PureState.ket x) = PureState.ket (sigma⁻¹ x). A caller passing a 3-cycle expecting |0⟩ to move to |1⟩ instead gets the predecessor basis state, and the smoke test misses this because bit-flip is self-inverse. Use the inverse permutation matrix here, or make the API/documentation explicitly expose the inverse convention.

Useful? React with 👍 / 👎.