refactor: QuantumInfo line lengths <100characters

[jstoobysmith]

This was done entirely using Claude Opus 4.8.

AI summary

Wrap QuantumInfo source lines to 100 characters

Reformats every file under ./QuantumInfo so no line exceeds 100 characters, by redistributing existing content across multiple lines. Pure formatting change — comments wrapped at word boundaries; Lean code broken at safe points (binder groups, after binary operators / :=, deeper-indented tactic continuations, inside bracketed argument lists) per the project's house style. 61 files changed.

Lemmas / definitions added or removed

None. No declarations were added, removed, or modified. Verified mechanically: the set of theorem/lemma/def/abbrev/instance/structure/class/inductive declarations is identical before and after (2146 in both), and the whitespace- and comment-stripped token stream of all 61 files matches the previous revision exactly, except for the semantics-preserving edits noted below.

Only non-whitespace edits (all semantics-preserving)

• Channels/CPTP.lean, States/Mixed/MState.lean — 4 places where a ; tactic separator became a newline (equivalent in Lean 4; the following tactic stays at the same indentation column).
• Capacity/Capacity.lean, ForMathlib/HermitianMat/CFC.lean — one variable [..] [..] command split into two variable lines (equivalent).
• Channels/Dual.lean, States/Mixed/MState.lean — a few trailing -- comments moved onto their own line above the code (comments are inert).

Reviewer map

Review in this order; spend the most time on the first group (densest wrapping decisions), and on the "non-whitespace edits" files above:

1. Largest / densest wraps — Entropy/Relative.lean, ForMathlib/HermitianMat/CFC.lean, ForMathlib/Majorization.lean, ForMathlib/Matrix.lean, ResourceTheory/SteinsLemma.lean, Entropy/SSA.lean, States/Mixed/MState.lean.
2. Medium — ForMathlib/LimSupInf.lean, ForMathlib/HermitianMat/LogExp.lean, ForMathlib/HermitianMat/Rpow.lean, ForMathlib/HermitianMat/Inner.lean, Channels/Unbundled.lean, ForMathlib/Isometry.lean, States/Entanglement.lean, Entropy/DPI.lean.
3. Remainder — the other ~40 files (small, mechanical splits).

Tip: review with whitespace ignored (git diff -w / "Hide whitespace" on GitHub) — most hunks collapse to nothing, leaving only the genuine edits called out above for scrutiny.

Known exception

One line remains >100 chars: ForMathlib/HayataGroup/TraceInequality/LownerHeinzCore.lean:10, a Lean import whose module path is a single unsplittable token (already over-length before this PR).

[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.