auto-task(conj_isCompletelyPositive): reuse congruence_CP to shorten proof

[jstoobysmith]

Summary

Golfs the proof of MatrixMap.conj_isCompletelyPositive in
QuantumInfo/Channels/Unbundled.lean, collapsing a 52-line tactic block down
to two lines.

Motivation

The existing proof carried the note --TODO: This is identical to congruence_CP.
Indeed, congruence_CP (proved earlier in the same file) already establishes
(conj M).IsCompletelyPositive for M : Matrix B A 𝕜 with [RCLike 𝕜], via the
clean conj_kron/conj_isPositive route. conj_isCompletelyPositive is the
exact same statement over [RCLike R]; the only thing congruence_CP needs that
the ambient context here does not provide is DecidableEq on the codomain B,
which the original proof already pulled in with classical. (The companion lemma
of_kraus_CP likewise reaches congruence_CP and supplies decidability the same
way.)

So the long, manual Kronecker-index manipulation is entirely redundant and is
replaced by a direct appeal to the existing lemma.

Change

Before (52-line tactic proof doing a manual suffices … PosSemidef, index
juggling over Matrix.single/kron_def, convert, and a Cholesky-style
m = m'ᴴ * m' decomposition):

theorem conj_isCompletelyPositive (M : Matrix B A R) : (conj M).IsCompletelyPositive := by
  --TODO: This is identical to congruence_CP
  intro n m h
  classical
  open ComplexOrder in
  open Kronecker in
  suffices ((M ⊗ₖ 1 : Matrix (B × Fin n) (A × Fin n) R) * m * (M.conjTranspose ⊗ₖ 1)).PosSemidef by
    convert this
    ...
    tauto
  obtain ⟨m', rfl⟩ : ∃ B, m = B.conjTranspose * B := by
    ...
  convert Matrix.posSemidef_conjTranspose_mul_self ... using 1
  ...
  tauto

After:

theorem conj_isCompletelyPositive (M : Matrix B A R) : (conj M).IsCompletelyPositive := by
  -- This is `congruence_CP`, which only additionally needs `DecidableEq` on the codomain.
  classical
  exact congruence_CP M

The statement (name, binders, type) is unchanged. Only the proof body is edited;
no other declaration, import, or docstring is touched.

Verification

• lake build QuantumInfo.Channels.Unbundled — succeeds.
• lake build QuantumInfo — succeeds (8636 jobs), so all downstream users still
  compile.
• Axiom check on MatrixMap.conj_isCompletelyPositive: only propext,
  Classical.choice, Quot.sound (no sorry, no new axioms).

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.