Write the migration-inventory audit note for the #7177 pass-through removals

[claude]

Context

Follow-up from #7177 (refactor(qiclean): reuse Kraus channel APIs directly).

docs/project_conventions.md §Style states the repository-local pass-through
exception:

a public declaration that merely forwards to an existing theorem, exposes a
bundled-structure field, or names a proof step now written at the use site
may be removed without a transition declaration, provided all non-Archive
uses are migrated, no blueprint \lean{...} tag cites the old name, and
the PR body plus an audit note name each removed declaration with its
replacement.

PR #7177 removed roughly twenty public pass-through declarations and
repointed all Blueprint \lean{} tags to their QICLean owners, but its body
only names the removed categories ("adjoints, invariant projections,
irreducibility, peripheral theory, correlations, map powers, and
channelhood") and no docs/audits/*.md note was added. The per-declaration
inventory required by the exception is missing.

Mathematical statement

N/A — this is a documentation/audit-trail obligation, not a formalization
task.

Source

• File: docs/project_conventions.md:9-16 (§Style, pass-through exception)

• Claim: "...the PR body plus an audit note name each removed declaration
  with its replacement."

• Diff evidence (PR refactor(qiclean): reuse Kraus channel APIs directly #7177, base 588d73d, head 63e7912): the following
  public declarations were deleted, each with a direct QICLean replacement
  used at their former call sites:

  Removed (TNLean)	Replacement (QICLean)
  MPSTensor.transferMap_conjTranspose_eq_adjoint	Kraus.mapLM_conjTranspose_eq_adjoint
  MPSTensor.transferMap_adjoint_eq_adjointMapLM	Kraus.adjointMapLM_apply (via Kraus.mapLM_conjTranspose_eq_adjoint)
  MPSTensor.transferMap_adjoint_apply_eq_adjointMap	Kraus.adjointMapLM_apply (via Kraus.mapLM_conjTranspose_eq_adjoint)
  MPSTensor.lowerZero_implies_invariance	Kraus.lowerZero_implies_invariance
  MPSTensor.isUnit_peripheral_eigenvector	Kraus.isUnit_peripheral_eigenvector
  MPSTensor.peripheralEigenvalues_pow_mem_of_irreducible_unital_of_adjoint_fixedPoint	Kraus.peripheralEigenvalues_pow_mem_of_irreducible_unital_of_adjoint_fixedPoint
  MPSTensor.peripheral_isRootOfUnity_of_irreducible_unital_of_adjoint_fixedPoint	Kraus.peripheral_isRootOfUnity_of_irreducible_unital_of_adjoint_fixedPoint
  MPSTensor.peripheralEigenvalues_mul_mem_of_irreducible_unital_of_adjoint_fixedPoint	Kraus.peripheralEigenvalues_mul_mem_of_irreducible_unital_of_adjoint_fixedPoint
  MPSTensor.peripheralEigenvalues_eq_range_primitiveRoot	Kraus.peripheralEigenvalues_eq_range_primitiveRoot
  MPSTensor.isIrreducibleCP_transferMap_conjTranspose_of_isIrreducibleTensor	Kraus.isIrreducibleMap_mapLM_conjTranspose ∘ Kraus.isIrreducibleMap_mapLM_of_isIrreducibleFamily
  MPSTensor.isIrreducibleTensor_of_isIrreducibleMap_conjTranspose	Kraus.isIrreducibleFamily_of_isIrreducibleMap_mapLM ∘ Kraus.isIrreducibleMap_mapLM_conjTranspose_iff
  MPSTensor.lowerZero_of_posSemidef_fixedPoint	Kraus.lowerZero_of_posSemidef_fixedPoint
  MPSTensor.invariance_implies_lowerZero	Kraus.invariance_implies_lowerZero
  MPSTensor.isIrreducibleCP_transferMap_of_isIrreducibleTensor	Kraus.isIrreducibleMap_transferMap_of_isIrreducibleFamily
  MPSTensor.isIrreducibleTensor_of_isIrreducibleMap	Kraus.isIrreducibleFamily_of_isIrreducibleMap_transferMap
  MPSTensor.self_correlation_persists	Kraus.self_correlation_persists
  MPSTensor.transferMap_conjTranspose	Kraus.map_conjTranspose
  MPSTensor.transferMap_pow_smul_eigenvector	Module.End.pow_apply_of_mem_eigenspace (Mathlib)
  MPSTensor.trace_eigenvector_eq_zero	Kraus.trace_eigenvector_eq_zero
  MPSTensor.posSemidef_pow_fixedPoint_unique_of_isPrimitivePaper	Kraus.posSemidef_pow_fixedPoint_unique
  MPSTensor.transferMap_pow_apply_eq_sum	Kraus.transferMap_pow_apply'
  MPSTensor.IsPrimitiveMPS.transferMap_isChannel	Kraus.isChannel_transferMap _ hP.norm (inlined)
  MPSTensor.isIrreducibleMap_of_isIrreducibleTensor	Kraus.isIrreducibleMap_transferMap_of_isIrreducibleFamily

  (Three already-@[deprecated] aliases in TNLean/MPS/Core/TransferPeripheral.lean
  were also deleted; these do not need inventorying since they were already
  flagged for removal.)

Formalization target

Not a Lean change. Add docs/audits/2026-08-25_issue7177_kraus_pass_through.md
(or similarly named) recording the table above, following the format of
existing notes such as docs/audits/2026-08-25_issue6861_wielandt_pass_through.md.

Mathematical reference

N/A (documentation/process obligation, not a paper-facing statement).

References

• PR: refactor(qiclean): reuse Kraus channel APIs directly #7177
• Convention: docs/project_conventions.md §Style
• Precedent notes: docs/audits/2026-08-20_issue6621_frobenius_pass_through.md,
  docs/audits/2026-08-25_issue6861_wielandt_pass_through.md