Exercise PLAN-315

Twirling sends any state to a twirl-invariant Werner state whose visibility, measured against the swap, equals that of the original state.

1. Left invariance of the measure makes the twirl commute with every unitary-tensor-unitary conjugation.
2. An already-Werner state is unchanged by the twirl, so twirling is idempotent.
3. Cyclicity of the trace plus the swap's invariance let the unitary pair cancel inside the visibility integral.
4. Averaging the constant original trace against the swap preserves the visibility.

Twirling produces a Werner state: by left invariance of the invariant measure, applying a fixed unitary pair to the twirled operator and reaveraging merely reparametrizes the integration variable, leaving the integral unchanged; hence the twirled operator commutes with every unitary-tensor-unitary conjugation, which is the defining symmetry of a Werner state. Already invariant: if a state already has the Werner symmetry, then every term in the twirl average equals the state itself, so the average is the state; applying this to an already-twirled operator shows twirling is idempotent, i.e. the twirled state is a fixed point. Visibility preserved: the visibility is the trace of the state against the swap operator. Compute the visibility of the twirled state by moving the swap inside the average and using cyclicity of the trace to conjugate the swap by the unitary pair; the swap commutes with every unitary tensored with itself, so the conjugated swap equals the swap, and the unitary pair cancels against its adjoint. Each term of the average therefore reduces to the trace of the original state against the swap, and averaging a constant returns that constant. Hence the twirled state has the same visibility as the original.

1. Shows twirling yields the Werner symmetry using left invariance of the measure to reparametrize the average (1 weight)
2. Proves twirling is idempotent: an already-symmetric state is a fixed point, so the twirled state is invariant under further twirling (1 weight)
3. Uses cyclicity of the trace and the swap's invariance under unitary-tensor-unitary conjugation to evaluate the twirled visibility (1 weight)
4. Concludes each averaged term equals the original trace against the swap, so visibility is preserved (1 weight)

No aligned Lean view has been admitted for this native core in this textbook checkpoint. This is not a claim that the underlying mathematics lacks a formal proof. Contributions must preserve this exact target contract and split.

Read the Lean track and existing diagnostic warmups

• website/research/sources.json

  leditzky-2025-repth-qit

  Source SHA-256: 9f85f45f20ed5a46931ad0dec3b94ee09748bc56e39fae29b0aefe910440b0ae · MIT metadata only
• Primary source

Contract: bc58bc4b583d136463b728d03b29019cf787f6c077b44e40f16f13ffad3be134

Item digest: 92a2b9973081ad5bf6b6ed502bb11e407263dfc26ea1de0bd92d9591e1674980

Graph snapshot: qcb-snapshot-ffa644f0da3031a1ce754b9a

Authored support steps: 4. This is not measured graph distance or model difficulty.